Abstract
Formal methods and tools have been widely applied to the development of railway systems during the last decades. However, no universally accepted formal framework has emerged, and railway companies wishing to introduce formal methods have little guidance for the selection of the most appropriate methods and tools to adopt. A work package (WP) of the European project ASTRail, funded under the Shift2Rail initiative, addresses this problem, by performing a survey that considers scientific literature, international projects, and practitioners’ perspectives to identify a collection of formal methods and tools to be applied in railways. This paper summarises the current results of this WP. We surveyed 114 scientific publications, 44 practitioners, and 8 projects to come to a shortlist of 14 methods considered suitable for system modelling and verification in railways. The methods and tools were reviewed according to a set of functional, language-related, and quality features. The current paper extends the body of knowledge with a set of publicly available documents that can be leveraged by companies for guidance on formal methods selection in railway system development.
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
Notes
- 1.
- 2.
- 3.
- 4.
In the case of SCADE, due to licensing issues, it was not possible to gain a hands-on experience within the limited timespan of the project. Hence, our evaluation is based on the analysis of the available official tool documentation and presentations, and on the experiences reported in students’ assignments at the University of Florence, carried out under the ANSYS SCADE Academic Program.
References
Abrial, J.R.: Formal methods: theory becoming practice. J. Univers. Comput. Sci. 13(5), 619–628 (2007). https://doi.org/10.3217/jucs-013-05-0619
Basile, D., ter Beek, M.H., Ciancia, V.: Statistical model checking of a moving block railway signalling scenario with Uppaal SMC. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 372–391. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03421-4_24
Basile, D., et al.: On the industrial uptake of formal methods in the railway domain – a survey with stakeholders. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 20–29. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98938-9_2
ter Beek, M.H., Gnesi, S., Knapp, A.: Formal methods for transport systems. Int. J. Softw. Tools Technol. Transf. 20(3), 237–241 (2018). https://doi.org/10.1007/s10009-018-0487-4
Berger, U., James, P., Lawrence, A., Roggenbach, M., Seisenberger, M.: Verification of the European rail traffic management system in real-time maude. Sci. Comput. Program. 154, 61–88 (2018). https://doi.org/10.1016/j.scico.2017.10.011
Bjørner, D.: New results and trends in formal techniques and tools for the development of software for transportation systems – a review. In: Tarnai, G., Schnieder, E. (eds.) Proceedings of the 4th Symposium on Formal Methods for Railway Operation and Control Systems, FORMS 2003. L’Harmattan, Hungary (2003)
Bosschaart, M., Quaglietta, E., Janssen, B., Goverde, R.M.P.: Efficient formalization of railway interlocking data in RailML. Inf. Syst. 49, 126–141 (2015). https://doi.org/10.1016/j.is.2014.11.007
Boulanger, J.L. (ed.): Formal Methods Applied to Industrial Complex Systems—Implementation of the B Method. Wiley, Hoboken (2014). https://doi.org/10.1002/9781119002727
Chiappini, A., et al.: Formalization and validation of a subset of the European Train Control System. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, ICSE 2010, vol. 2, pp. 109–118. ACM, USA (2010). https://doi.org/10.1145/1810295.1810312
European Committee for Electrotechnical Standardization: CENELEC EN 50128—Railway applications – Communication, signalling and processing systems – Software for railway control and protection systems, 1 June 2011. https://standards.globalspec.com/std/1678027/cenelec-en-50128
Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167–183. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05032-4_13
Ferrari, A., Fantechi, A., Magnani, G., Grasso, D., Tempestini, M.: The Metrô Rio case study. Sci. Comput. Program. 78(7), 828–842 (2013). https://doi.org/10.1016/j.scico.2012.04.003
Ferrari, A., et al.: Survey on formal methods and tools in railways technical report on the activities performed within ASTRail, Deliverable D4.1. Technical report 396822, ISTI-CNR (2018). https://doi.org/10.5281/zenodo.2573921
Ferrari, A., Fantechi, A., Gnesi, S., Magnani, G.: Model-based development and formal methods in the railway industry. IEEE Softw. 30(3), 28–34 (2013). https://doi.org/10.1109/MS.2013.44
Flammini, F. (ed.): Railway Safety, Reliability, and Security: Technologies and Systems Engineering. IGI Global, Hershey (2012). https://doi.org/10.4018/978-1-4666-1643-1
Haxthausen, A.E., Peleska, J., Kinder, S.: A formal approach for the construction and verification of railway control systems. Formal Aspects Comput. 23(2), 191–219 (2011). https://doi.org/10.1007/s00165-009-0143-6
Iliasov, A., Taylor, D., Laibinis, L., Romanovsky, A.: Formal verification of signalling programs with SafeCap. In: Gallina, B., Skavhaug, A., Bitsch, F. (eds.) SAFECOMP 2018. LNCS, vol. 11093, pp. 91–106. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99130-6_7
James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Techniques for modelling and verifying railway interlockings. Int. J. Softw. Tools Technol. Transf. 16, 685–711 (2014). https://doi.org/10.1007/s10009-014-0304-7
Kitchenham, B.: Procedures for performing systematic reviews. Technical report TR/SE-0401. University of Keele, UK, July 2004. https://goo.gl/vYU8Fu
Lecomte, T., Deharbe, D., Prun, E., Mottin, E.: Applying a formal method in industry: a 25-year trajectory. In: Cavalheiro, S., Fiadeiro, J. (eds.) SBMF 2017. LNCS, vol. 10623, pp. 70–87. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70848-5_6
Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Formal Aspects Comput. 23(6), 683–709 (2011). https://doi.org/10.1007/s00165-010-0172-1
Mazzanti, F., Ferrari, A.: Ten diverse formal models for a CBTC automatic train supervision system. In: Gallagher, J.P., van Glabbeek, R., Serwe, W. (eds.) Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation, MARS/VPT 2018. EPTCS, vol. 268, pp. 104–149 (2018). https://doi.org/10.4204/EPTCS.268.4
Mazzanti, F., Ferrari, A., Spagnolo, G.O.: Towards formal methods diversity in railways: an experience report with seven frameworks. Int. J. Softw. Tools Technol. Transf. 20(3), 263–288 (2018). https://doi.org/10.1007/s10009-018-0488-3
Mazzanti, F., Spagnolo, G.O., Della Longa, S., Ferrari, A.: Deadlock avoidance in train scheduling: a model checking approach. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 109–123. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10702-8_8
Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Defining and model checking abstractions of complex railway models using CSP\(\parallel \)B. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 193–208. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39611-3_20
Rispoli, F., Castorina, M., Neri, A., Filip, A., Di Mambro, G., Senesi, F.: Recent progress in application of GNSS and advanced communications for railway signaling. In: Proceedings of the 23rd International Conference Radioelektronika, RADIOELEKTRONIKA 2013, pp. 13–22. IEEE (2013). https://doi.org/10.1109/RadioElek.2013.6530882
Vanit-Anunchai, S.: Modelling and simulating a Thai railway signalling system using Coloured Petri Nets. Int. J. Softw. Tools Technol. Transf. 20(3), 243–262 (2018). https://doi.org/10.1007/s10009-018-0482-9
Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133, 91–115 (2017). https://doi.org/10.1016/j.scico.2016.05.010
Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Oudshoorn, M.J. (ed.) Proceedings of the 26th Australasian Computer Science Conference, ACSC 2003. Conferences in Research and Practice in Information Technology, vol. 16, pp. 309–316. Australian Computer Society, Australia (2003). http://crpit.com/confpapers/CRPITV16Winter.pdf
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.S.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1–19:36 (2009). https://doi.org/10.1145/1592434.1592436
Acknowledgements
This work has been partially funded by the ASTRail project. This project received funding from the Shift2Rail Joint Undertaking under the European Union’s Horizon 2020 research and innovation programme under grant agreement No. 777561. The content of this paper reflects only the authors’ view and the Shift2Rail Joint Undertaking is not responsible for any use that may be made of the included information.
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
Ferrari, A. et al. (2019). Survey on Formal Methods and Tools in Railways: The ASTRail Approach. 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_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-18744-6_15
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)