Formal methods for transport systems | International Journal on Software Tools for Technology Transfer Skip to main content
Springer Nature Link
Log in

Formal methods for transport systems

  • Introduction
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Formal methods and verification tools have been in use in the engineering of safety-critical transport systems for well over 30 years. In both the railway and the avionics domain, for instance, formal methods are specifically recommended in current international certification standards for ultra-dependable systems and for products at the highest integrity level. In fact, traditionally, the applications of formal methods and tools to such transport systems concern demonstrating, with the highest levels of assurance, the correct functioning of the software systems involved, such as train signalling systems to avoid collisions. More recently, however, formal methods and verification tools have started to be applied also to the scheduling and management of transport systems or networks, for instance to optimise the exploitation of a railway line or to improve the operational efficiency of a bus network. In this introduction to the special issue on “Formal Methods for Transport Systems”, we outline some recent achievements for each of the above-mentioned types of application of formal methods and tools. These achievements are represented by three selected papers: one was selected from the “Formal Methods and Safety Certification: Challenges in the Railways Domain” track at the seventh International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016); another one was selected from the 21st International Workshop on Formal Methods for Industrial Critical Systems and the 16th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS 2016); a final one was selected after an open call for contributions.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Notes

  1. www.shift2rail.org.

References

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

    Article  Google Scholar 

  2. Gigante, G., Pascarella, D.: Formal methods in avionic software certification: the DO-178C perspective. In: Margaria, T., Steffen, B. (eds.) Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications and Case Studies (ISoLA 2012), Part II. Lecture Notes in Computer Science, vol. 7610, pp. 205–215. Springer (2012)

  3. Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., Núñez, M. (eds.) Software Engineering and Formal Methods—Revised Selected Papers of the SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD, and OpenCert. Lecture Notes in Computer Science, vol. 8368, pp. 167–183. Springer (2013)

  4. Gnesi, S., Margaria, T.: Formal Methods for Industrial Critical Systems: A Survey of Applications. Wiley, Hoboken (2013)

    Google Scholar 

  5. European Committee for Electrotechnical Standardization: CENELEC—EN 50128: railway applications—communication, signalling and processing systems—software for railway control and protection systems, June (2011). http://standards.globalspec.com/std/1678027/cenelec-en-50128

  6. Radio Technical Commission for Aeronautics: RTCA DO–178: software considerations in airborne systems and equipment certification, December (2011). http://standards.globalspec.com/std/1830812/rtca-do-178

  7. Almeida, J.B., Frade, M.J., Pinto, J.S., de Sousa, S.M.: An overview of formal methods tools and techniques. In: Rigorous Software Development: An Introduction to Program Verification, pp. 15–44. Springer (2011)

  8. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  9. Fantechi, A., Ferrari, A., Gnesi, S.: Formal methods and safety certification: challenges in the railways domain. In: Margaria, Steffen (eds.) [10], pp. 261–265

  10. Margaria, T., Steffen, B. (eds.): Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications (ISoLA 2016), Part II. Lecture Notes in Computer Science, vol. 9953. Springer (2016)

  11. ter Beek, M.H., Gnesi, S., Knapp, A. (eds.): Critical Systems: Formal Methods and Automated Verification—Proceedings of the Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS 2016). Lecture Notes in Computer Science, vol. 9933. Springer (2016)

  12. Vanit-Anunchai, S.: Modelling and simulating a Thai railway signalling system using Coloured Petri Nets. Int. J. Softw. Tools Technol. Transf. (2018). https://doi.org/10.1007/s10009-018-0482-9

  13. 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. (2018). https://doi.org/10.1007/s10009-018-0488-3

  14. Mazzanti, F., Spagnolo, G.O., Ferrari, A.: Designing a deadlock-free train scheduler: a model checking approach. In: Badger, J.M., Rozier, K.Y. (eds.) Proceedings of the 6th International NASA Formal Methods Symposium (NFM 2014). Lecture Notes in Computer Science, vol. 8430, pp. 264–269. Springer (2014)

  15. IEEE Vehicular Technology Society: IEEE Std 1474.1-2004(R2009): IEEE standard for communications-based train control (CBTC) performance and functional requirements, February (2005). https://doi.org/10.1109/IEEESTD.2004.95746

  16. Littlewood, B., Popov, P., Strigini, L.: Modeling software design diversity: a review. ACM Comput. Surv. 33(2), 177–208 (2001)

    Article  Google Scholar 

  17. Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Int. J. Softw. Tools Technol. Transf. (2018). https://doi.org/10.1007/s10009-018-0483-8

Download references

Acknowledgements

We would like to thank all authors for their contributions and the reviewers of ISoLA 2016, FMICS-AVoCS 2016 and in particular those of this special issue for their reviews.

Author information

Authors and Affiliations

  1. Istituto di Scienza e Tecnologie dell’Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek & Stefania Gnesi

  2. Institute for Software and Systems Engineering, Universität Augsburg, Augsburg, Germany

    Alexander Knapp

Authors
  1. Maurice H. ter Beek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefania Gnesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexander Knapp
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maurice H. ter Beek.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

ter Beek, M.H., Gnesi, S. & Knapp, A. Formal methods for transport systems. Int J Softw Tools Technol Transfer 20, 237–241 (2018). https://doi.org/10.1007/s10009-018-0487-4

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-018-0487-4

Keywords

Search

Navigation