Name
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). |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1016/S1571-0661(04)00166-5 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
tracking system | Control theory,Program transformation,Simulation,Computer science,Control function,Automated theorem proving,Modeling language,Formal methods,Throughput,Train | Journal |
Volume | Issue | ISSN |
50 | 1 | 1571-0661 |
Citations | PageRank | References |
1 | 0.43 | 0 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Deepak Kapur | 1 | 2282 | 235.00 |
| Victor L. Winter | 2 | 110 | 17.04 |
| Raymond Berg | 3 | 1 | 0.77 |