nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin

verfasst von : Paolo Arcaini, Pavel Ježek, Jan Kofroň

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

KI-gestützte Suche

Aus

Abstract

The Spin model checker has been successfully applied to the modelling, validation, and verification of different safety-critical systems. In this paper, we model and validate the Hybrid ERTMS/ETCS Level 3 Case Study using Spin; in particular, we show the assumptions we made to keep the state space limited, and present the problems and ambiguities that arose during the modelling. Although Spin offers several advantages in terms of validation and verification facilities, its modelling language Promela is limited if compared to higher level notations of other formal methods. Therefore, we discuss the advantages and disadvantages of using the tool, and how it could be improved in terms of modelling facilities.

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 Modeling the Hybrid ERTMS/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach

Nächstes Kapitel Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains

Actually, two trains can be in a TTD if they are operating in on-sight mode in which the drivers are fully responsible for the train movement; this setting, however, is an exceptional case that is not a part of normal operational mode.

Note that the case study assignment [11] considers movement only in one direction, i.e., no backward moves.

Formulations in [6] such as “A value between 5–10 s would seem to be practical” and “...this timer could be set to a value of at least 27 s ...” are not of much use.

The simulation output of the assertion violation can be found at http://d3s.mff.cuni.cz/~kofron/abz18casestudy.html.

Note that in Spin, we sometimes need to perform multiple steps in order to model a single step of a scenario reported in the requirements document; therefore, the step numbers (6 and 7) reported in the figure are different from the corresponding steps of the requirements document (steps 3 and 4).

http://spinroot.com/spin/success.html.

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

Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 61–74. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_6CrossRef

Arvind, D.N., Katelman, M.: Getting formal verification into design flow. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 12–32. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_2CrossRef

Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-642-18216-7CrossRefMATH

Carioni, A., Gargantini, A., Riccobene, E., Scandurra, P.: A scenario-based validation language for ASMs. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 71–84. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87603-8_7CrossRef

Hybrid ERTMS/ETCS Level 3. Technical report, EEIG ERTMS Users Group, July 2017

Chen, J., Cui, H.: Translation from adapted UML to promela for CORBA-based applications. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 234–251. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24732-6_17CrossRef

Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_29CrossRef

Glossary of terms and abbreviations. Technical report, ERA * UNISIG * EEIG ERTMS USERS GROUP, May 2016

10.

Havelund, K., Lowry, M., Penix, J.: Formal analysis of a space-craft controller using SPIN. IEEE Trans. Softw. Eng. 27(8), 749–765 (2001)CrossRef

11.

Hoang, T.S., Butler, M., Reichl, K.: The hybrid ERTMS/ETCS level 3 case study. Technical report (2018)

12.

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

13.

Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising event-B models with B-motion studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202–204. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04570-7_17CrossRef

14.

Leuschel, M.: The high road to formal validation. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 4–23. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87603-8_2CrossRef

15.

Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRef

16.

Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606–620. Springer, Heidelberg (2006). https://doi.org/10.1007/11901433_33CrossRef

17.

Prigent, A., Cassez, F., Dhaussy, P., Roux, O.: Extending the translation from SDL to Promela. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 79–94. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46017-9_8CrossRef

Titel: Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin
verfasst von: Paolo Arcaini
Pavel Ježek
Jan Kofroň
Verlag: Springer International Publishing
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_19

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"