Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach | International Journal on Software Tools for Technology Transfer Skip to main content
Springer Nature Link
Log in

Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach

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

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

This paper presents a specification of the hybrid ERTMS/ETCS level 3 standard in the framework of the case study proposed for ABZ2018. The specification is based on methods and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requirements. The requirements are specified with SysML/KAOS goal diagrams and are automatically translated into B System specifications, in order to obtain the architecture of the formal specification. Domain properties are specified by ontologies with the SysML/KAOS domain modeling language, based on OWL and PLIB. Their automatic translation completes the structural part of the formal specification. The only part of the specification that must be manually completed is the body of events. The construction is incremental, based on refinement mechanisms that exist within the involved methods. Regarding the case study, the formal specification includes seven refinement levels and all proofs have been discharged under the Rodin platform.

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. University Paris Est Créteil, France; University of Sherbrooke, Canada; Télécom SudParis, France; Institut Mines-Telecom Brest, France

  2. THALES, France; ClearSy Systems Engineering, France; Openflexo, France

  3. Montreal is the second-largest city in Canada and the largest city in Québec

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: Butler et al. [11], pp. 322–337

  4. ANR-14-CE28-0009: Formose ANR project (2017)

  5. Arcaini, P., Jezek, P., Kofron, J.: Modelling the hybrid ERTMS/ETCS level 3 case study in Spin. In: Butler et al. [11], pp. 277–291

  6. Arora, C., Sabetzadeh, M., Briand, L.C.: An empirical study on the potential usefulness of domain models for completeness checking of requirements. Empir. Softw. Eng. 24(4), 2509–2539. https://doi.org/10.1007/s10664-019-09693-x

  7. Bjrner, D.: Domain analysis and description principles, techniques, and modelling languages. ACM Trans. Softw. Eng. Methodol. 28(2), 8:1–8:67 (2019). https://doi.org/10.1145/3295738

  8. Broy, M.: Domain modeling and domain engineering: key tasks in requirements engineering. In: Münch, J., Schmid, K. (eds.) Perspectives on the Future of Software Engineering. Essays in Honor of Dieter Rombach, pp. 15–30. Springer. Berlin (2013)

  9. Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The electrum analyzer: model checking relational first-order temporal specifications. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3–7, 2018, pp. 884–887. ACM (2018)

  10. Butler, M.J., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.): Rigorous Development of Complex Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 4157. Springer, Berlin (2006)

  11. Butler, M.J., Raschke, A., Hoang, T.S., Reichl, K. (eds.): Abstract State Machines, Alloy, B, TLA, VDM, and Z–6th International Conference, ABZ 2018, Southampton, UK, June 5–8, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10817. Springer (2018)

  12. Clancy, T.: The standish group CHAOS report. Project Smart pp. 8–9 (2014)

  13. ClearSy: Atelier B: B System (2014). http://clearsy.com/. Accessed Oct 2019

  14. Cunha, A., Macedo, N.: Validating the hybrid ERTMS/ETCS level 3 concept with electrum. In: Butler et al. [11], pp. 307–321

  15. Deploy Project: Rodin Atelier B Provers Plug-in (2017). https://www3.hhu.de/stups/handbook/rodin/current/html/atelier_b_provers.html. Accessed Oct 2019

  16. Dghaym, D., Poppleton, M., Snook, C.F.: Diagram-led formal modelling using iUML-B for hybrid ERTMS level 3. In: Butler et al. [11], pp. 338–352

  17. de Almeida Falbo, R., Guizzardi, G., Duarte, K.C.: An ontological approach to domain engineering. In: Proceedings of the 14th International Conference on Software Engineering and Knowledge Engineering, SEKE 2002, Ischia, Italy, July 15–19, 2002. pp. 351–358. ACM (2002). https://doi.org/10.1145/568760.568822

  18. EEIG ERTMS Users Group: Hybrid ERTMS/ETCS level 3: Principles. Ref. 16E042 Version 1C (2018)

  19. Fotso, S.J.T., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. In: Butler et al. [11], pp. 262–276

  20. Fotso, S.J.T., Mammar, A., Laleau, R., Frappier, M.: Event-B expression and verification of translation rules between SysML/KAOS domain models and B System specifications. In: Butler et al. [11], pp. 55–70

  21. Hacid, K., Ameur, Y.A.: Strengthening MDE and formal design models by references to domain ontologies. A model annotation based approach. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques—7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9952, pp. 340–357 (2016). https://doi.org/10.1007/978-3-319-47166-2_24

  22. 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: Butler et al. [11], pp. 292–306

  23. Hause, M., et al.: The SysML modelling language. In: Fifteenth European Systems Engineering Conference. vol. 9. Citeseer (2006)

  24. Hoang, T.S., Butler, M.J., Reichl, K.: The hybrid ERTMS/ETCS level 3 case study. In: Butler et al. [11], pp. 251–261

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

    Google Scholar 

  26. Jackson, D.: Software Abstractions—Logic, Language, and Analysis. MIT Press (2006). http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=10928. Accessed Oct 2019

  27. Jackson, M.A.: Software Requirements and Specifications–A Lexicon of Practice. Principles and Prejudices. Addison-Wesley, Boston (1995)

    Google Scholar 

  28. Jetbrains: Jetbrains mps (2017). https://www.jetbrains.com/mps/

  29. Laleau, R., Semmak, F., Matoussi, A., Petit, D., Hammad, A., Tatibouet, B.: A first attempt to combine SysML requirements diagrams and B. Innov. Syst. Softw. Eng. 6(1–2), 47–54 (2010)

    Article  Google Scholar 

  30. Lecomte, T., Déharbe, D., Prun, É., Mottin, E.: Applying a formal method in industry: a 25-year trajectory. In: Formal Methods: Foundations and Applications—20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29–December 1, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10623, pp. 70–87. Springer (2017)

  31. Lee, D.G., Suh, N.P.: Axiomatic design and fabrication of composite structures-applications in robots, machine tools, and automobiles, p. 732. Oxford University Press, Oxford (2005)

    Google Scholar 

  32. Leuschel, M., Butler, M.J.: Prob: A Model Checker for B. Lecture Notes in Computer Science, vol. 2805, pp. 855–874. Springer, Berlin (2003)

  33. Mammar, A., Frappier, M., Fotso, S.J.T., Laleau, R.: An Event-B model of the hybrid ERTMS/ETCS level 3 standard. In: Butler et al. [11], pp. 353–366

  34. Mammar, A., Laleau, R.: On the use of domain and system knowledge modeling in goal-based Event-B specifications. In: ISoLA 2016, Lecture Notes in Computer Science. pp. 325–339. Springer

  35. Matoussi, A., Gervais, F., Laleau, R.: A goal-based approach to guide the design of an abstract Event-B specification. In: Perseil, I., Breitman, K.K., Sterritt, R. (eds.) 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011, Las Vegas, Nevada, USA, 27–29 April 2011. pp. 139–148

  36. Micouin, P., Fabre, L., Becquet, R., Paper, P., Razafimahefa, T., Guérin, F.: Property model methodology: a landing gear operational use case. INCOSE Int. Symp. 28(1), 321–336 (2018). https://doi.org/10.1002/j.2334-5837.2018.00484.x

    Article  Google Scholar 

  37. Nicola, F., van Houten, H., Arenas, L., Bartholomeus, M.: ERTMS level 3: the game-changer. IRSE News View 232, 2–9 (2017)

    Google Scholar 

  38. Nuseibeh, B.: Weaving together requirements and architectures. Computer 34(3), 115–119 (2001)

    Article  Google Scholar 

  39. Openflexo: Openflexo project (2019). http://www.openflexo.org. Accessed Oct 2019

  40. Openflexo: Openflexo sysml/kaos tool (2019). https://downloads.openflexo.org/Formose/. Accessed Oct 2019

  41. Pierra, G.: The PLIB ontology-based approach to data integration. In: IFIP 18th World Computer Congress. IFIP, vol. 156, pp. 13–18. Kluwer/Springer (2004)

  42. Roques, A.: PlantUML: open-source tool that uses simple textual descriptions to draw UML diagrams. http://plantuml.sourceforge.net/index.html (2015). Accessed Oct 2019

  43. Bechhofer, S.: Web ontology language (OWL). In: Liu, L., Özsu, M.T. (eds.) Encyclopedia of Database Systems, 2nd edn. Springer, New York (2018)

    Google Scholar 

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

    Article  Google Scholar 

  45. SYSTEREL: Rodin SMT Solvers Plug-in (2017). http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in. Accessed Oct 2019

  46. SysML/KAOS requirements modeling of a road transportation system (2018) https://github.com/stuenofotso/SysML_KAOS_Domain_Model_Parser/tree/master/Bonaventure_project

  47. Tueno, S., Frappier, M., Laleau, R., Mammar, A., Barradas, H.R.: The Generic SysML/KAOS Domain Metamodel. ArXiv e-prints, cs.SE (2018). arXiv:1811.04732

  48. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Towards using ontologies for domain modeling within the SysML/KAOS approach. In: IEEE Proceedings of MoDRE Workshop, 25th IEEE International Requirements Engineering Conference

  49. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: The SysML/KAOS Domain Modeling Approach. ArXiv e-prints, cs.SE (2017). arXiv:1710.00903

  50. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: The SysML/KAOS Domain Modeling Language (Tool and Case Studies) (2017). https://github.com/stuenofotso/SysML_KAOS_Domain_Model_Parser/tree/master. Accessed Oct 2019

  51. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: SysML/KAOS Approach on the Hybrid ERTMS/ETCS Level 3 case study (2018). https://github.com/stuenofotso/SysML_KAOS_Domain_Model_Parser/tree/master/ABZ18_ERTMS. Accessed Oct 2019

  52. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: SysML/KAOS Domain Modeling Tool (2018). https://github.com/stuenofotso/SysML_KAOS_Domain_Model_Parser. Accessed Oct 2019

  53. van Lamsweerde, A.: Requirements Engineering-From System Goals to UML Models to Software Specifications. Wiley, Hoboken (2009)

    Google Scholar 

Download references

Acknowledgements

This work is carried out within the framework of the FORMOSE project [4] funded by the French National Research Agency (ANR). It is also partly supported by the Natural Sciences and Engineering Research Council of Canada (NSERC).

Author information

Authors and Affiliations

  1. GRIL Université de Sherbrooke, Sherbrooke, QC, J1K 2R1, Canada

    Steve Jeffrey Tueno Fotso & Marc Frappier

  2. LACL Université Paris-Est Créteil, 94010, Créteil, France

    Régine Laleau

  3. SAMOVAR-CNRS Télécom SudParis, 91000, Evry, France

    Amel Mammar

Authors
  1. Steve Jeffrey Tueno Fotso
    View author publications

    You can also search for this author inPubMed Google Scholar

  2. Marc Frappier
    View author publications

    You can also search for this author inPubMed Google Scholar

  3. Régine Laleau
    View author publications

    You can also search for this author inPubMed Google Scholar

  4. Amel Mammar
    View author publications

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence to Steve Jeffrey Tueno Fotso.

Additional information

Publisher's Note

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

French National Research Agency (ANR).

Natural Sciences and Engineering Research Council of Canada (NSERC)

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Tueno Fotso, S.J., Frappier, M., Laleau, R. et al. Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. Int J Softw Tools Technol Transfer 22, 349–363 (2020). https://doi.org/10.1007/s10009-019-00542-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-019-00542-2

Keywords