Heitmeyer, C.L. and N. Lynch, "The Generalized Railroad Crossing: A
Case Study in Formal Verification of Real-Time Systems",
Proceedings, 15th IEEE Real-Time Systems Symposium,
Dec 7-9, 1994.

<blockquote>
A New Solution to the Generalized Railroad Crossing problem, based on
time 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.
</blockquote>