2021
Conference article  Open Access

Formal analysis of the UNISIG safety application intermediate sub-layer. Applying Formal Methods to railway standard interfaces

Basile D., Fantechi A., Rosadi I.

Formal Methods  Standard interface  Unisig  Uppaal  Railway 

The combined use of standard interfaces and formal methods is currently under investigation by Shift2Rail, a joint undertaking between railway stakeholders and the EU. Standard interfaces are useful to increase market competition and standardization whilst reducing long-term life cycle costs. Formal methods are needed to achieve interoperability and safety of standard interfaces and are one of the targets of the 4SECURail project funded by Shift2Rail. This paper presents the modelling and analysis of the selected case study of the 4SECURail project: the Safe Application Intermediate sub-layer of the UNISIG RBC/RBC Safe Communication Interface. The adopted formal method is Statistical Model Checking of a network of Stochastic Priced Timed Automata, as provided by the Uppaal SMC tool. The main contributions are: (i) rigorous complete and publicly available models of an official interface specification already in operation, (ii) identification of safety and interoperability issues in the original specification using Statistical Model Checking, (iii) quantification of costs for learning the adopted formal method and developing the carried out analysis.

Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 174–190, Online conference, 24-26/08/2021


Metrics



Back to previous page
BibTeX entry
@inproceedings{oai:it.cnr:prodotti:456088,
	title = {Formal analysis of the UNISIG safety application intermediate sub-layer. Applying Formal Methods to railway standard interfaces},
	author = {Basile D. and Fantechi A. and Rosadi I.},
	doi = {10.1007/978-3-030-85248-1_11},
	booktitle = {FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 174–190, Online conference, 24-26/08/2021},
	year = {2021}
}

4SECURAIL
FORMAL METHODS AND CSIRT FOR THE RAILWAY SECTOR


OpenAIRE