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
Erschienen in:
ABZ Languages and Tools in Industrial-Scale Application Kapitel lesen Erstes Kapitel lesen

2018 | OriginalPaper | Buchkapitel

Diagram-Led Formal Modelling Using iUML-B for Hybrid ERTMS Level 3

verfasst von : Dana Dghaym, Michael Poppleton, Colin Snook

Erschienen in: Abstract State Machines, Alloy, B, TLA, VDM, and Z

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We demonstrate diagrammatic Event-B formal modelling of a hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. We perform a refinement-based formal development and verification of the no-collision safety requirement. The development reveals limitations in the specification and identifies assumptions on the environment. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method using the UML-like state and class diagrams of iUML-B. We suggest enhancements to the existing iUML-B method that would have benefitted this development.

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
Vorheriges Kapitel The ABZ-2018 Case Study with Event-B
Nächstes Kapitel An Event-B Model of the Hybrid ERTMS/ETCS Level 3 Standard
Fußnoten
2
Controlled and trusted (trains) are terms that we have introduced, they are not terms from the specification.
 
3
Note that class invariants are implicitly quantified over instances of the class, hence the antecedent https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-91271-4_23/468119_1_En_23_IEq43_HTML.gif is added automatically.
 
Literatur
1.
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRef
2.
Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRef
3.
Butler, M., Colley, J., Edmunds, A., Snook, C., Evans, N., Grant, N., Marshall, H.: Modelling and refinement in CODA. In: Refine@IFM 2013, EPTCS, Turku, Finland, vol. 115, pp. 36–51 (2013)CrossRef
4.
Butler, M., Dghaym, D., Fischer, T., Hoang, T., Reichl, K., Snook, C., Tummeltshammer, P.: Formal modelling techniques for efficient development of railway control products. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2017. LNCS, vol. 10598, pp. 71–86. Springer, Heidelberg (2017). https://​doi.​org/​10.​1007/​978-3-319-68499-4_​5CrossRef
5.
Fischer, T., Snook, C., Hoang, T.: Formal model validation through acceptance tests. Technical report, University of Southampton, UK, March 2018
6.
Furness, N., van Houten, H., Arenas, L., Bartholomeus, M.: ERTMS Level 3: the game-changer. IRSE News 232, 2–9 (2017)
7.
Fürst, A., Hoang, T.S., Basin, D., Sato, N., Miyazaki, K.: Large-scale system development using Abstract Data Types and refinement. Sci. Comput. Program. 131, 59–75 (2016)CrossRef
8.
9.
10.
11.
Hoang, T.S., Snook, C., Ladenberger, L., Butler, M.: Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion studio, and co-simulation. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 360–375. Springer, Cham (2016). https://​doi.​org/​10.​1007/​978-3-319-33600-8_​31CrossRef
12.
Krenn, W., Schlick, R., Tiran, S., Aichernig, B., Jobstl, E., Brandl, H.: MoMut::UML model-based mutation testing for UML. In: 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST), pp. 1–8 (2015)
13.
14.
Said, M., Butler, M., Snook, C.: A method of refinement in UML-B. Softw. Syst. Model. 14(4), 1557–1580 (2015)CrossRef
15.
Salehi, A., Butler, M., Rezazadeh, A.: Language and tool support for event refinement structures in Event-B. Formal Asp. Comput. 27(3), 499–523 (2015)MathSciNetCrossRef
16.
17.
Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)CrossRef
Metadaten
Titel
Diagram-Led Formal Modelling Using iUML-B for Hybrid ERTMS Level 3
verfasst von
Dana Dghaym
Michael Poppleton
Colin Snook
Copyright-Jahr
2018
Buch
Abstract State Machines, Alloy, B, TLA, VDM, and Z

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

Electronic ISBN: 978-3-319-91271-4

Copyright-Jahr: 2018

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