|Title||The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems|
|Publication Type||Conference Paper|
|Year of Publication||1994|
|Authors||Heitmeyer, C. L., and N. Lynch|
|Conference Name||IEEE Real-Time Systems Symposium|
|Conference Location||San Juan, Puerto Rico|
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.
|NRL Publication Release Number|| |