Gunter Leeb and Nancy Lynch. Proving Safety Properties of the Steam Boiler Controller. In Jean-Raymond Abrial, Egon Boerger, and Hans Langmaack, editors, Proceedings of Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, volume 11654 of Lecture Notes in Computer Science, Springer-Verlag 1996. (Full Version-Corrected / Short Version-Corrected)

Abstract

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.''

Corrections

After our paper "Proving Safety Properties of the Steam Boiler Controller" went already to print, Myla Archer and Constance Heitmeyer verified the lengthy lemmas and theorems with the theorem prover PVS. Unfortunately, several errors were found in the proofs. A summary of the corrections to the (published) paper can be found here (full/short) or downloaded: Corrections for the full version or short version . No major changes were done to the model.