@MASTERSTHESIS\{IMM2012-06262,
    author       = "M. Aan{\ae}s and H. P. Thai",
    title        = "Modelling and Verification of Relay Interlocking Systems",
    year         = "2012",
    school       = "Technical University of Denmark, {DTU} Informatics, {E-}mail: reception@imm.dtu.dk",
    address      = "Asmussens Alle, Building 305, {DK-}2800 Kgs. Lyngby, Denmark",
    type         = "",
    note         = "{DTU} supervisor: Associate Professor Anne Haxthausen, ah@imm.dtu.dk, {DTU} Informatics",
    url          = "http://www.imm.dtu.dk/English.aspx",
    abstract     = "Electrical relay based interlocking systems are widely used by Banedanmark to ensure safe operation of trains at stations in Denmark. These systems are documented by diagrams showing the electrical circuitry, physical track layout of the stations and train route tables. 
The safety of each station is currently verified by inspecting the diagrams by hand. This process is time consuming and possibly error-prone. Therefore Banedanmark wishes to automate the process. 
Our goal is to develop a method for automated model and safety property generation of the external part of a particular type of relay interlocking system, the {DSB} type 1954. This is then to be combined with the already developed model of the internal system and verified as a whole.
We specified a data model for interlocking plans, developed a behavioural model of external events and formalised safety properties which, among other things, assert that trains does not collide and does not derail. We then developed an executable specification of a generator that, given an interlocking plan, can generate a model of the external events. This model can then be combined with the model of the internal events and model checked.
The entire process was applied to the small Danish railway station Stenstrup, which uses the {DSB} type 1954 relay interlocking system. The result is that all generated safety properties are satisfied for the combined model of the interlocking system at Stenstrup."
}