Title :
The generalized railroad crossing: a case study in formal verification of real-time systems
Author :
Heitmeyer, Constance ; Lynch, Nancy
Author_Institution :
Naval Res. Lab., Washington, DC, USA
Abstract :
A new solution to the generalized railroad crossing problem, based on timed automata, invariants and simulation mappings, is presented and evaluated. The solution shows formally the correspondence between four system descriptions: an axiomatic specification, an operational specification, a discrete system implementation, and a system implementation that works with a continuous gate model
Keywords :
automata theory; formal specification; formal verification; railways; real-time systems; axiomatic specification; continuous gate model; discrete system implementation; formal verification; generalized railroad crossing problem; invariants; operational specification; real-time systems; simulation mappings; system descriptions; system implementation; timed automata; Automata; Rail transportation; Real time systems; Software requirements and specifications;
Conference_Titel :
Real-Time Systems Symposium, 1994., Proceedings.
Conference_Location :
San Juan
Print_ISBN :
0-8186-6600-5
DOI :
10.1109/REAL.1994.342724
