Skip to main content
SpringerLink
Log in

The Steam Boiler problem in Lustre

  • Chapter
  • First Online:
Book cover Formal Methods for Industrial Applications

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1165))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. C. Lewerentz, T. Lindner (Eds.). Formal Development of Reactive Systems. Case Study Production Cell. Springer-Verlag, 1993.

    Google Scholar 

  2. Halbwachs N., A Tutorial of Lustre, IMAG, Grenoble, 1993.

    Google Scholar 

  3. Halbwachs N., Synchronous programming of reactive systems, Kluwer Academic, 1993

    Google Scholar 

  4. Halbwachs N., Lagnier F., Ratel C., Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE, IIE Trans. on Soft. Engin., Special issue on The Specification and Analusis of Real-Time Systems, September, 1992.

    Google Scholar 

  5. Bouajjani A., Fernadez J.-C, Halbwachs N., On the verification of safety properties. TR Spectre L12, IMAG, Grenoble, 1990.

    Google Scholar 

  6. Holzmann G.J., Design and Validation of Computer Protocols, 512 pgs, ISBN 0-13-539925-4, Publ. Prentice Hall, (c) 1991 AT&T Bell Laboratories.

    Google Scholar 

  7. Manna Z., Pnueli A., Temporal Verification of Reactive Systems: Safety, Springer-Verlag, 1995.

    Google Scholar 

  8. R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine. The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science B, Vol. 138, pp. 3–34. January 1995.

    Google Scholar 

  9. S. Bensalem, P. Caspi, C. Parent, Handling data-flow programs in PVS, http:// www.imag.fr/VERIMAG/PEOPLE/Catherine.Parent, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire de Téléinformatique, Ecole Polytechnique Fédérale, CH-1015, Lausanne, Switzerland

    Thierry Cattel & Gregory Duval

Authors
  1. Thierry Cattel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gregory Duval
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jean-Raymond Abrial Egon Börger Hans Langmaack

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Cattel, T., Duval, G. (1996). The Steam Boiler problem in Lustre. In: Abrial, JR., Börger, E., Langmaack, H. (eds) Formal Methods for Industrial Applications. Lecture Notes in Computer Science, vol 1165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027235

Download citation

  • DOI: https://doi.org/10.1007/BFb0027235

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61929-1

  • Online ISBN: 978-3-540-49566-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation