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.
ABSTRACT
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.
Postscript
With separate annex containing PVS theories on CD-ROM, pp. 30.
Postscript