Model Checking Geographically Distributed Railway Control Systems |
|
| Abstract | The goal of this project is to investigate model checking as a verification method for analysis of distributed railway control systems wrt. safety.
To drive this investigation an engineering concept of a distributed railway interlocking system is conceived and described. The concept is distilled into an abstract generic model in a model checking language. Furthermore is a tool developed to assist in generating concrete models from the generic model, that are both valid and constrained to help reduce the state space to be searched when model checking the concrete model instances.
The outcome of the project is not only a verified engineering concept, an abstract model of the concept and a tool to assist in exploring concrete instances an abstract model, -but also an example of how an engineering concept can be modeled as an abstract model and verified through model checking. |
| Type | Master's thesis [Academic thesis] |
| Year | 2016 |
| Publisher | Technical University of Denmark, Department of Applied Mathematics and Computer Science |
| Address | Richard Petersens Plads, Building 324, DK-2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk |
| Series | DTU Compute M.Sc.-2016 |
| Note | DTU supervisor: Associate professor Anne Elisabeth Haxthausen, and professor Alessandro Fantechi. |
| Electronic version(s) | [pdf] |
| Publication link | http://www.compute.dtu.dk/English.aspx |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |