Designing a controller for a multi-train multi-track system

Deepak Kapur, Victor L. Winter, Raymond S. Berg

Research output: Contribution to journalConference articlepeer-review

1 Scopus citations


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).

Original languageEnglish (US)
Pages (from-to)65-79
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Issue number1
StatePublished - Aug 2001
Externally publishedYes
EventATMOS 2001, Algorithmic Methods and Models for Optimization of Railways (Satellite Workshop of ICALP 2001) - Crete, Greece
Duration: Jul 13 2001Jul 13 2001

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Designing a controller for a multi-train multi-track system'. Together they form a unique fingerprint.

Cite this