ICTEAM - Public Thesis defense

Formal verification of railway interlocking systems by Christophe LIMBREE

Pour l’obtention du grade de Docteur en sciences de l’ingénieur et technologie

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 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)

Télécharger l'annonce