Modelling Interlocking Systems for Railway Stations |
| | Abstract | Interlocking systems are used for ensuring the safety of trains. This master thesis is made in cooperation with Banedanmark and deals with relay-based interlocking systems for railway stations. The goal of this project is to develop a formal method for verifying that such systems guarantee the safety of trains.
By using RSL models of interlocking systems, this thesis deduces an automated procedure for making an RSL-SAL transition system that defines the dynamic behaviour of an interlocking system. Also, the procedure specifies how to auto-generate confi dence conditions for the generated transition system, formulated using Linear Temporal Logic (LTL). Finally, a tool for computing such a transition system and its associated con fidence conditions is implemented using Java.
Furthermore, this thesis develops patterns for specifying the behaviour of external inputs to an interlocking system (e.g. a rule can de fine when a train can enter a station), formulated using RSL-SAL. Also, patterns for specifying safety properties are developed using LTL.
Altogether, the tool and patterns de fine a method that uses the state-space based model checker SAL for verifying that interlocking systems guarantee the safety of trains. The method has successfully been applied to a Danish railway station. | | Type | Master's thesis [Academic thesis] | | Year | 2008 | | Publisher | Technical University of Denmark, DTU Informatics, E-mail: reception@imm.dtu.dk | | Address | Asmussens Alle, Building 305, DK-2800 Kgs. Lyngby, Denmark | | Series | IMM-M.Sc.-2008-68 | | Note | DTU supervisor: Associate Professor Anne Haxthausen, ah@imm.dtu.dk, DTU Informatics | | Electronic version(s) | [pdf] | | Publication link | http://www.imm.dtu.dk/English.aspx | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|