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 language | English (US) |
|---|---|
| Pages (from-to) | 65-79 |
| Number of pages | 15 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 50 |
| Issue number | 1 |
| DOIs | |
| State | Published - Aug 2001 |
| Externally published | Yes |
| Event | ATMOS 2001, Algorithmic Methods and Models for Optimization of Railways (Satellite Workshop of ICALP 2001) - Crete, Greece Duration: Jul 13 2001 → Jul 13 2001 |
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)