Assertional Specification and Verification using PVS of the Steam Boiler Control System

Jan Vitt and Jozef Hooman

Appeared in: Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165, Springer-Verlag, pages 453-472, 1996.


An implementation of the steam boiler control system has been derived using a formal method based on assumption/commitment pairs. Intermediate stages of top-down design are represented in a mixed formalism where programs and assertional specifications are combined in a single framework. Design steps can be verified by means of compositional proof rules. This framework has been defined in the specification language of the verification system PVS (Prototype Verification System). By the interactive proof checker of PVS, the correctness of each refinement step has been checked mechanically.


With separate annex containing PVS theories on CD-ROM, pp. 30.