FM Past Program: Union Switch & Signal Project

This page is not maintained. It is probably out of date.
As part of a joint research agreement, NASA Langley formal methods researchers collaborated with engineers at Union Switch and Signal (US&S) to use Formal Methods in the design of railway switching and control applications. Railway switching control systems, like digital flight control systems, are safety critical systems. US\&S is the leading U.S. supplier of railway switching control systems. Their Advanced Technology Group, lead by Dr. Joseph Profeta, has applied formal methods in past efforts and turned to NASA for expertise in integrating these techniques into their next generation products.

The initial project, started in 1993, was a cooperative effort between NASA, US&S and Odyssey Research Associates. The result of this first years work was a formal mathematical model of a railway switching network, defined in two levels. The top most level of the model provides the mechanisms for defining the basic concepts; track, switches, trains and their positions and control liners of a train (i.e. how far down the track it has clearance to travel.) The second level is a formalization of the standard scheme used in railroad control, the block model control system. A proof that the fixed block control system is ``safe'' with respect to the top level model has been completed. Models of US&S proprietary control schemes were also formulated.

The European formal methods community has addressed safety properties of certain components of railroad control systems, but the work there has typically been at lower level. The cooperative work with US&S is unique in that a high level model of a railroad system has been described and used to analyze the safety of various control schemes.

The next phase of the collaborative effort will concentrate on formal modeling and analysis of the fault-tolerant core of US&S's next generation fail-stop control architecture.

References (These may be ordered)

  1. Hoover, D. N. A Mathematical Model for Railway Control Systems. NASA Contractor Report 198353, June 1996.

  2. Profeta, Joe; and Hoover, D.N: Union Switch & Signal Project, Slides presented at the Third NASA Langley Formal Methods Workshop, May 10-12, 1995.

Curator and Responsible NASA Official: C. Michael Holloway
last modified: 21 March 1996 (11:12:24)