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.
Document type :
Conference papers
Complete list of metadatas

http://hal.univ-grenoble-alpes.fr/hal-02043174
Contributor : Yves Ledru <>
Submitted on : Wednesday, February 20, 2019 - 5:42:39 PM
Last modification on : Thursday, September 19, 2019 - 11:25:54 AM

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

62