CSP Specification and Verification of a Relay-Based Railway Interlocking System

In previous work, we have presented a methodology for the specification and verification of relay-based Railway Interlocking Systems (RIS) based on their transient states. By using CSP as formal support, it is possible to use a model checker in order to analyse the safety of such critical systems as a way to improve their safety. However, this type of verification tends to consume a lot of computational resources, which hinders the use of this methodology for industrial systems. This work presents a proposal for a new methodology for the specification of RIS. In this work we rebuild the whole model by changing the notion of components, integrating them in the core of the model while keeping their interface visible to the end-user. In this context, it is possible to maintain the concepts of instantiating and combining components at the same time we reduce the number of components and states as a way to alleviate the time spent on model checking. Besides, we propose a new methodology of verification based on the decomposition of the model. Our new proposed approach supports the analysis of a bigger set of properties of these systems, like the analysis of the Ringbell Effect, short circuits, deadlocks, divergences, and components that cannot be activated at the same time. In order to evaluate our approach, a new industrial case study is modelled and analysed.