Loading...
Please wait, while we are loading the content...
Similar Documents
Safety Property Verification of ESTEREL Programs and . . . (1995)
| Content Provider | CiteSeerX |
|---|---|
| Author | Jagadeesan, Lalita Jategaonkar Puchol, Carlos Olnhausen, James E. Von |
| Description | We present a technique for automatically verifying linear-time temporal logic safety properties of programs written in ESTEREL, a formally-defined language for programming reactive systems. In our approach, linear-time temporal logic safety properties are first translated into ESTEREL programs that model these properties. Using the ESTEREL compiler, the translations are compiled in parallel with the ESTEREL program to be verified. A trivial reachability analysis of the output of the compiler then indicates whether or not the safety property is satisfied by the program. We describe two real-world software problems --- ESTEREL versions of two features of the AT&T5ESS switching system --- and one well-known benchmark problem --- the generalized railroad crossing problem --- that we have verified using our technique and associated tool set. |
| File Format | |
| Language | English |
| Publisher Date | 1995-01-01 |
| Publisher Institution | IN PROCEEDINGS OF THE 7TH INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION, VOLUME 939 OF THE LECTURE NOTES IN COMPUTER SCIENCE |
| Access Restriction | Open |
| Subject Keyword | Safety Property Verification Real-world Software Problem Esterel Version Safety Property Esterel Program Linear-time Temporal Logic Safety Property Trivial Reachability Analysis Well-known Benchmark Problem Esterel Compiler Formally-defined Language Reactive System Associated Tool Set |
| Content Type | Text |
| Resource Type | Article |
