Skip to main content
SpringerLink
Log in
Book cover

International Conference on Integrated Formal Methods

IFM 2018: Integrated Formal Methods pp 20–29Cite as

On the Industrial Uptake of Formal Methods in the Railway Domain

A Survey with Stakeholders

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11023))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    http://astrail.eu.

  2. 2.

    http://shift2rail.org.

  3. 3.

    http://conferences.ncl.ac.uk/rssrail/.

  4. 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. 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. 6.

    For this and subsequent questions, respondents could select more than one answer.

References

  1. 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

    Article  MathSciNet  Google Scholar 

  2. 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)

    Google Scholar 

  3. 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

    Google Scholar 

  4. 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

  5. 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

    Article  Google Scholar 

  6. 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)

    Google Scholar 

  7. 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

    Book  Google Scholar 

  8. 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

  9. 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

    Chapter  Google Scholar 

  10. 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

    Chapter  Google Scholar 

  11. 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

    Article  Google Scholar 

  12. 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

    Book  Google Scholar 

  13. 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

    Article  Google Scholar 

  14. 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

  15. 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

    Article  Google Scholar 

  16. 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

    Chapter  Google Scholar 

  17. 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

    Chapter  Google Scholar 

  18. 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

    Article  Google Scholar 

  19. 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

  20. 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

    Article  Google Scholar 

  21. 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

    Article  Google Scholar 

  22. 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

  23. 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

  24. 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

  25. 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

    Article  Google Scholar 

Download references

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

  1. ISTI–CNR, Pisa, Italy

    Davide Basile, Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, Franco Mazzanti & Alessio Ferrari

  2. SIRTI S.p.A., Genoa, Italy

    Andrea Piattino & Daniele Trentini

  3. Università di Firenze, Florence, Italy

    Davide Basile & Alessandro Fantechi

Authors
  1. Davide Basile
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maurice H. ter Beek
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alessandro Fantechi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Stefania Gnesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Franco Mazzanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Andrea Piattino
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Daniele Trentini
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Alessio Ferrari
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alessio Ferrari .

Editor information

Editors and Affiliations

  1. Università della Svizzera Italiana, Lugano, Switzerland

    Carlo A. Furia

  2. University of Queensland, Brisbane, Queensland, Australia

    Kirsten Winter

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation