Model Checking Geographically Distributed Railway Control Systems



AbstractThe 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.
TypeMaster's thesis [Academic thesis]
Year2016
PublisherTechnical University of Denmark, Department of Applied Mathematics and Computer Science
AddressRichard Petersens Plads, Building 324, DK-2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk
SeriesDTU Compute M.Sc.-2016
NoteDTU supervisor: Associate professor Anne Elisabeth Haxthausen, and professor Alessandro Fantechi.
Electronic version(s)[pdf]
Publication linkhttp://www.compute.dtu.dk/English.aspx
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering