TitleThe Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems
Publication TypeConference Paper
Year of Publication1994
AuthorsHeitmeyer, C. L., and N. Lynch
Conference NameIEEE Real-Time Systems Symposium
Conference LocationSan Juan, Puerto Rico
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.

Full Text

HeitmeyerLynch1994b.pdf

NRL Publication Release Number

04-1221-1296