CSP specification and verification of relay-based railway interlocking systems
Dalay Israel de Almeida Pereira, Marcel Oliveira, P. E. R. Bezerra, Philippe Bon, Simon Collart-Dutilleul · Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing · 2022
Despite the existence of new technologies, relay-based electrical circuits are still used in the majority of the Railway Interlocking Systems installations. Due to their safety-critical aspects, these systems must be safety-proved before their implementation and use. Although the railway standards strongly recommend the use of Formal Methods for the specification and proof of these systems, the literature is scarce in this regard. This article presents the results of using a process-based language, CSP, for the specification of the relay-based Railway Interlocking Systems. Differently from other approaches, our methodology allows the specification of transient states. As a result, it is possible to perform a stronger verification, including an investigation about the existence of state succession cycles, which are dangerous in such systems. An electrical circuit example with such problem is discussed and specified, demonstrating the need of our methodology for the safety proof of these systems.