The Steam Boiler Control Specification Problem

by J.-R. Abrial, E. Börger, and H. Langmaack

Please note:
A Lecture Notes in Computer Science volume on the Steam Boiler Control Specification Problem is now available from Springer-Verlag or your local bookstore. Its title is

Jean-Raymond Abrial, Egon Börger, and Hans Langmaack.
Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control.
LNCS 1165, Springer-Verlag, October 1996. (ISBN 3-540-61929-1)

A number of case studies have been proposed for testing semantic methods in computer science with respect to their versatility and applicability to embedded control system design. Some of these case studies have been treated in a number of different formalisms, giving opportunity for comparing the strengths and weaknesses of the individual methods.

Based on the insight that thorough comparison between the various design formalisms proposed in the literature as well as some amount of unification would be crucial both to industrial takeover and to scientific progress in the field, an international seminar on "Methods for Semantics and Specification" was held at Schloß Dagstuhl, Wadern, Germany, on June 5-9, 1995. The seminar took the form of a "competition" between different researchers who had been invited as representatives of their particular methods. The competition was on the steam boiler control specification problem of J.-R. Abrial, E. Börger, and H. Langmaack, which has been posed to the participants as a common case study. This specification problem has been derived from an original text that has been written by LtCol. J.C. Bauer for the Institute for Risk Research of the University of Waterloo, Ontario, Canada. The original text has been submitted as a competition problem to be solved by the participants of the International Software Safety Symposium organized by the Institute for Risk Research.

The organizers of the Dagstuhl seminar "Methods for Semantics and Specification" would very much like to invite further researchers to the competition. These web pages have proved to be an effective means for information dissemination between research groups and will remain open for new contributions.

Everybody being interested in the case study may follow the hyperlinks to obtain

the problem statement of the steam boiler control specification problem,
additional information concerning the dynamic behaviour of the steam boiler,
the report on the Dagstuhl seminar "Methods for Semantics and Specification",
a Tcl/Tk-based steam boiler simulator written by Annette Lötzbeyer ( Forschungszentrum Informatik, Karslruhe, Germany),
solutions to the specification problem received thus far.

Solutions should be submitted electronically (preferrably as a Postscript file) to

   Martin Fränzle   (mf@informatik.uni-kiel.d400.de)
   Institut für Informatik und Praktische Mathematik
   Christian-Albrechts-Universität Kiel
   Preußerstr. 1-9
   D-24105 Kiel
   Germany

for inclusion into the WWW page.

If you are interested in other comparative studies on formal methods, have a look at the case study "Production Cell" that was launched by the Forschungszentrum Informatik, Karslruhe, Germany, and coordinated by Claus Lewerentz and Thomas Lindner.

Last modified: Martin Fränzle (mf@informatik.uni-kiel.d400.de), Thu, Nov 14, 1996