Abstract
Over the past decade, the growing number of safety-critical software in the railway signalling industry has led customers and industrials to look for efficient, cost-effective, verification and validation techniques. Formal methods, which have proven to be applicable and beneficial in terms of accuracy and completeness, are good candidates. However, they are still far from being used systematically for the verification of all safety-critical railway signalling systems. In order to evaluate their applicability, Alstom successfully experimented on its interlocking systems the model checking methods and tools developed by Systerel. This article describes the methodology used to industrialize this experimental model checking application process.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bernardeschi, C., Fantechi, A., Gnesi, S., Mongardi, G.: Proving safety properties for embedded control systems. In: Hlawiczka, A., Silva, J.G., Simoncini, L. (eds.) EDCC 1996. LNCS, vol. 1150, pp. 321–332. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61772-8_46
Breton, N., Fonteneau, Y.: S3: proving the safety of critical systems. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 231–242. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33951-1_17
Eisner, C.: Using symbolic model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 99–109. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48153-2_9
Haxthausen, A.E., Peleska, J., Pinger, R.: Applied bounded model checking for interlocking system designs. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 205–220. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05032-4_16
James, P., et al.: Verification of solid state interlocking programs. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 253–268. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05032-4_19
Mota, J.L., et al.: Safety demonstration for a rail signaling application in nominal and degraded modes using formal proof. In: Formal Methods Applied to Industrial Complex Systems, pp. 71–113, July 2014. https://doi.org/10.1002/9781119004707.ch4
Ordioni, J., Breton, N., Colaço, J.L.: HLL vol 2.7 modelling language specification. Other STF-16-01805, RATP, May 2018. https://hal.archives-ouvertes.fr/hal-01799749
Winter, K.: Model checking railway interlocking systems, February 2002. https://doi.org/10.1145/563857.563836
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Parillaud, C., Fonteneau, Y., Belmonte, F. (2019). Interlocking Formal Verification at Alstom Signalling. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2019. Lecture Notes in Computer Science(), vol 11495. Springer, Cham. https://doi.org/10.1007/978-3-030-18744-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-18744-6_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-18743-9
Online ISBN: 978-3-030-18744-6
eBook Packages: Computer ScienceComputer Science (R0)