Beta 1


Title Modelling railway interlocking systems
Author Gjaldbæk, Torben
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2002
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.
Imprint Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK-2800 Kgs. Lyngby, Denmark
Keywords Formal methods; Java; railway interlocking systems; RAISE; safety; verification
Admin Creation date: 2006-06-22    Update date: 2012-12-20    Source: dtu    ID: 58300    Original MXD