Programming and verifying real-time systems by means of the synchronous data-flow programming language Lustre

Abstract:
We investigate the benefits of using a synchronous data-flow language for programming critical real-time systems. These benefits concern ergonomy --- since the dataflow approach meets traditional description tools used in this domain ---, and ability to support formal design and verification methods. We show, on a simple example, how the language Lustre and its associated verification tool Lesar, can be used to design a program, to specify its critical properties, and to verify these properties.

Reference:

   @ARTICLE{lesar:tse,
      AUTHOR = {N. Halbwachs and F. Lagnier and C. Ratel },
      TITLE = {Programming and verifying real-time systems by means of 
               the synchronous data-flow programming language Lustre},
      JOURNAL = {IEEE Transactions on Software Engineering, 
                 Special Issue on the Specification and Analysis 
                 of Real-Time Systems},
      MONTH={September },
      YEAR=1992
   }

Postscript file