Abstract
The railway sector has seen a large number of successful applications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in railways is limited. As a first step to address this, we present the results of a questionnaire submitted to 44 stakeholders with experience in the application of formal tools in railways. The questionnaire was oriented to gather information about industrial projects, and about the functional and quality features that a formal tool should have to be successfully applied in railways. The results show that the most used tools are, as expected, those of the B family, followed by an extensive list of about 40 tools, each one used by few respondents only, indicating a rich, yet scattered, landscape. The most desired features concern formal verification, maturity, learnability, quality of documentation, and ease of integration in a CENELEC process. This paper extends the body of knowledge on formal methods applications in the railway industry, and contributes with a ranked list of tool features considered relevant by railway stakeholders.
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.
We did not weigh the results based on the declared experience of the respondents, because we wanted to give equal importance to their different answers, regardless of the specific experience.
- 5.
When present, the subsequent answers of these respondents were discarded from our statistics, since they were considered outliers with respect to our population sample.
- 6.
For this and subsequent questions, respondents could select more than one answer.
References
Abrial, J.R.: Formal methods: theory becoming practice. J. Univ. 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.) Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018). LNCS. Springer, Heidelberg (2018, to appear)
ter Beek, M.H., Fantechi, A., Ferrari, A., Gnesi, S., Scopigno, R.: Formal methods for the railway sector. ERCIM News 112, 44–45 (2018). https://ercim-news.ercim.eu/en112/r-i/formal-methods-for-the-railway-sector
ter Beek, M.H., Fantechi, A., Gnesi, S.: Product line models of large cyber-physical systems: the case of ERTMS/ETCS. In: Proceedings of the 22nd International Systems and Software Product Line Conference (SPLC 2018). ACM (2018). https://doi.org/10.1145/3233027.3233046
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
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 (2003)
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
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
Fantechi, A., Ferrari, A., Gnesi, S.: Formal methods and safety certification: challenges in the railways domain. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 261–265. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_18
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
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
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
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). Electronic Proceedings in Theoretical Computer Science, 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\(||\)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
Scupin, R.: The KJ method: a technique for analyzing data derived from Japanese ethnology. Hum. Organ. 56(2), 233–237 (1997). https://doi.org/10.17730/humo.56.2.x335923511444655
Sun, P.: Model based system engineering for safety of railway critical systems. Ph.D. thesis, Ecole Centrale de Lille (2015). https://tel.archives-ouvertes.fr/tel-01293395
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.: Model checking railway interlocking systems. In: Oudshoorn, M.J. (ed.) Proceedings of the 25th Australasian Conference on Computer Science (ACSC 2002). Conferences in Research and Practice in Information Technology, vol. 4, pp. 303–310. Australian Computer Society (2002). http://crpit.com/confpapers/CRPITV4Winter.pdf
Winter, K., Johnston, W., Robinson, P., Strooper, P., van den Berg, L.: Tool support for checking railway interlocking designs. In: Cant, T. (ed.) Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software (SCS 2005). Conferences in Research and Practice in Information Technology, vol. 55, pp. 101–107. Australian Computer Society (2006). http://crpit.com/confpapers/CRPITV55Winter.pdf
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 (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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Basile, D. et al. (2018). On the Industrial Uptake of Formal Methods in the Railway Domain. In: Furia, C., Winter, K. (eds) Integrated Formal Methods. IFM 2018. Lecture Notes in Computer Science(), vol 11023. Springer, Cham. https://doi.org/10.1007/978-3-319-98938-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-98938-9_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98937-2
Online ISBN: 978-3-319-98938-9
eBook Packages: Computer ScienceComputer Science (R0)