A separation of concerns approach for the verified modelling of railway signalling rules - Université Grenoble Alpes
Communication Dans Un Congrès Année : 2019

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

Résumé

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.
Fichier non déposé

Dates et versions

hal-02043174 , version 1 (20-02-2019)

Identifiants

Citer

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⟩
168 Consultations
0 Téléchargements

Altmetric

Partager

More