nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Modelling and Analysing ERTMS Hybrid Level 3 with the mCRL2 Toolset

verfasst von : Maarten Bartholomeus, Bas Luttik, Tim Willemse

Erschienen in: Formal Methods for Industrial Critical Systems

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

ERTMS Hybrid Level 3 is a recent proposal for a train control system specification that serves to increase the capacity of the railway network by allowing multiple trains with an integrity monitoring system and a GSM-R connection to the trackside on a single section. In this paper we model the principles of ERTMS Hybrid Level 3 in the \(\mathrm {mCRL2}\) process algebra and perform an analysis with its associated toolset. Our analysis has resulted in suggestions for improvement of the principles that will be taken into account in the next version of the specification.

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 Formal Verification of a Programmable Hypersurface

Nächstes Kapitel Progress Checking for Dummies

The \(\mathrm {mCRL2}\) code is distributed with the \(\mathrm {mCRL2}\) toolset (git commit 2e671cb), which is available from https://www.mcrl2.org.

Berger, U., James, P., Lawrence, A., Roggenbach, M., Seisenberger, M.: Verification of the European rail traffic management system in real-time maude. Sci. Comput. Program. 154, 61–88 (2018)CrossRef

Canonico, R., Marrone, S., Nardone, R., Vittorini, V.: A framework to evaluate 5G networks for smart and fail-safe communications in ERTMS/ETCS. In: Fantechi, A., Lecomte, T., Romanovsky, A.B. (eds.) RSSRail 2017. LNCS, vol. 10598, pp. 34–50. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68499-4_3CrossRef

Cimatti, A.: Formal verification and validation of ERTMS industrial railway train spacing system. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378–393. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_29CrossRef

Cranen, S., Luttik, B., Willemse, T.A.C.: Evidence for fixpoint logic. In: CSL, vol. 41. LIPIcs, pp. 78–93. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)

Cunha, A., Macedo, N.: Validating the hybrid ERTMS/ETCS level 3 concept with electrum. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 307–321. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_21CrossRef

EEIG ERTMS Users Group. Hybrid ERTMS/ETCS Level 3. Ref: 16E045, Version: 1A, 14 July 2017. http://users.ecs.soton.ac.uk/asf08r/ABZ2018/16E0421A_HL3.pdf

Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167–183. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05032-4_13CrossRef

Furness, N., van Houten, H., Arenas, L., Bartholomeus, M.: ERTMS Level 3: the game-changer. IRSE News 232, 2–9 (2017)

Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press (2014)

10.

Mammar, A., Frappier, M., Tueno Fotso, S.J., Laleau, R.: An Event-B model of the hybrid ERTMS/ETCS level 3 standard. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 353–366. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_24CrossRef

11.

Platzer, A., Quesel, J.-D.: European train control system: a case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 246–265. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10373-5_13CrossRef

12.

Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133, 91–115 (2017)CrossRef

13.

Wesselink, W., Willemse, T.A.C.: Evidence extraction from Parameterised Boolean Equation Systems. In: Benzmüller, C., Otten, J. (eds.) ARQNL, vol. 2095. CEUR Workshop Proceedings, pp. 86–100 (2018). CEUR-WS.org

Titel: Modelling and Analysing ERTMS Hybrid Level 3 with the mCRL2 Toolset
verfasst von: Maarten Bartholomeus
Bas Luttik
Tim Willemse
Verlag: Springer International Publishing
Buch: Formal Methods for Industrial Critical Systems
Print ISBN: 978-3-030-00243-5

Electronic ISBN: 978-3-030-00244-2

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-00244-2_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"