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

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

Research output: Contribution to journalConference article

1 Scopus citations

Abstract

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
Volume50
Issue number1
DOIs
Publication statusPublished - Aug 1 2001
EventATMOS 2001, Algorithmic Methods and Models for Optimization of Railways (Satellite Workshop of ICALP 2001) - Crete, Greece
Duration: Jul 13 2001Jul 13 2001

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this