Steam boiler control specification problem: A TLA solution

. Our solution to the specification problem in the specification language TLA+ is based on a model of operation where several components proceed synchronously. Our first specification concerns a simplified controller and abstracts from many details given in the informal problem description. We successively add modules to build a model of the state of the steam boiler, detect failures, and model message transmission. We give a more detailed controller specification and prove that it refines the abstract controller. We also address the relationship between the physical state of the steam boiler and the model maintained by the controller and discuss the reliability of failure detection. Finally, we discuss the implementability of our specification. 1 Introduction We propose a solution to the steam boiler control specification problem [AS] by means of a formal specification in the specification language TLA+, which is based on Lamport's Temporal Logic of Actions TLA [L94]. The overall str..