Abstract—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.

Index Terms—Railway interlocking systems, relay diagrams, graph, b-method, framework.

Dalay Israel de Almeida Pereira, Philippe Bon, and Simon Collart-Dutilleul are with Univ Lille Nord de France, IFSTTAR, COSYS/ESTAS, 59650 Villeneuve d’Ascq, France. Matthieu Perin is with Institut de Recherche Technologique Railenium, F-59300 Famars, France.

Cite:Dalay Israel de Almeida Pereira, Matthieu Perin, Philippe Bon, Simon Collart-Dutilleul, "A Framework for the Formal Specification of Relay-Based Systems Based on a b-Method Graph Specification," International Journal of Computer and Electrical Engineering vol. 11, no. 1, pp. 11-19, 2019.