Formal verification of railway interlocking systems

Description

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. Safety of modern railway 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.

This PhD 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.

Jury members :

Prof. Charles Pecheur (UCLouvain), supervisor
Prof. Peter Van Roy (UCLouvain), chairperson
Prof. Axel Legay (UCLouvain), secretary
Prof. Gilles Perrouin (UNamur, Belgium)
Prof. Alessandro Fantechi (UNIFI, Italy)

Period	18 Dec 2019
Examinee	Christophe Limbrée
Examination held at	Université Catholique de Louvain (UCL)
Degree of Recognition	International