B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution

Abstract

In the railway signalling domain, a railway interlocking system (RIS) is responsible for controlling the movement of trains by allowing or denying their routing according to safety rules. Relay diagrams are a commonly used abstraction in order to model relay-based RIS, describing these systems by graph-like schemata that present the connections between electrical components. The verification of these diagrams regarding safety, however, is a challenging task, due to their complexity and the lack of tools for the automatic proof and animation. The analysis of relay diagrams by a specialist is the main method to verify the correctness and the safety of these systems. Nonetheless, human manual analysis is error prone. This paper presents an approach for formally specifying the behaviour of the systems described in relay diagrams in the B-method formal language. Considering that each relay has only two states, it is possible to describe the rules for the state evolution of a system by logical propositions. Furthermore, it is possible to use ProB in order to animate and model-check the specification.