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

Author

Halbwachs, Nicolas ; Lagnier, Fabienne ; Ratel, Christophe

Volume

18

Issue

9

fYear

1992

fDate

9/1/1992 12:00:00 AM

Firstpage

785

Lastpage

793

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;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.159839

Filename

159839