A Framework for the Formal Specification of Relay-Based Systems Based on a b-Method Graph Specification
Univ Lille Nord de France, IFSTTAR, COSYS/ESTAS, 59650 Villeneuve d’Ascq, France., Dalay Israel de Almeida Pereira, Matthieu Perin, Philippe Bon, Simon Collart-Dutilleul · International Journal of Computer and Electrical Engineering · 2019
A railway interlocking system is one example of a critical system, and, therefore, it must have a high level of reliability in order to avoid problems that may result on the loss of people's lives.However, many railway systems are still specified using historical relay-based diagrams, whose analysis are made by human inspection, which is error prone.Relay-based diagrams are specified by nodes and cables in a graphical manner, which resemble undirected graphs.This paper presents a framework for the specification of relay diagrams in a formal language, B-method, based on the specification of a graph and its properties.The use of a formal language allows one to prove the correctness of these railway interlocking systems regarding structural properties.This framework has been evaluated by the specification of a case study.