Formal Analysis and Monitoring of Legacy Safety-Critical Interlocking Systems with the Use of Certified Industrial Tools

Although Formal Methods have been used for decades in the development of industrial critical systems, there are still many products that do not use this technology. The use of Formal Methods in such a context is generally highly recommended, but not mandatory, as other technologies may be used as support to certify the safety of the systems. Relay-based railway interlocking systems, for instance, are legacy systems used in the majority of railway installations and whose safety has been attested through their use for decades. Their maintenance, however, requires analysis to avoid losing their safety features. In previous papers, we have presented the CLEARSY Safety Platform (CSSP) and how it can be used to analyse and replace these legacy interlocking systems in a safety-proved manner using certified industrial tools. In this paper, we extend this discussion to present how the CSSP can be used to monitor the legacy relay-based RIS to improve their safety during their execution. The strategy is to describe the system safety properties using logic and then implement it in the CSSP, which in turn is responsible for monitoring the system components to ensure its correct functioning and raise flags when an unsafe state is found. The benefits of using our approach in industry are discussed as we present how it can be applied in two industrial case studies.