Steam boiler control specification problem: A TLA solution

Frank Leßke, Stephan Merz

Abstract

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

Reference

@InCollection{lesske:steamboiler,
  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"
}