language: en

Refining Abstract Machine Specifications of the Steam Boiler Control to Well Documented Executable Code

Christoph Beierle, Egon Borger, Igor D - urd -anovic, Uwe Glasser, Elvinia Riccobene
1 Fernuniversitat-GH Hagen,
Germany,
christoph.beierle@fernuni-hagen.de
2 Universita di Pisa,
Italy,
boerger@di.unipi.it
3 Universitat-GH Paderborn,
Germany,
igor@uni-paderborn.de
4 Universitat-GH Paderborn,
Germany,
glaesser@uni-paderborn.de
5 Universita di Catania,
Italy,
riccobene@dipmat.unict.it

Abstract. We use the steam boiler control specification problem to illustrate how the evolving algebra approach to the specification and the verification of complex systems can be exploited for a reliable and well documented development of executable, but formally inspectable and systematically modifiable code. A hierarchy of stepwise refined abstract machine models is developed, the ground version of which can be checked for whether it faithfully reflects the informally given problem. The sequence of machine models yields various abstract views of the system, making the various design decisions transparent, and leads to a C++ program. This program has been demonstrated during the Dagstuhl-Meeting on Methods for Semantics and Specification, in June 1995, to control the Karlsruhe steam boiler simulator satisfactorily. The abstract machines are evolving algebras and thereby have a rigorous semantical foundation, allowing us to formalize and prove, under precisely stated assumptions, some typical sample properties of the system. This provides insight into the structure of the system which supports easily maintainable extensions and modifications of both the abstract specification and the implementation.

1 Introduction