@MASTERSTHESIS\{IMM2005-03966,
    author       = "M. S. Madsen and M. M. B{\ae}k",
    title        = "Modelling a Distributed Railway Control System",
    year         = "2005",
    keywords     = "formal specification, railway lines, control systems, {JAVA,} {XML,} simulation, safety, {RAISE}",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Assoc. Prof. Anne Haxthausen",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/3966-full.html",
    abstract     = "This thesis concerns the development of a distributed control system for a simple railway line. Control systems exist to ensure safety of trains by preventing events like derailments and collisions.

Formal development methods and specification languages can increase the correctness of software systems. These methods are essential to the development of safety critical systems where human lives are at stake. Therefore a formal method is applied to the development in this thesis.

A formal model, using the {RAISE} specification language (RSL), of a distributed control system for railway lines is developed. The formal specification language is used to ensure correctness and safety of the system. The model is separated in modules so a clear separation of the static, dynamics, and control properties is obtained.

The model is constructed with provability of safety in mind. Proof obligations are sketched and the theory of how to prove safety properties in the model is briefly described. A single informal proof of one proof obligation is performed.

The model is refined through a number of steps. This is done by first specifying an abstract applicative model which then is refined to a concrete version. The concrete model is transformed to an imperative version.

The imperative model is implemented in the {JAVA} programming language. The result is a generic simulator which can take a configuration (a railway line structure) as input and simulate trains operating on this line. A configuration editor is developed to ease the construction of new railway configurations.

The developed model is fairly complex compared to other formally developed models since it also concerns time issues. These complicate the model by adding a considerably larger state space to the model. Events like collisions and braking distances become major issues in the development."
}