Heitmeyer, C.L. and N. Lynch, "The Generalized Railroad Crossing: A
Case Study in Formal Verification of Real- Time Systems",
NRL Memorandum Report 7619, Wash, D.C,
1994.

<blockquote>
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.  The details
of the proofs, which were omitted from the conference paper due to
lack of space, are included.
</blockquote>