Gunter Leeb and Nancy Lynch: Proving Safety Properties of the
Steam Boiler Controller
In this paper we model a hybrid system consisting of a continuous steam
boiler and a discrete controller. Our model uses Timed Automata to show
formally that certain safety requirements can be guaranteed under the
described assumptions and failure model. We prove incrementally that a
simple controller model and a controller model tolerating sensor faults
preserve the required safety conditions. The specification of the steam
boiler and the failure model follow the specification problem for
participants of the Dagstuhl Meeting Methods for Semantics and
Specification.