@MASTERSTHESIS\{IMM2002-01260,
    author       = "T. Gjaldb{\ae}k",
    title        = "Modelling railway interlocking systems",
    year         = "2002",
    keywords     = "Formal methods, Java, railway interlocking systems, {RAISE,} safety, verification",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/1260-full.html",
    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."
}