Modelling railway interlocking systems |
| | Abstract | Railway interlocking systems serve to ensure the safety of railway traffic by preventing collisions and derailments. This thesis presents a formal model of interlocking systems for railway lines.
The initial model is generic and discrete event based. It is presented as an algebraic, applicative specification divided into five parts:
A part describing the static layout of lines,
A part describing dynamic properties of the uncontrolled domain,
A part describing the means of control for lines,
A part describing dynamic properties of the controlled domain,
A part describing the functions of interlocking systems.
Safety requirements are expressed using concepts from the uncontrolled and controlled domain. A series of proof obligations ensuring safety is stated. These proof obligations are verified using formal and mathematical proofs.
Two refinement steps are made, making the model more concrete. A main program using the functions of the interlocking system is specified. The refined model is implemented using the Java programming language, and a simulator visualizing the model is developed and tested. | | Keywords | Formal methods, Java, railway interlocking systems, RAISE, safety, verification | | Type | Master's thesis [Academic thesis] | | Year | 2002 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-THESIS-2002-66 | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|