Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers | SpringerLink
Skip to main content
Springer Nature Link
Log in

Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Applications (ISoLA 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12478))

Included in the following conference series:

Abstract

The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.

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

Access this chapter

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

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    http://www.shift2rail.org.

  2. 2.

    https://www.4securail.eu/.

  3. 3.

    https://projects.shift2rail.org/s2r_ip2_n.aspx?p=X2RAIL-2.

  4. 4.

    https://uic.org/.

  5. 5.

    https://www.era.europa.eu/.

  6. 6.

    http://www.ertms.net/wp-content/uploads/2014/09/ERTMS_Factsheet_8_UNISIG.pdf.

  7. 7.

    https://www.agilealliance.org/.

  8. 8.

    https://eulynx.eu/.

  9. 9.

    https://www.graphviz.org/.

  10. 10.

    https://www.ptc.com/en/products/plm/plm-products/windchill/modeler/sysim.

  11. 11.

    https://sparxsystems.com/products/ea/index.html.

  12. 12.

    https://www.nomagic.com/products/cameo-systems-modeler.

  13. 13.

    https://www3.hhu.de/stups/prob/.

  14. 14.

    http://www.eclipse.org/org/documents/epl-v10.html.

  15. 15.

    http://www.formalmind.com/.

  16. 16.

    https://www.mcrl2.org/.

  17. 17.

    https://cadp.inria.fr/.

  18. 18.

    https://cocotec.io/fdr/index.html.

  19. 19.

    http://fmt.isti.cnr.it/kandisti/.

  20. 20.

    http://www.event-b.org/.

  21. 21.

    http://www.uppaal.org/.

References

  1. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

  2. ASTRail Deliverable D4.3: Validation Report. http://astrail.eu/download.aspx?id=d7ae1ebf-52b4-4bde-b25e-ae251fd906df

  3. 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). https://doi.org/10.1007/978-3-319-98938-9_2

    Chapter  Google Scholar 

  4. ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011). https://doi.org/10.1016/j.scico.2010.07.002

    Article  MATH  Google Scholar 

  5. ter Beek, M.H., et al.: Adopting formal methods in an industrial setting: the railways case. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 762–772. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_46

    Chapter  Google Scholar 

  6. Behrmann, G., et al.: UPPAAL 4.0. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of SysTems (QEST 2006), pp. 125–126. IEEE (2006). https://doi.org/10.1109/QEST.2006.59

  7. Bendisposto, J., et al.: ProB 2.0 tutorial. In: Butler, M., Hallerstede, S., Waldén, M. (eds.) Proceedings of the 4th Rodin User and Developer Workshop. TUCS Lecture Notes, Turku Centre for Computer Science (2013)

    Google Scholar 

  8. Berglehner, R., Rasheeq, A.: An approach to improve SysML railway specification using UML-B and EVENT-B. In: Poster at the 3rd International Conference on Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification (RSSRail 2019) (2019). https://doi.org/10.13140/RG.2.2.21925.45288

  9. Bernardi, S., et al.: Enabling the usage of UML in the verification of railway systems: the DAM-rail approach. Rel. Eng. Syst. Saf. 120, 112–126 (2013). https://doi.org/10.1016/j.ress.2013.06.032

    Article  Google Scholar 

  10. Besnard, V., Brun, M., Jouault, F., Teodorov, C., Dhaussy, P.: Unified LTL verification and embedded execution of UML models. In: Proceedings of the 21th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems (MoDELS 2018), pp. 112–122. ACM (2018). https://doi.org/10.1145/3239372.3239395

  11. Bhaduri, P., Ramesh, S.: Model Checking of Statechart Models: Survey and Research Directions. CoRR cs.SE/0407038 (2004). http://arxiv.org/abs/cs.SE/0407038

  12. Broy, M., Crane, M.L., Dingel, J., Hartman, A., Rumpe, B., Selic, B.: 2\(^{nd}\) UML 2 semantics symposium: formal semantics for UML. In: Kühne, T. (ed.) MODELS 2006. LNCS, vol. 4364, pp. 318–323. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69489-2_39

    Chapter  Google Scholar 

  13. Bui, N.L.: An analysis of the benefits of EULYNX-style requirements modeling for ProRail. Ph.D. thesis, Technische Universiteit Eindhoven (2017). https://research.tue.nl/files/91220589/2017_09_28_ST_Bui_L.pdf

  14. Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2

    Chapter  Google Scholar 

  15. Butler, M., et al.: The first twenty-five years of industrial use of the B-method. In: ter Beek, M.H., Ničković, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 189–209. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58298-2_8

    Chapter  Google Scholar 

  16. Caltais, G., Leitner-Fischer, F., Leue, S., Weiser, J.: SysML to NuSMV model transformation via object-orientation. In: Berger, C., Mousavi, M.R., Wisniewski, R. (eds.) CyPhy 2016. LNCS, vol. 10107, pp. 31–45. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-51738-4_3

    Chapter  Google Scholar 

  17. Chen, J., Cui, H.: Translation from adapted UML to Promela for CORBA-based applications. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 234–251. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24732-6_17

    Chapter  Google Scholar 

  18. Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten years of performance evaluation for concurrent systems using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 128–142. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16561-0_18

    Chapter  Google Scholar 

  19. Crane, M.L., Dingel, J.: UML vs. classical vs. Rhapsody statecharts: not all models are created equal. In: Briand, L., Williams, C. (eds.) MODELS 2005. LNCS, vol. 3713, pp. 97–112. Springer, Heidelberg (2005). https://doi.org/10.1007/11557432_8

    Chapter  Google Scholar 

  20. Cranen, S., et al.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199–213. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_15

    Chapter  Google Scholar 

  21. European Committee for Electrotechnical Standardization: CENELEC EN 50128 – Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems, June 2011. https://standards.globalspec.com/std/1678027/cenelec-en-50128

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

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

  24. Fantechi, A., Fokkink, W., Morzenti, A.: Some trends in formal methods applications to railway signaling. In: Gnesi, S., Margaria, T. (eds.) Formal Methods for Industrial Critical Systems: A Survey of Applications, chap. 4, pp. 61–84. Wiley (2013). https://doi.org/10.1002/9781118459898.ch4

  25. Fecher, H., Schönborn, J., Kyas, M., de Roever, W.-P.: 29 new unclarities in the semantics of UML 2.0 state machines. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 52–65. Springer, Heidelberg (2005). https://doi.org/10.1007/11576280_5

    Chapter  Google Scholar 

  26. 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). https://doi.org/10.1007/978-3-030-18744-6_15

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  28. Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H., Fantechi, A.: Comparing formal tools for system design: a judgment study. In: Proceedings of the 42nd International Conference on Software Engineering (ICSE), pp. 62–74. ACM (2020). https://doi.org/10.1145/3377811.3380373

  29. Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Ničković, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 3–69. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58298-2_1

    Chapter  Google Scholar 

  30. Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 3–26. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68270-9_1

    Chapter  Google Scholar 

  31. Gibson-Robinson, T., Armstrong, P.J., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. 18(2), 149–167 (2016). https://doi.org/10.1007/s10009-015-0377-y

    Article  MATH  Google Scholar 

  32. Grumberg, O., Meller, Y., Yorav, K.: Applying software model checking techniques for behavioral UML models. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 277–292. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_25

    Chapter  Google Scholar 

  33. Hvid Hansen, H., Ketema, J., Luttik, B., Mousavi, M.R., van de Pol, J., dos Santos, O.M.: Automated verification of executable UML models. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 225–250. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_12

    Chapter  Google Scholar 

  34. Jussila, T., Dubrovin, J., Junttila, T., Latvala, T., Porres, I.: Model checking dynamic and hierarchical UML state machines. In: Proceedings of the 3rd International Workshop on Model Development, Validation and Verification (MoDeVa 2006), pp. 94–110. University of Queensland (2006)

    Google Scholar 

  35. Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 395–414. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45739-9_23

    Chapter  Google Scholar 

  36. Lang, F., Mateescu, R., Mazzanti, F.: Sharp congruences adequate with temporal logics combining weak and strong modalities. TACAS 2020. LNCS, vol. 12079, pp. 57–76. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_4

    Chapter  Google Scholar 

  37. Liu, S., et al.: A formal semantics for complete UML state machines with communications. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 331–346. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38613-8_23

    Chapter  Google Scholar 

  38. Löfving, C., Borälv, A: X2Rail-2 Deliverable D5.1, Formal Methods (Taxonomy and Survey), Proposed Methods and Applications, May 2018. https://projects.shift2rail.org/download.aspx?id=b4cf6a3d-f1f2-4dd3-ae01-2bada34596b8

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

  40. ModelDriven: The fUML Reference Implementation. https://github.com/ModelDriven/fUML-Reference-Implementation/blob/master/README.md

  41. Ober, I., Graf, S., Ober, I.: Validation of UML models via a mapping to communicating extended timed automata. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 127–145. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24732-6_9

    Chapter  Google Scholar 

  42. Object Management Group: Unified Modelling Language, December 2017. https://www.omg.org/spec/UML/About-UML/

  43. Object Management Group: Precise Semantics of UML Composite Structure (PSCS), March 2018. https://www.omg.org/spec/PSCS/1.1/PDF

  44. Object Management Group: OMG Systems Modeling Language (OMG SysML), November 2019. http://www.omg.org/spec/SysML/1.6/

  45. Oliveira, R., Dingel, J.: Supporting model refinement with equivalence checking in the context of model-driven engineering with UML-RT. In: Burgueño, L., et al. (eds.) Proceedings of the 20th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2017) – Satellite Events. CEUR Workshop Proceedings, vol. 2019, pp. 307–314. CEUR-WS.org (2017). http://ceur-ws.org/Vol-2019/modevva_2.pdf

  46. OMG: Action Language for Foundational UML (Alf) – Concrete Syntax for a UML Action Language, July 2017. https://www.omg.org/spec/ALF/1.1

  47. OMG: Semantics of a Foundational Subset for Executable UML Models (fUML), December 2018. https://www.omg.org/spec/FUML/1.4/PDF

  48. Pétin, J.F., Evrot, D., Morel, G., Lamy, P.: Combining SysML and formal methods for safety requirements verification. In: Proceedings of the 22nd International Conference on Software & Systems Engineering and their Applications (ICSSEA 2010) (2010). https://hal.archives-ouvertes.fr/hal-00533311/document

  49. Simons, A.J.H., Graham, I.: 30 things that go wrong in object modelling with UML 1.3. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems. SECS, vol. 523, pp. 237–257. Springer, Heidelberg (1999). https://doi.org/10.1007/978-1-4615-5229-1_17

    Chapter  Google Scholar 

  50. Snook, C., Savicks, V., Butler, M.: Verification of UML models by translation to UML-B. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 251–266. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_13

    Chapter  Google Scholar 

  51. UNISIG: RBC-RBC Safe Communication Interface – SUBSET-098, February 2012. https://www.era.europa.eu/sites/default/files/filesystem/ertms/ccs_tsi_annex_a_-_mandatory_specifications/set_of_specifications_3_etcs_b3_r2_gsm-r_b1/index063_-_subset-098_v300.pdf

  52. UNISIG: FIS for the RBC/RBC Handover – SUBSET-039, December 2015. https://www.era.europa.eu/sites/default/files/filesystem/ertms/ccs_tsi_annex_a_-_mandatory_specifications/set_of_specifications_3_etcs_b3_r2_gsm-r_b1/index012_-_subset-039_v320.pdf

  53. Visual Paradigm: What is Unified Modeling Language (UML)?. https://www.visual-paradigm.com/guide/uml-unified-modeling-language/what-is-uml/

  54. Yeung, W.L., Leung, K.R.P.H., Wang, J., Dong, W.: Improvements towards formalizing UML state diagrams in CSP. In: Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), pp. 176–184. IEEE (2005). https://doi.org/10.1109/APSEC.2005.70

  55. Zhang, S.J., Liu, Y.: An automatic approach to model checking UML state machines. In: Proceedings of the 4th International Conference on Secure Software Integration and Reliability Improvement (SSIRI-C 2010), pp. 1–6. IEEE (2010). https://doi.org/10.1109/SSIRI-C.2010.11

Download references

Acknowledgements

This work has been partially funded by the 4SECURail project. The 4SECURail project received funding from the Shift2Rail Joint Undertaking under the European Union’s Horizon 2020 research and innovation programme under grant agreement No 881775 in the context of the open call S2R-OC-IP2-01-2019, part of the “Annual Work Plan and Budget 2019”, of the programme H2020-S2RJU-2019. 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.

We also would like to thank the Italian MIUR PRIN 2017FTXR7S project IT MaTTerS (Methods and Tools for Trustworthy Smart Systems).

Author information

Authors and Affiliations

  1. ISTI–CNR, Pisa, Italy

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

  2. Università di Firenze, Firenze, Italy

    Alessandro Fantechi

  3. SIRTI S.p.A., Genova, Italy

    Laura Masullo, Andrea Piattino & Daniele Trentini

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. Alessio Ferrari
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Stefania Gnesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Laura Masullo
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Franco Mazzanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Andrea Piattino
    View author publications

    You can also search for this author in PubMed Google Scholar

  9. Daniele Trentini
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Davide Basile .

Editor information

Editors and Affiliations

  1. University of Limerick and Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Basile, D. et al. (2020). Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020. Lecture Notes in Computer Science(), vol 12478. Springer, Cham. https://doi.org/10.1007/978-3-030-61467-6_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-61467-6_30

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-61466-9

  • Online ISBN: 978-3-030-61467-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation