Modelling and Verifi cation of Relay Interlocking Systems



AbstractElectrical 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.
TypeMaster's thesis [Industrial collaboration]
Year2012
PublisherTechnical University of Denmark, DTU Informatics, E-mail: reception@imm.dtu.dk
AddressAsmussens Alle, Building 305, DK-2800 Kgs. Lyngby, Denmark
SeriesIMM-M.Sc.-2012-14
NoteDTU supervisor: Associate Professor Anne Haxthausen, ah@imm.dtu.dk, DTU Informatics
Electronic version(s)[pdf]
Publication linkhttp://www.imm.dtu.dk/English.aspx
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering