Beta 1

Title Verication of Safety Properties for Relay Interlocking Systems
Author Eriksen, Louise Elmose
Pedersen, Boe
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 2010
Abstract Many people travel by train, and thus rely on trains being a safe means of transportation. BaneDanmark, who is responsible for most of the Danish railway network, uses relay based interlocking systems to ensure that no trains collide and no trains derail. The goal of this project is to develop a method for deriving safety properties from a given relay interlocking system and for specifying how the interlocking system can be verified in relation to the safety properties. In order to derive and formalise safety properties it has been decided that a model of relay interlocking systems should be developed. The model has been specified in the formal specification language Maude which additionally can be used for model verification as it provides a model checking tool. LTL (Linear Temporal Logic) is used to formalise the safety properties, thus enabling that the safety properties can be verified using the Maude model checking tool. The behaviour of interlocking systems as well as the methods for deriving safety properties from a model and verifying a given model in relation to these safety properties, has been specified in a generic way, to support any given interlocking system. Additionally, some tools have been developed to ease the specification of a model given the documentation of an interlocking system. The method has been successfully applied to a number of smaller interlocking systems and partly to the more complex system of Stenstrup station.
Imprint Technical University of Denmark (DTU) : Kgs. Lyngby, Denmark
Series IMM-M.Sc.-2010-57
Original PDF ep10_57_net.pdf (3.15 MB)
Admin Creation date: 2010-09-10    Update date: 2010-09-10    Source: dtu    ID: 266717    Original MXD