Connie Heitmeyer and Nancy Lynch. The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time System. Proceedings of the 15th IEEE Real-Time Systems Symposium, pages 120--131, San Juan, Puerto Rico, December 1994. IEEE Computer Society Press. .pdf.

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.