Paper Info
Title
Specifying, programming and verifying real-time systems using a synchronous declarative language
Abstract
We advocate the use of the synchronous declarative language Lustre as a unique language for specifying and programming real-time systems. Furthermore, we show that the finite automaton produced by the Lustre compiler may be used for verifying many logical properties, by model checking. The paper deals with an example program, extracted from a railways regulation system.
Year
DOI
Venue
1989
10.1007/3-540-52148-8_18
computer aided verification
Keywords
Field
DocType
synchronous declarative language,verifying real-time systems,real-time system,finite automaton,model checking,real time systems
Fifth-generation programming language,Programming language,Model checking,Computer science,Algorithm,Linear temporal logic,Compiler,Finite-state machine,Declarative programming,Temporal logic,Boolean data type
Conference
Volume
ISSN
ISBN
407
0302-9743
0-387-52148-8
Citations 
PageRank 
References 
21
12.68
7
Authors
4
Name
Order
Citations
PageRank
N. Halbwachs124432.81
Daniel Pilaud22413.46
Ouabdesselam, F.311821.72
A-C. Glory42112.68