| ||||
| ||||
![]() Title:A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways Conference:AVOCS 2018 Tags:Compositional verification, ic3, Interlocking, nuxmv and Ocra 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. A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways ![]() A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways | ||||
Copyright © 2002 – 2025 EasyChair |