Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum | International Journal on Software Tools for Technology Transfer
Skip to main content
Springer Nature Link
Log in

Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum

  • ABZ 2018
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

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 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. We also show how the Analyzer can be used to depict scenarios (and counter-examples) in a graphical notation that is logic-agnostic, making them understandable by stakeholders without expertise in formal specification.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9

Similar content being viewed by others

Notes

  1. http://haslab.github.io/Electrum/ertms_1C.ele.

  2. A third integrity issue in HL3 arises when trains report length changes; since they are treated exactly as integrity lost reports, for simplicity we encode only the latter in our model.

  3. http://haslab.github.io/Electrum/ertms_1C.thm.

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

  5. https://www.atelierb.eu.

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

References

  1. Abrial, J.: The B-Book—Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)

    MATH  Google Scholar 

  2. Abrial, J.: Modeling in Event-B—System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

  3. Abrial, J.: The ABZ-2018 case study with Event-B. In: ABZ, Volume 10817 of LNCS, pp. 322–337. Springer (2018)

  4. Abrial, J., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010)

    Article  Google Scholar 

  5. Arcaini, P., Jezek, P., Kofron, J.: Modelling the Hybrid ERTMS/ETCS Level 3 case study in S pin. In: ABZ, Volume 10817 of LNCS, pp. 277–291. Springer (2018)

  6. Couto, R., Campos, J.C., Macedo, N., Cunha, A.: Improving the visualization of Alloy instances. In: F-IDE@FLoC, Volume 284 of EPTCS, pp. 37–52 (2018)

  7. Cunha, A., Macedo, N.: Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum. In: ABZ, Volume 10817 of LNCS, pp. 307–321. Springer (2018)

  8. Dghaym, D., Poppleton, M., Snook, C.: Diagram-led formal modelling using iUML-B for Hybrid ERTMS Level 3. In: ABZ, Volume 10817 of LNCS, pp. 338–352. Springer (2018)

  9. EEIG ERTMS Users Group: Hybrid ERTMS/ETCS Level 3—principles. http://www.ertms.be/sites/default/files/2018-03/16E0421A_HL3.pdf 16E042, version 1A (2017)

  10. EEIG ERTMS Users Group: Hybrid ERTMS/ETCS Level 3—principles. https://ertms.be/sites/default/files/2018-07/16E0421C_HL3-clean.pdf 16E042, version 1C (2018)

  11. ERA, UNISIG, and EEIG ERTMS Users Group: Glossary of unisig terms and abbreviations. https://www.era.europa.eu/filebrowser/download/492_en SUBSET-023, issue 3.3.0 (2016)

  12. Fotso, S., Frappier, M., Laleau, R., Mammar, A.: Modeling the Hybrid ERTMS/ETCS Level 3 standard using a formal requirements engineering approach. In: ABZ, Volume 10817 of LNCS, pp. 262–276. Springer (2018)

  13. Hansen, D., Leuschel, M., Schneider, D., Krings, S., Körner, P., Naulin, T., Nayeri, N., Skowron, F.: Using a formal B model at runtime in a demonstration of the ETCS Hybrid Level 3 concept with real trains. In: ABZ, Volume 10817 of LNCS, pp. 292–306. Springer (2018)

  14. Hoang, T.S., Butler, M., Reichl, K.: The Hybrid ERTMS/ETCS Level 3 case study. In: ABZ, Volume 10817 of LNCS, pp. 251–261. Springer (2018)

  15. Holzmann, G.J.: The SPIN Model Checker-Primer and Reference Manual. Addison-Wesley, Boston (2004)

    Google Scholar 

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

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

    Google Scholar 

  18. Leuschel, M., Butler, M.: ProB: A model checker for B. In: FME, Volume 2805 of LNCS, pp. 855–874. Springer (2003)

  19. 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)

  20. Mammar, A., Frappier, M., Fotso, S., Laleau, R.: An Event-B model of the Hybrid ERTMS/ETCS Level 3 standard. In: ABZ, Volume 10817 of LNCS, pp. 353–366. Springer (2018)

  21. Mammar, A., Laleau, R.: On the use of domain and system knowledge modeling in goal-based Event-B specifications. In: ISoLA, Volume 9952 of LNCS, pp. 325–339 (2016)

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

  23. Snook, C.: iUML-B statemachines. In: Proceedings of the Rodin Workshop 2014, pp. 29–30. http://eprints.soton.ac.uk/365301/ (2014)

  24. Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)

    Article  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çã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.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Cunha, A., Macedo, N. Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum. Int J Softw Tools Technol Transfer 22, 281–296 (2020). https://doi.org/10.1007/s10009-019-00540-4

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-019-00540-4

Keywords

Search

Navigation