Abstract

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

Details

Actions