Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 3/2020

10.10.2019 | ABZ 2018

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

verfasst von: Steve Jeffrey Tueno Fotso, Marc Frappier, Régine Laleau, Amel Mammar

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 3/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Vorheriger Artikel A formal refinement-based analysis of the hybrid ERTMS/ETCS level 3 standard

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
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
 
Literatur
1.
Abrial, J.: The B-book–Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)MATH
2.
Abrial, J.: Modeling in Event-B–System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRef
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.
7.
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.
14.
Cunha, A., Macedo, N.: Validating the hybrid ERTMS/ETCS level 3 concept with electrum. In: Butler et al. [11], pp. 307–321
15.
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)
26.
27.
Jackson, M.A.: Software Requirements and Specifications–A Lexicon of Practice. Principles and Prejudices. Addison-Wesley, Boston (1995)
28.
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)CrossRef
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)
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.
37.
Nicola, F., van Houten, H., Arenas, L., Bartholomeus, M.: ERTMS level 3: the game-changer. IRSE News View 232, 2–9 (2017)
38.
Nuseibeh, B.: Weaving together requirements and architectures. Computer 34(3), 115–119 (2001)CrossRef
39.
40.
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.
43.
Bechhofer, S.: Web ontology language (OWL). In: Liu, L., Özsu, M.T. (eds.) Encyclopedia of Database Systems, 2nd edn. Springer, New York (2018)
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)CrossRef
45.
46.
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.
51.
52.
53.
van Lamsweerde, A.: Requirements Engineering-From System Goals to UML Models to Software Specifications. Wiley, Hoboken (2009)
Metadaten
Titel
Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach
verfasst von
Steve Jeffrey Tueno Fotso
Marc Frappier
Régine Laleau
Amel Mammar
Publikationsdatum
10.10.2019
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 3/2020
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-019-00542-2

Weitere Artikel der Ausgabe 3/2020

International Journal on Software Tools for Technology Transfer 3/2020 Zur Ausgabe

ABZ 2018

The ABZ-2018 case study with Event-B

ABZ 2018

Validation of the Hybrid ERTMS/ETCS Level 3 using Spin

ABZ 2018

A formal refinement-based analysis of the hybrid ERTMS/ETCS level 3 standard

ABZ 2018

Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model

Introduction

Introduction to special section on the ABZ 2018 case study: Hybrid ERTMS/ETCS Level 3

ABZ 2018

Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B