Skip to main content
SpringerLink
Log in
Book cover

International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z

ABZ 2018: Abstract State Machines, Alloy, B, TLA, VDM, and Z pp 307–321Cite as

Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10817))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    http://www.ertms.net/.

  2. 2.

    http://haslab.github.io/Electrum/ertms.ele.

  3. 3.

    http://haslab.github.io/Electrum/ertms.thm.

  4. 4.

    https://github.com/haslab/Electrum/wiki/ERTMS.

  5. 5.

    http://haslab.github.io/Electrum/ertms.als.

References

  1. Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)

    Article  Google Scholar 

  2. EEIG ERTMS Users Group: Hybrid ERTMS/ETCS Level 3 - Principles (2017)

    Google Scholar 

  3. INESC TEC, ONERA: Electrum Analyzer, v1.0. Available Under the MIT License (2018). https://github.com/haslab/Electrum/releases/tag/v1.0

  4. Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012). revised edn

    Google Scholar 

  5. Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: SIGSOFT FSE. pp. 373–383. ACM (2016)

    Google Scholar 

  6. Macedo, N., Cunha, A., Pessoa, E.: Exploiting partial knowledge for efficient model analysis. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 344–362. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_23

    Chapter  Google Scholar 

  7. Moreira, J.M., Cunha, A., Macedo, N.: An ORCID based synchronization framework for a national CRIS ecosystem. F1000Research 4(181) (2015)

    Google Scholar 

Download references

Acknowledgements

The authors would like to thank David Chemouil for the support provided during the model checking of the model. This work is financed by the ERDF - European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 and by National Funds through the Portuguese funding agency, FCT - Fundaç\(\tilde{a}o\) para a Ciência e a Tecnologia within project POCI-01-0145-FEDER-016826.

Author information

Authors and Affiliations

  1. INESC TEC & Universidade do Minho, Braga, Portugal

    Alcino Cunha & Nuno Macedo

Authors
  1. Alcino Cunha
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nuno Macedo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nuno Macedo .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Universität Ulm, Ulm, Germany

    Alexander Raschke

  3. University of Southampton, Southampton, United Kingdom

    Thai Son Hoang

  4. Thales Austria GmbH, Vienna, Austria

    Klaus Reichl

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Cunha, A., Macedo, N. (2018). Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-91271-4_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-91270-7

  • Online ISBN: 978-3-319-91271-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation