Generalized Railroad Crossing

During the last decade, a large collection of formal methods have been invented for specifying, designing, and analyzing real-time systems. To compare these methods and to better understand their use in developing practical real-time systems, one of us (Heitmeyer) has defined a benchmark problem, called the Generalized Railroad (GRC) Crossing problem [1]. The problem is as follows. The system to be developed operates a gate at a railroad crossing. The railroad crossing I lies in a region of interest R. A set of trains travel through R on multiple tracks in both directions. A sensor system determines when each train enters and exits region R. To describe the system formally, we define a gate function g from real times to the interval [0,90], where g(t)=0 means the gate is down and g(t)=90 means the gate is up. We also define a sequence of "occupancy intervals", where each occupancy interval is a maximal time interval during which one or more trains are in I. Given two "positive tolerance" constants xi(1) and xi(2), the problem is to develop a system to operate the crossing gate that satisfies the following two properties: Safety Property: The gate is down during all occupancy intervals. Utility Property: If t is not in any occupancy interval, nor within xi(1) prior to an occupancy interval, nor within xi(2) after an occupancy interval, then the gate is up. To solve the GRC problem, real-time researchers have applied a variety of formal methods, including process algebraic, event-based, and logic-based approaches. They have also used various mechanical proof systems, including PVS, EVES, and FDR, to formally analyze and verify their solutions. Three early efforts to solve the GRC problem are described in [2] This paper describes a new solution of the GRC based on the Lynch-Vaandrager timed automaton model , using invariant assertion and simulation mapping techniques. To develop the solution, a ``formal methods expert'' (Lynch) and an ``applications expert'' (Heitmeyer) worked closely together to refine the GRC problem statement and to design and verify an implementation. Our close collaboration was in sharp contrast to the limited interaction between the Naval Research Laboratory (NRL) group that originated the GRC problem and the formal methods groups that developed earlier solutions. In the earlier work, the NRL group limited interaction both to encourage original solutions and to prevent some groups from having more information and thus unfair advantage over other groups. While these early efforts produced a variety of solutions and many insights into the relative strengths and weaknesses of the different formalisms, they suffered from two limitations. First, because the original problem statement was somewhat ambiguous, each group solved a slightly different problem, which caused difficulties in comparing the solutions. Second, the limited interaction meant that deficiencies in the GRC problem statement went uncorrected. Our collaboration allowed us quickly to identify and correct these deficiencies. It also led us to represent the problem and its solution in a form that is both understandable to applications experts and usable by formal methods experts for verification. Related Publications There are several versions of this work in print. A summary version appeared in the 1994 RTSS symposium. A full version, with all proofs appears in a Technical Memo. Finally, a rewritten, summarized version appears as a book chapter. [1] C. L. Heitmeyer and R. D. Jeffords and B. G. Labaw. A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-time Systems, in Proc., Tenth Intern. Workshop on Real-Time Operating Systems and Software, May, 1993. [2] C. Heitmeyer and R. Jeffords. Formal specification and verification of real-time systems: A comparison study, Technical report, NRL, Wash., DC, 1994. In preparation.

TOC / LCS / MIT Last modified: Fri Jan 16 10:40:57 1998	Comments?