Title :
Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE
Author :
Halbwachs, Nicolas ; Lagnier, Fabienne ; Ratel, Christophe
fDate :
9/1/1992 12:00:00 AM
Abstract :
The benefits of using a synchronous data-flow language for programming critical real-time systems are investigated. 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. It is shown, using 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. As the language LUSTRE and its uses have already been discussed in several papers, emphasis is put on program verification
Keywords :
parallel languages; parallel programming; program verification; real-time systems; critical properties; critical real-time systems; data-flow language LUSTRE; dataflow approach; ergonomy; formal design; program verification; synchronous data-flow language; traditional description tools; verification methods; verification tool LESAR; Application software; Computer languages; Design methodology; Difference equations; Differential equations; Finite difference methods; Formal verification; Real time systems; Software quality; Switches;
Journal_Title :
Software Engineering, IEEE Transactions on
