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 Citation (Scopus)

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
StatePublished - 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

Controller
Controllers
Control Function
Acceleration control
Rapid transit
Formal methods
Program Transformation
Formal Methods
Modeling Language
Railway
Efficient Implementation
Throughput
Confidence
Specifications
Proof by induction
Safety
Specification
Optimization
Methodology
Theorem

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Designing a controller for a multi-train multi-track system. / Kapur, Deepak; Winter, Victor L.; Berg, Raymond S.

In: Electronic Notes in Theoretical Computer Science, Vol. 50, No. 1, 01.08.2001, p. 65-79.

Research output: Contribution to journalConference article

Kapur, Deepak ; Winter, Victor L. ; Berg, Raymond S. / Designing a controller for a multi-train multi-track system. In: Electronic Notes in Theoretical Computer Science. 2001 ; Vol. 50, No. 1. pp. 65-79.
@article{706ba30a9161466fade1349d614aa63d,
title = "Designing a controller for a multi-train multi-track system",
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).",
author = "Deepak Kapur and Winter, {Victor L.} and Berg, {Raymond S.}",
year = "2001",
month = "8",
day = "1",
doi = "10.1016/S1571-0661(04)00166-5",
language = "English (US)",
volume = "50",
pages = "65--79",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "1",

}

TY - JOUR

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

AU - Kapur, Deepak

AU - Winter, Victor L.

AU - Berg, Raymond S.

PY - 2001/8/1

Y1 - 2001/8/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=19144369001&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=19144369001&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)00166-5

DO - 10.1016/S1571-0661(04)00166-5

M3 - Conference article

AN - SCOPUS:19144369001

VL - 50

SP - 65

EP - 79

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 1

ER -