Formal verification of railway interlocking systems
(2019)
Files
thesisLimbreeChristophe.pdf
Restricted Access - Adobe PDF
- 1.16 MB
Details
- Authors
- Supervisors
- Pecheur, Charles
- Abstract
- The railways have been a vector of progress and economic growth since the 18th century. At the same time, the railways system designers have always focused on safety. In this context, a railway interlocking is a system that allows to control the train traffic in a station in a safe way. Modern railway interlocking are computer-based but guaranteeing the safety of their software components cannot be achieved exhaustively by means of classical testing methods. In computer science, model checking is a technique for automatically verifying the correctness properties of finite states systems. Practically, the behavior of a system represented by a model is examined exhaustively in order to detect unsafe states . This thesis proposes a model checking-based approach to verify safety properties on railway interlocking systems. The verification relies on a generic model that is extracted from the configuration of an interlocking (application data) and safety properties expressing the absence of unsafe situation (e.g., train collisions). A compositional verification technique extends this approach in order to verify larger stations and railway networks. Different algorithms and tools are elaborated in order to automate the verification process and tackle the state space explosion problem inherent to model checking. The verification approach is applied to real railway stations of the Belgian network.
- Affiliations
Citations
Limbrée, C. (2019). Formal verification of railway interlocking systems. https://hdl.handle.net/2078.5/169993