FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways

Authors: Christophe Limbrée and Charles Pecheur

Paper Information

Title:A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
Authors:Christophe Limbrée and Charles Pecheur
Proceedings:AVOCS Pre-proceedings
Editors: David Pichardie and Mihaela Sighireanu
Keywords:Interlocking, Compositional verification, Ocra, ic3, nuxmv
Abstract:

ABSTRACT. Modern railway stations are controlled by computerized systems called interlockings. In fact the middle size and large size stations usually required to use several interlockings then forming a network. Many researches propose to verify the safety properties of such system by mean of model checking. Our approach goes a step further and proposes a method to extend the verification process to interconnected 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 mean of interfaces. Our first contribution comes in the form of a catalogue of formal definitions covering all the interfaces used by the Belgian Railways. Each interface can then be bound to a formal contract allowing its verification by the ocra tool. Our second contribution is to propose an algorithm able to split the topology controlled by a single interlocking into components. This allows to reduce the size of the model to be verified thereby reducing the state space explosion while providing guarantees on the whole interlocking.

Pages:17
Talk:Jul 19 12:00 (Session 132A: AVoCS Regular Papers 3)
Paper: