||Verication of Safety Properties for Relay Interlocking Systems
||Eriksen, Louise Elmose
||Haxthausen, Anne Elisabeth (Software Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
||Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
||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.
||Technical University of Denmark (DTU) : Kgs. Lyngby, Denmark
Creation date: 2010-09-10
Update date: 2010-09-10