The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.09 - September (1992 vol.18)
pp: 785-793
ABSTRACT
<p>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.</p>
INDEX TERMS
data-flow language LUSTRE; synchronous data-flow language; critical real-time systems; ergonomy; dataflow approach; traditional description tools; formal design; verification methods; verification tool LESAR; critical properties; program verification; parallel languages; parallel programming; program verification; real-time systems
CITATION
N. Halbwachs, F. Lagnier, C. Ratel, "Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE", IEEE Transactions on Software Engineering, vol.18, no. 9, pp. 785-793, September 1992, doi:10.1109/32.159839
16 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool