A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railway

Modern railway stations are controlled by computerized systems called interlockings. In fact the middle size and large size stations usually require to use several interlockings, then forming a network of interlockings. Much research propose to verify the safety properties of such systems by means of model checking. Our approach goes a step further and proposes a method to extend the verification process to a network of interlockings. This process is known as compositional verification. Each interlocking is seen as the component of a larger system (i.e., station) and interacts with its neighbours by means of interfaces. Our first contribution comes in the form of a catalogue of elements that constitute the interfaces (as used in the Belgian railways) and associated contracts. Each interface can then be bound to a formal contract allowing its verification by the ocra tool. Our second contribution comes in the form of an algorithm designed to split the topology controlled by a single interlocking into components. The verification of a large station can therefore be achieved by verifying its constituting components and their interaction thereby tackling the state space explosion problem while providing guarantees on the whole interlocking