Solutions to the Steam Boiler Case Study

21 solutions to the steam boiler case study have been collected in a Lecture Notes in Computer Science volume which includes a CD-ROM that contains executable code, full definitions of all parts of the specification, and detailed descriptions of foundational matters where appropriate. This volume is available from Springer-Verlag or your local bookstore as
  • 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)

  • This WWW page contains the abstracts of these contributions and the full text of all other solutions submitted so far.

    Solutions covered by the LNCS volume

  • Mattin Addibpour and Enn Tyugu (Royal Institute of Technology, Stockholm, Sweden).
    Structural Synthesis of Programs from Refined User Requirements (Programming boiler control in NUT).
  • Christoph Andriessens and Thomas Lindner (FZI Karlsruhe, Germany).
    Using FOCUS, LUSTRE, and Probability Theory for the Design of a Reliable Control Program.
  • Christoph Beierle (Fernuniversität-GH Hagen, Germany), Egon Börger (Università di Pisa, Italy), Igor Ðurdanovic (Universität-GH Paderborn, Germany), Uwe Glässer (Universität-GH Paderborn, Germany), Elvinia Riccobene (Università di Catania, Italy).
    Refining Abstract Machine Specifications of the Steam Boiler Control to Well Documented Executable Code.
  • Michel Bidoit (Ecole Normale Supérieure, Paris, France), Claude Chevenier, Christine Pellen, and Jérôme Ryckbosch (Direction des Etudes et Recherches, Electricité de France).
    An Algebraic Specification of the Steam-Boiler Control System.
  • Robert Büssow and Matthias Weber (Technische Universität Berlin, Germany).
    A Steam-Boiler Control Specification with Statecharts and Z.
  • Michael Butler (Univ. of Southampton, United Kingdom), Emil Sekerinski (Åbo Akademi, Turku, Finland), Kaisa Sere (Univ. of Kuopio, Finland).
    An Action System Approach to the Steam Boiler Problem.
  • Thierry Cattel and Gregory Duval (Ecole Polytechnique Fédérale, Lausanne, Switzerland).
    The Steam Boiler Problem in Lustre.
  • Jorge Cuéllar and Isolde Wildgruber (Siemens R&D, Munich, Germany).
    The Steam Boiler Controller Problem: The TLT Solution.
  • Jorge Cuéllar and Isolde Wildgruber (Siemens R&D, Munich, Germany).
    The Real-Time Behaviour of the Steam Boiler.
  • Gregory Duval and Thierry Cattel (Ecole Polytechnique Fédérale, Lausanne, Switzerland).
    Specifying and Verifying the Steam Boiler Problem with SPIN.
  • Angelo Garganti and Angelo Morzenti (Politecnico di Milano, Italy).
    TRIO Specification of a Steam Boiler Controller.
  • Marie-Claude Gaudel (Université de Paris Sud & CNRS, Orsay, France), Pierre Dauchy (IMASSA-CERMA, Brétigny/Orge, France), Carole Khoury (Université de Paris Sud & CNRS, Orsay, France).
    A Formal Specification of the Steam-Boiler Control Problem by Algebraic Specifications with Implicit State.
  • Thomas A. Henzinger and Howard Wong-Toi (Cornell University, Ithaca, USA).
    Using HYTECH to synthesize control parameters for a steam boiler.
  • Yves Ledru and Marie-Laure Potet (IMAG, Grenoble, France).
    A VDM specification of the steam-boiler problem.
  • Gunter Leeb (Vienna University of Technology, Austria), Nancy Lynch (Massachusetts Institute of Technology, USA).
    Proving Safety Properties of the Steam Boiler Controller.
    (The authors provide more recent information on this contribution.)
  • Frank Leßke and Stephan Merz (Technical University of Munich, Germany).
    Steam boiler control specification problem: A TLA solution.
  • Li XiaoShan (UNU/IIST, Macau), Wang JuAn (University of Macau).
    Specifying Optimal Design of a Steam-boiler System.
  • Peter Csaba Ölveczky (University of Bergen, Norway), Piotr Kosiuczenko (Politechnika Warszawska, Poland and LMU Munich, Germany), Martin Wirsing (LMU Munich, Germany.
    An object-oriented algebraic steam-boiler control specification.
  • Michael Schenke (University of Oldenburg, Germany), Anders P. Ravn (Technical University of Denmark, Lyngby, Denmark).
    Refinement from a control problem to programs.
  • Christian P. Schinagl (TU-Graz, Austria).
    VDM specification of the steam-boiler control using RSL notation..
  • Jan Vitt (University of Kiel, Germany), Jozef Hooman (Eindhoven University of Technology, The Netherlands).
    Assertional Specification and Verification Using PVS of the Steam Boiler Control System.
  • Andreas Willig (Technical University Berlin, Germany), Ina Schieferdecker (GMD Fokus, Berlin, Germany).
    Specifying and Verifying the Steam Boiler Control System with Time Extended LOTOS.
  • Full text of further solutions

  • So-Ming So and Mabo R. Ito (The Univeristy of British Columbia, Canada).
    GrafTab - An Innovative Requirements Specification Method (A Requirements Specification of a Steam Boiler Controller).
    October 6, 1995.
  • Hans Rischel (Technical Univ. of Denmark), Jorge Cuellar (Siemens Corporate Research and Development, Munich, Germany), Simon Mørk (Technical Univ. of Denmark), Anders P. Ravn (Technical Univ. of Denmark), Isolde Wildgruber (Siemens Corporate Research and Development).
    Development of Safety-Critical Real-Time Systems.
    October 31, 1995.
  • Wang JuAn (University of Macau), Li XiaoShan (UNU/IIST, Macau).
    A Duration Calculus Approach to Specifying a Steam-boiler Control System.
    2nd version, December 1995.
  • Lars Kühne, Michael Siegel, and Bernd Weber (University of Kiel, Germany).
    Development of a Steamboiler Control using Statemate.
    December 1995.
  • Jim Alves-Foss (Univ. of Idaho, USA).
    A Constraint-Oriented Specification of a Steam-Boiler Controller in Higher Order Logic.
    January 1996.
  • Hugo Fierz (ETH Zürich, Switzerland).
    Steam Boiler Control Specification Problem: CIP Solution.
    January 1996.
  • Victor Yodaiken (New Mexico Institute of Technology, USA).
    Specification with Moore machines: the steam boiler control example.
    January 1996.
  • Pascal Bernard (IUT Nantes, France).
    A Z specification of the boiler.
    January 1996.
  • Armen Gabrielian (UniView Systems, Montain View, USA).
    The HMS Machine Specification of a Steam Boiler Control System.
    January 1996.
  • Marie-Claude Gaudel (Université de Paris Sud & CNRS, Orsay, France), Pierre Dauchy (IMASSA-CERMA, Brétigny/Orge, France), Carole Khoury (Université de Paris Sud & CNRS, Orsay, France).
    A Formal Specification of the Steam-Boiler Control Problem by Algebraic Specifications with Implicit State.
    January 1996.
  • Mete Kabakcioglu (Universidad de Los Andes , Bogotá, Colombia and FH Albstadt-Sigmaringen, Germany).
    Steam Boiler Specification with TOP: An Executable Specification Language with Time, Objects and Productions.
    March 1996.
  • A. John van Shouwen (Nortel, Canada).
    Steam-Boiler Controller System (SBCS) Specification Using the SCR Approach.
    May 1996.

  • Last modified: Martin Fränzle (mf@informatik.uni-kiel.d400.de), Tue Dec 10, 1996