Steam boiler control specification problem: A TLA solution

Frank Leßke, Stephan Merz
We specify a controller for a steam boiler problem, which was presented to the formal methods community as a competitive case study. 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.
© Springer-Verlag
Available as:  gzip'ed Postscript 
See also:  Steamboiler problem page
  author =    "Frank Le{\ss}ke and Stephan Merz",
  title =     "Steam boiler control specification problem:
               A {TLA} solution",
  booktitle = "Formal Methods for Industrial Applications:
               Specifying and Programming the Steam Boiler Control",
  publisher = "Springer-Verlag",
  year =      1996,
  editor =    "J.-R. Abrial and E. B{\"o}rger and H. Langmaack",
  volume =    1165,
  series =    "{L}ecture {N}otes in {C}omputer {S}cience",
  pages =     "339--359",
  address =   "Berlin"

Stephan Merz
Last modified: Mon Feb 17 14:57:40 MET 2003