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.
A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railway
Electronic Communications of the EASST ; 76 , Electronic Communications of the EASST, Vol. 76 (2019): Automated Verification of Critical Systems 2018 (AVoCS 2018)
2019
Aufsatz (Zeitschrift)
Elektronische Ressource
Englisch
Compositional Verification of Railway Interlockings: Comparison of Two Methods
British Library Conference Proceedings | 2022
|Simulating and analyzing railway interlockings in ExSpect
TIBKAT | 1994
|Electric railway traction. Part 4: Signalling and interlockings
IET Digital Library Archive | 1995
|Safety assurance of configuration data for railway signal interlockings
IET Digital Library Archive | 2006
|