Beta 1

Title Modelling Interlocking Systems for Railway Stations
Author Le Bliguet, Marie
Andersen Kjær, Andreas
Supervisor Haxthausen, Anne Elisabeth (Software Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2008
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 denes the dynamic behaviour of an interlocking system. Also, the procedure specifies how to auto-generate confidence conditions for the generated transition system, formulated using Linear Temporal Logic (LTL). Finally, a tool for computing such a transition system and its associated confidence 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 dene 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 define 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.
Series IMM-M.Sc.-2008-68
Original PDF ep08_68_net.pdf (5.54 MB)
Admin Creation date: 2008-07-18    Update date: 2008-07-18    Source: dtu    ID: 221879    Original MXD