A Separation Of Concerns Approach For The Verified Modelling Of Railway Signalling Rules

This paper proposes a modelling approach for railway signalling rules. It adopts a separation of concerns approach similar to the one used in information systems security. It first models the effect of operations, and then specifies permissions involving the agent performing the action and the conditions that must be satisfied before performing this action. These models are expressed in SecureUML diagrams enhanced with B assertions. It then takes advantage of the B4MSecure tool to translate these diagrams into B machines. It finally relies on the ProB tool to verify the model using model-checking and animation. Model-checking assesses the reachability of desired states, and verifies the absence of accidents. The approach proceeds by introducing human errors, checking their consequences, and deploying counter-measures.