Designing a Controller for a Multi-Train Multi-Track System1 1This work was supported by the United States Department of Energy under Contract DEAC04-94AL85000. Sandia is a multiprogram laboratory operated by Sandia Corporation, a Lockheed Martin Company, for the United States Department of Energy.
Deepak Kapur, Victor Winter, Raymond S. Berg · Electronic Notes in Theoretical Computer Science · 2001
The use of formal methods for analyzing and synthesizing a controller for a multi-train multi-track railway system is discussed. The research was motivated by a case study involving the Bay Area Rapid Transit (BART) system. The overall goal is to design a train acceleration control function that enables trains to be safely placed but also increases system throughput. The use of a modeling language for specifying safety properties and a control function is illustrated. The program transformation methodology supported in the HATS system is employed to generate an efficient implementation from a high-level specification of a controller. This implementation can then be used to simulate the controller behavior, thus further enhancing confidence in the design. Properties of optimization transformations can be verified using an rewrite-rule based induction theorem prover Rewrite Rule Laboratory (RRL).