Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum

Alcino Cunha, Nuno Macedo
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

This paper reports on the development of a formal model for the Hybrid ERTMS/ETCS Level 3 concept in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic operators. We show how Electrum and its Analyzer can be used to perform scenario exploration to validate this model, namely to check that all the example operational scenarios described in the reference document are admissible, and to reason about expected safety properties, which can be easily specified and model checked for arbitrary track configurations. The Analyzer depicts scenarios (and counter-examples) in a graphical notation that is logic-agnostic, making them understandable for stakeholders without expertise in formal specification.

Document

Reference

% BibTex
@inproceedings{cunha2018validating,
  title={Validating the hybrid ERTMS/ETCS level 3 concept with electrum},
  author={Cunha, Alcino and Macedo, Nuno},
  booktitle={International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z},
  pages={307--321},
  year={2018},
  organization={Springer}
}

Sources

  • Used formal method: Electrum

  • Resources and tools: Electrum

    For more information, please contact the authors

ABZ'18

Related