||Modelling railway interlocking systems
||Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
||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.
||Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK-2800 Kgs. Lyngby, Denmark
||Formal methods; Java; railway interlocking systems; RAISE; safety; verification
Creation date: 2006-06-22
Update date: 2012-12-20