[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14290))

  • The original version of chapter 1 has been revised: two authors’ names and the publication year in Reference [36] have been corrected. A correction to this chapter can be found at https://doi.org/10.1007/978-3-031-43681-9_15

Abstract

The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into industrial model-based development tools has been the subject of recent research, indicating the potential transfer of academic techniques to enhance industrial tools. This paper explores the integration of an academic formal verification tool, UML Model Checker (UMC), with an industrial model-based development tool, Sparx Enterprise Architect (Sparx EA). The case study being analyzed is a railway standard interface. The paper demonstrates how formal verification techniques from academic tools can be integrated into industrial development practices using industrial tools, and how simulation in Sparx EA can be derived from traces generated by the UMC formal verification activity. From this experience, we derive a set of lessons learned and research challenges.

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
£29.99 /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
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 39.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 49.99
Price includes VAT (United Kingdom)
  • 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

Change history

  • 20 March 2024

    A correction has been published.

References

  1. CADP: bcgcmp man page, https://cadp.inria.fr/man/bcg_cmp.html

  2. Dassault Cameo Systems Modeler, https://www.3ds.com/products-services/catia/products/no-magic/cameo-systems-modeler/, Accessed Apr 2023

  3. mCRL2: ltscompare man page, https://www.mcrl2.org/web/user_manual/tools/release/ltscompare.html

  4. Multiple improvements to executable state machine code generation, https://sparxsystems.com/products/ea/15.2/history.html, Accessed May 2023

  5. PTC Windchill Modeler SySim, https://www.ptc.com/en/products/windchill/modeler/sysim, Accessed Apr 2023

  6. Sparx Systems Enterprise Architect, https://sparxsystems.com/products/ea/index.html, Accessed May 2023

  7. The Shift2Rail 4SECURail project site, https://projects.shift2rail.org/s2r_ip2_n.aspx?p=s2r_4securail, Accessed May 2023

  8. UMC project website, https://fmt.isti.cnr.it/umc

  9. André, É., Liu, S., Liu, Y., Choppy, C., Sun, J., Dong, J.S.: Formalizing UML state machines for automated verification-a survey. ACM Comput. Surv. (2023). https://doi.org/10.1145/3579821

    Article  Google Scholar 

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

  11. Basile, D., Mazzanti, F., Ferrari, A.: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect - Complementary Data (2023). https://doi.org/10.5281/zenodo.7920448

    Article  Google Scholar 

  12. Basile, D., et al.: Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 467–485. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-61467-6_30

    Chapter  Google Scholar 

  13. Basile, D., ter Beek, M.H., Ferrari, A., Legay, A.: Modelling and Analysing ERTMS L3 Moving Block Railway Signalling with Simulink and Uppaal SMC. In: Larsen, K.G., Willemse, T. (eds.) FMICS 2019. LNCS, vol. 11687, pp. 1–21. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-27008-7_1

    Chapter  Google Scholar 

  14. Basile, D., ter Beek, M.H., Lazreg, S., Cordy, M., Legay, A.: Static detection of equivalent mutants in real-time model-based mutation testing. Empir. Softw. Eng. 27(7), 160 (2022). https://doi.org/10.1007/s10664-022-10149-y

    Article  Google Scholar 

  15. Basile, D., Fantechi, A., Rosadi, I.: Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 174–190. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-85248-1_11

    Chapter  Google Scholar 

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

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

  18. Belli, D., Mazzanti, F.: A case study in formal analysis of system requirements. In: Masci, P., Bernardeschi, C., Graziani, P., Koddenbrock, M., Palmieri, M. (eds.) SEFM Workshops. LNCS, vol. 13765, pp. 164–173. Springer (2022). https://doi.org/10.1007/978-3-031-26236-4_14

  19. Bougacha, R., Laleau, R., Dutilleul, S.C., Ayed, R.B.: Extending SysML with refinement and decomposition mechanisms to generate Event-B specifications. In: Ameur, Y.A., Craciun, F. (eds.) TASE. LNCS, vol. 13299, pp. 256–273. Springer (2022). https://doi.org/10.1007/978-3-031-10363-6_18

  20. Bouwman, M., Luttik, B., van der Wal, D.: A Formalisation of SysML State Machines in mCRL2. In: Peters, K., Willemse, T.A.C. (eds.) FORTE 2021. LNCS, vol. 12719, pp. 42–59. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-78089-0_3

    Chapter  Google Scholar 

  21. Broy, M., Cengarle, M.V.: UML formal semantics: lessons learned. Softw. Syst. Model. 10(4), 441–446 (2011). https://doi.org/10.1007/s10270-011-0207-y

    Article  Google Scholar 

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

  23. Cavada, R., Cimatti, A., Griggio, A., Susi, A.: A formal IDE for railways: Research challenges. In: Masci, P., Bernardeschi, C., Graziani, P., Koddenbrock, M., Palmieri, M. (eds.) SEFM Workshops. LNCS, vol. 13765, pp. 107–115. Springer (2022). https://doi.org/10.1007/978-3-031-26236-4_9

  24. Champelovier, D., et al.: Reference manual of the LOTOS NT to LOTOS translator (2023), https://cadp.inria.fr/ftp/publications/cadp/Champelovier-Clerc-Garavel-et-al-10.pdf, Accessed May 2023

  25. Chiappini, A., et al.: Formalization and validation of a subset of the European Train Control System. In: Proceedings of the 32nd International Conference on Software Engineering (ICSE). pp. 109–118. ACM (2010). https://doi.org/10.1145/1810295.1810312

  26. Cook, S.: Looking back at UML. Softw. Syst. Model. 11(4), 471–480 (2012). https://doi.org/10.1007/s10270-012-0256-x

    Article  Google Scholar 

  27. Derezińska, A., Szczykulski, M.: Interpretation Problems in Code Generation from UML State Machines: A Comparative Study. In: Kwater, T., Zuberek, W.M., Ciarkowski, A., Kruk, M., Pekala, R., Twaróg, B. (eds.) Proceedings of the 2nd Scientific Conference on Computing in Science and Technology (STI). pp. 36–50. Monographs in Applied Informatics, Warsaw University of Life Sciences (2012)

    Google Scholar 

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

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

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

  31. Ferrari, A., ter Beek, M.H.: Formal methods in railways: a systematic mapping study. ACM Comput. Surv. 55(4), 69:1–69:37 (2022). https://doi.org/10.1145/3520480

  32. Ferrari, A., Fantechi, A., Bacherini, S., Zingoni, N.: Modeling guidelines for code generation in the railway signaling context. In: Denney, E., Giannakopoulou, D., Pasareanu, C.S. (eds.) Proceedings of the 1st NASA Formal Methods Symposium (NFM). NASA Conference Proceedings, vol. CP-2009-215407, pp. 166–170 (2009), https://ntrs.nasa.gov/citations/20100024476

  33. Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H.: Systematic evaluation and usability analysis of formal methods tools for railway signaling system design. IEEE Trans. Softw. Eng. 48(11), 4675–4691 (2022). https://doi.org/10.1109/TSE.2021.3124677

    Article  Google Scholar 

  34. Filipovikj, P., Mahmud, N., Marinescu, R., Seceleanu, C., Ljungkrantz, O., Lönn, H.: Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 748–756. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_46

    Chapter  Google Scholar 

  35. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013). https://doi.org/10.1007/s10009-012-0244-z

    Article  Google Scholar 

  36. 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 (2022). https://doi.org/10.1007/978-3-030-58298-2_1

    Chapter  Google Scholar 

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

  38. Gleirscher, M., Marmsoler, D.: Formal methods in dependable systems engineering: a survey of professionals from Europe and North America. Empir. Softw. Eng. 25(6), 4473–4546 (2020). https://doi.org/10.1007/s10664-020-09836-5

    Article  Google Scholar 

  39. Gnesi, S., Mazzanti, F.: An Abstract, on the Fly Framework for the Verification of Service-Oriented Systems. In: Wirsing, M., Hölzl, M. (eds.) Rigorous Software Engineering for Service-Oriented Systems. LNCS, vol. 6582, pp. 390–407. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20401-2_18

    Chapter  Google Scholar 

  40. Horváth, B., et al.: Pragmatic verification and validation of industrial executable sysml models. Syst. Eng. (2023). https://doi.org/10.1002/sys.21679

  41. Huisman, M., Gurov, D., Malkis, A.: Formal Methods: From Academia to Industrial Practice. A Travel Guide (2020), https://arxiv.org/abs/2002.07279

  42. Leduc, G.: Information technology-enhancements to LOTOS (E-LOTOS). ISO/IEC International Standard (2001), https://www.iso.org/obp/ui/#iso:std:iso-iec:15437:ed-1:v1:en

  43. Mazzanti, F., Basile, D.: 4SECURail Deliverable D2.2 Formal development Demonstrator prototype, 1st Release (2020), https://www.4securail.eu/pdf/4SR-WP2-D2.2-Formal-development-demonstrator-prototype-1st%20release-CNR-3.0.pdf, Accessed May 2023

  44. Mazzanti, F., et al.: 4SECURail Deliverable D2.1 Specification of formal development demonstrator (2020), https://www.4securail.eu/pdf/4SR-WP2-D2.1-Specification%20of%20formal%20development%20demonstrator-CNR-1.0.pdf, Accessed May 2023

  45. Mazzanti, F., Belli, D.: 4SECURail Deliverable D2.5 Formal development demonstrator prototype, final release (2021), https://www.4securail.eu/pdf/4SR-WP2-D2.5-Formal-development-demonstrator-prototype.final-release-CNR-1.0.pdf, Accessed May 2023

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

  47. Mazzanti, F., Belli, D.: The 4SECURail formal methods demonstrator. In: Dutilleul, S.C., Haxthausen, A.E., Lecomte, T. (eds.) RSSRail. LNCS, vol. 13294, pp. 149–165. Springer (2022). https://doi.org/10.1007/978-3-031-05814-1_11

  48. Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010). https://doi.org/10.1145/1646353.1646372

    Article  Google Scholar 

  49. Object Management Group: Unified Modelling Language (2017), https://www.omg.org/spec/UML/About-UML/

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

  51. Object Management Group: Precise Semantics of UML State Machines (PSSM) (2019), https://www.omg.org/spec/PSSM

  52. Peres, F., Ghazel, M.: A proven translation from a UML state machine subset to timed automata. ACM Trans. Embed. Comput. Syst. (2023). https://doi.org/10.1145/3581771

    Article  Google Scholar 

  53. Piattino, A.: 4SECURail Deliverable D2.3 Case study requirements and specification (2020), https://www.4securail.eu/pdf/4SR-WP2-D2.3-Case-study-requirements-and-specification-SIRTI-1.0.pdf, Accessed May 2023

  54. Salunkhe, S., Berglehner, R., Rasheeq, A.: Automatic Transformation of SysML Model to Event-B Model for Railway CCS Application. In: Raschke, A., Méry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 143–149. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-77543-8_14

    Chapter  Google Scholar 

  55. Seisenberger, M., et al.: Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in Railway. In: Margaria, T., Steffen, B. (eds.) ISoLA. LNCS, vol. 13704, pp. 246–268. Springer (2022). https://doi.org/10.1007/978-3-031-19762-8_20

  56. Sheng, H., Bentkamp, A., Zhan, B.: HHLPy: practical verification of hybrid systems using Hoare logic. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM. LNCS, vol. 14000, pp. 160–178. Springer (2023). https://doi.org/10.1007/978-3-031-27481-7_11

  57. Snook, C.F., Butler, M.J.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006). https://doi.org/10.1145/1125808.1125811

    Article  Google Scholar 

  58. Snook, C.F., Butler, M.J., Hoang, T.S., Fathabadi, A.S., Dghaym, D.: Developing the UML-B modelling tools. In: Masci, P., Bernardeschi, C., Graziani, P., Koddenbrock, M., Palmieri, M. (eds.) SEFM Workshops. LNCS, vol. 13765, pp. 181–188. Springer (2022). https://doi.org/10.1007/978-3-031-26236-4_16

  59. Stramaglia, A., Keiren, J. J. A.: Formal verification of an industrial UML-like model using mCRL2. In: Groote, J.F., Huisman, M. (eds.) FMICS. LNCS, vol. 13487, pp. 86–102. Springer (2022). https://doi.org/10.1007/978-3-031-15008-1_7

  60. UNISIG: RBC-RBC Safe Communication Interface - SUBSET-098 (2012), https://www.era.europa.eu/system/files/2023-01/sos3_index063_-_subset-098_v300.pdf, Accessed May 2023

  61. UNISIG: FIS for the RBC/RBC Handover - SUBSET-039 (2015), https://www.era.europa.eu/system/files/2023-01/sos3_index012_-_subset-039_v320.pdf, Accessed May 2023

Download references

Acknowledgements

This work has been partially funded by the 4SECURail project (Shift2Rail GA 881775). Part of this study was carried out within the MOST - Sustainable Mobility National Research Center and received funding from the European Union Next-GenerationEU (Piano Nazionale di Ripresa e Resilienza (PNRR) - Missione 4 Componente 2, Investimento 1.4 - D.D. 1033 17/06/2022, CN00000023). The content of this paper reflects only the author’s view and the Shift2Rail Joint Undertaking is not responsible for any use that may be made of the included information.

Author information

Authors and Affiliations

  1. Formal Methods and Tools Lab ISTI – CNR, Pisa, Italy

    Davide Basile, Franco Mazzanti & Alessio Ferrari

Authors
  1. Davide Basile
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Franco Mazzanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alessio Ferrari
    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. Fondazione Bruno Kessler, Povo, Italy

    Alessandro Cimatti

  2. NASA Langley Research Center, AMA-NASA LaRC, Hampton, VA, USA

    Laura Titolo

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Basile, D., Mazzanti, F., Ferrari, A. (2023). Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect. In: Cimatti, A., Titolo, L. (eds) Formal Methods for Industrial Critical Systems. FMICS 2023. Lecture Notes in Computer Science, vol 14290. Springer, Cham. https://doi.org/10.1007/978-3-031-43681-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-43681-9_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-43680-2

  • Online ISBN: 978-3-031-43681-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation