Paper Info
Title
Safety Property Verification of ESTEREL Programs and Applications to Telecommunications Software
Abstract
We present a technique for automatically verifying linear- time tempo- ral logic safety properties of programs written in E STEREL, a formally-defined language for programming reactive systems. In our approach, linear-time tempo- ral logic safety properties are first translated into ESTEREL programs that model these properties. Using the E STEREL compiler, the translations are compiled in parallel with the E STEREL program to be verified. A trivial reachability analysis of the output of the compiler then indicates whether or not th e safety property is satisfied by the program. We describe two real-world software problems — E S- TEREL versions of two features of the AT&T 5ESS R switching system — and one well-known benchmark problem — the generalized railroad cr ossing problem — that we have verified using our technique and associated toolset.
Year
DOI
Venue
1995
10.1007/3-540-60045-0_45
CAV
Keywords
Field
DocType
telecommunications software,safety property verification,esterel programs,linear time,reactive system,satisfiability
Programming language,Computer science,Algorithm,Telecommunications control software,Linear temporal logic,Compiler,Reachability,Software,Esterel,Temporal logic,Reactive system
Conference
Volume
ISSN
ISBN
939
0302-9743
3-540-60045-0
Citations 
PageRank 
References 
41
3.74
11
Authors
3
Name
Order
Citations
PageRank
Lalita Jategaonkar Jagadeesan128629.80
Carlos Puchol213818.65
James E. Von Olnhausen310411.05