Diagram-Led Formal Modelling Using iUML-B for Hybrid ERTMS Level 3

Dana Dghaym, Michael Poppleton, Colin F. Snook
Case Study Digital Printed Abstract View Cite Source
Type
Conference paper
Publication
6th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'18)

Abstract

We demonstrate diagrammatic Event-B formal modelling of a hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. We perform a refinement-based formal development and verification of the no-collision safety requirement. The development reveals limitations in the specification and identifies assumptions on the environment. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method using the UMLlike state and class diagrams of iUML-B. We suggest enhancements to the existing iUML-B method that would have benefitted this development.

Document

Reference

% BibTex
@inproceedings{dghaym2018diagram,
  title={Diagram-led formal modelling using iUML-B for hybrid ERTMS level 3},
  author={Dghaym, Dana and Poppleton, Michael and Snook, Colin},
  booktitle={International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z},
  pages={338--352},
  year={2018},
  organization={Springer}
}

Sources

  • Used formal method: Event-B and iUML-B

    For more information, please contact the authors

ABZ'18

Related