Paper Info
Title
Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE
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.
Year
DOI
Venue
1992
10.1109/32.159839
Software Engineering, IEEE Transactions  
Keywords
Field
DocType
associated verification tool,verifying real-time systems,language lustre,benefits concern ergonomy,synchronous data-flow language,critical property,dataflow approach,program verification,critical real-time system,verification method,synchronous data-flow language lustre,formal design,computer languages,differential equations,application software,real time systems,parallel programming,difference equations,switches,ergonomy,model checking,indexing terms,reactive system,finite difference methods,formal verification,design methodology,software quality,data flow
Formal design,Programming language,Computer science,Real-time computing,Real-time operating system,Theoretical computer science,Dataflow,Lustre (programming language),Lustre (mineralogy),Synchronous Data Flow,Software development,Data flow diagram
Journal
Volume
Issue
ISSN
18
9
0098-5589
Citations 
PageRank 
References 
126
8.23
20
Authors
3
Search Limit
100126
Name
Order
Citations
PageRank
Nicolas Halbwachs13957426.43
Fabienne Lagnier231326.77
Christophe Ratel320918.84