Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

A separation of concerns approach for the verified modelling of railway signalling rules

Abstract : 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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées
Contributeur : Yves Ledru <>
Soumis le : mercredi 20 février 2019 - 17:42:39
Dernière modification le : mercredi 5 août 2020 - 03:01:54




Yves Ledru, Akram Idani, Rahma Ben Ayed, Abderrahim Ait Wakrime, Philippe Bon. A separation of concerns approach for the verified modelling of railway signalling rules. RssRail 2019, International Conference on Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, Jun 2019, Lille, France. pp173-190, ⟨10.1007/978-3-030-18744-6_11⟩. ⟨hal-02043174⟩



Consultations de la notice