Formal Verification of Railway Interlockings: a Compositional Approach Based on a Library of Pre-verified Components

A railway interlocking system (RIS) is a safety critical system that allows to control the train traffic. Modern RIS rely on their software to guarantee the absence of dangerous situations leading to train collisions or derailments. For more than twenty years [5], researchers have worked on the development of formal method approaches to verify the absence of bugs in the RIS software and thereby improving the safety of the railway systems. A very popular formal verification approach is model checking. Practically, model checking of complex RIS remains hard due to the so-called state space explosion problem. Compositional verification can solve this issue by reducing a big network controlled by a RIS into a set of smaller sub-networks while still guaranteeing the safety of the composite. In this context, two different decomposition technique were proposed by the RobustRailS and the Louvain research groups. This article goes one step further and proposes a verification strategy based on the creation of a library made of typical re-usable pre-verified sub-networks (i.e., building blocks). During compositional verification, the goal is then to decompose the network into sub-networks that are in the library such that they do not need to be verified.