Adopting Formal Methods in an Industrial Setting: The Railways Case

  • Maurice H. ter BeekEmail author
  • Arne Borälv
  • Alessandro FantechiEmail author
  • Alessio FerrariEmail author
  • Stefania GnesiEmail author
  • Christer Löfving
  • Franco MazzantiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)


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. Two Shift2Rail projects, X2Rail-2 and ASTRail, have addressed this issue by performing a systematic search over the state of the art of formal methods application in railways to identify the best used practices. As part of the work of these projects, questionnaires on formal methods and tools have been designed to gather input and guidance on the adoption of formal methods in the railway domain. Even though the questionnaires were developed independently and distributed to different audiences, the responses show a certain convergence in the replies to the questions common to both. In this paper, we present a detailed report on such convergence, drawing some indications about methods and tools that are considered to constitute the most fruitful approaches to industrial adoption.



This work has been partially funded by the ASTRail and the X2Rail-2 projects. These projects received funding from the Shift2Rail Joint Undertaking under the European Union’s Horizon 2020 research and innovation programme under grant agreement No. 777561 and No. 777465.


  1. 1.
    Ameur, Y.A., Boniol, F., Wiels, V.: Toward a wider use of formal methods for aerospace systems design and verification. Int. J. Softw. Tools Technol. Transfer 12(1), 1–7 (2010)CrossRefGoogle Scholar
  2. 2.
    Basile, D., et al.: On the industrial uptake of formal methods in the railway domain. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 20–29. Springer, Cham (2018). Scholar
  3. 3.
    Butler, M.J., et al.: Formal modelling techniques for efficient development of railway control products. RSSRail. LNCS, vol. 10598, pp. 71–86. Springer, Cham (2017). Scholar
  4. 4.
    Davis, J.A., et al.: Study on the barriers to the industrial adoption of formal methods. In: Pecheur, C., Dierkes, M. (eds.) FMICS 2013. LNCS, vol. 8187, pp. 63–77. Springer, Heidelberg (2013). Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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). Scholar
  7. 7.
    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). Scholar
  8. 8.
    Ferrari, A., et al.: Survey on formal methods and tools in railways: The ASTRail approach. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 226–241. Springer, Cham (2019). Scholar
  9. 9.
    Garavel, H., Mateescu, R.: Reflections on Bernhard Steffen’s physics of software tools. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not?. LNCS, vol. 11200, pp. 186–207. Springer, Cham (2019). Scholar
  10. 10.
    Nyberg, M., Gurov, D., Lidström, C., Rasmusson, A., Westman, J.: Formal verification in automotive industry: enablers and obstacles. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 139–158. Springer, Cham (2018). Scholar
  11. 11.
    Plat, N., van Katwijk, J., Toetenel, H.: Application and benefits of formal methods in software development. Softw. Eng. J. 7(5), 335–346 (1992)CrossRefGoogle Scholar
  12. 12.
    X2Rail-2 - Deliverable D5.1, Formal Methods (Taxonomy and Survey), Proposed Methods and Applications (16 May 2018).

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.ISTI–CNRPisaItaly
  2. 2.Università di FirenzeFlorenceItaly
  3. 3.TrafikverketGöteborgSweden

Personalised recommendations