Skip to main content
Top

2018 | OriginalPaper | Chapter

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

Authors : Paolo Arcaini, Pavel Ježek, Jan Kofroň

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

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

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!

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!

Footnotes
1
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.
 
2
Note that the case study assignment [11] considers movement only in one direction, i.e., no backward moves.
 
3
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.
 
4
The simulation output of the assertion violation can be found at http://​d3s.​mff.​cuni.​cz/​~kofron/​abz18casestudy.​html.
 
5
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).
 
Literature
1.
go back to reference Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRef Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRef
6.
go back to reference Hybrid ERTMS/ETCS Level 3. Technical report, EEIG ERTMS Users Group, July 2017 Hybrid ERTMS/ETCS Level 3. Technical report, EEIG ERTMS Users Group, July 2017
8.
go back to reference 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 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
9.
go back to reference Glossary of terms and abbreviations. Technical report, ERA * UNISIG * EEIG ERTMS USERS GROUP, May 2016 Glossary of terms and abbreviations. Technical report, ERA * UNISIG * EEIG ERTMS USERS GROUP, May 2016
10.
go back to reference 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 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.
go back to reference Hoang, T.S., Butler, M., Reichl, K.: The hybrid ERTMS/ETCS level 3 case study. Technical report (2018) Hoang, T.S., Butler, M., Reichl, K.: The hybrid ERTMS/ETCS level 3 case study. Technical report (2018)
12.
go back to reference Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004) Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)
15.
go back to reference 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 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
Metadata
Title
Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin
Authors
Paolo Arcaini
Pavel Ježek
Jan Kofroň
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-319-91271-4_19

Premium Partner