Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B

Dghaym, Dana, Dalvandi, Mohammadsadegh, Poppleton, Michael and Snook, Colin (2019) Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B International Journal on Software Tools for Technology Transfer.

Preview

Text Formalising the Hybrid ERTMS Level 3 specification - VoR (OA).pdf - Version of Record Available under License Creative Commons Attribution. Download (1MB) | Preview

Abstract

We demonstrate refinement-based formal development of the hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. Our approach uses iUML-B diagrams as a front end to the Event-B modelling language. We use abstraction to verify the principle of movement authority before gradually developing the details of the Virtual Block Detector component in subsequent refinements, thus verifying that it preserves the safety properties. We animate the refined models to demonstrate their validity using the scenarios from the Hybrid ERTMS Level 3 (HLIII) specification. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method based on the state and class diagrams of iUML-B. The component and control flow architectures of the application, its environment and interacting systems emerge through the layered refinement process. The runtime semantics of the specification’s state-machine behaviour are modelled in the final refinements. We discuss how the model could be used to generate an implementation using code generation tools and techniques.

Item Type:	Article
Divisions :	Faculty of Engineering and Physical Sciences > Computer Science
Authors :	Name Email ORCID Dghaym, Dana Dalvandi, Mohammadsadegh m.dalvandi@surrey.ac.uk Poppleton, Michael Snook, Colin
Date :	12 November 2019
Funders :	European Union's Horizon 2020
DOI :	10.1007/s10009-019-00548-w
Grant Title :	ECSEL Joint Undertaking
Copyright Disclaimer :	© The Author(s) 2019. Open Access. This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
Uncontrolled Keywords :	ERTMS; Event-B; iUML-B; Refinement; Validation
Depositing User :	Clive Harris
Date Deposited :	09 Dec 2019 13:02
Last Modified :	09 Dec 2019 13:02
URI:	http://epubs.surrey.ac.uk/id/eprint/853248

Actions (login required)

View Item

Downloads