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

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.

BibTeX:

@inproceedings{arcaini_modelling_2018,
    title = {{Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin}},
    author = {Arcaini, Paolo and Jež ek, Pavel and Kofroň, Jan},
    year = {2018},
    booktitle = {{Abstract State Machines, Alloy, B, TLA, VDM, and Z}},
    editor = {Butler, Michael and Raschke, Alexander and Hoang, Thai Son and Reichl, Klaus},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    doi = {10.1007/978-3-319-91271-4_19},
    isbn = {978-3-319-91271-4},
    pages = {277--291},
    url = {https://link.springer.com/chapter/10.1007\%2F978-3-319-91271-4_19},
}

Proceedings paper