The steam boiler problem in Lustre

This paper reports the results of specifying, verifying and implementing the steam boiler problem with Lustre. The model is detailed and is able to drive the system and takes device failures (pumps, pump controllers, water, steam and transmission) and emergency stop into account. Safety properties have been checked on the model with Lesar, the Lustre model-checker. An implementation of the system have been made using the C code produced by Lustre from the model and linked with the TCL/TK simulation. This application shows Lustre's suitability for developing safe control process problems from specifications


Published in:
Formal Methods for Industrial Applications. Specifying and Programming the Steam Boiler Control, 149-64
Presented at:
Schloss Dagstuhl, Germany
Year:
1996
Publisher:
Springer-Verlag
Laboratories:




 Record created 2007-01-11, last modified 2018-03-17


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)