Advertisement

Statistical Model Checking of a Moving Block Railway Signalling Scenario with Uppaal SMC

Experience and Outlook
  • Davide Basile
  • Maurice H. ter BeekEmail author
  • Vincenzo Ciancia
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)

Abstract

We present an experience in modelling and statistical model checking a satellite-based moving block signalling scenario from the railway industry with Uppaal SMC. This demonstrates the usability and applicability of Uppaal SMC in the railway domain. We also propose a promising direction for future work, in which we envision spatio-temporal analysis with Uppaal SMC.

Notes

Acknowledgements

This work was partially funded by the Tuscany Region project SISTER and by the ASTRail project, which received funding from the Shift2Rail Joint Undertaking under the European Union’s Horizon 2020 research and innovation programme under Grant Agreement No. 777561. 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 thank our colleagues in the Formal Methods and Tools research group at ISTI-CNR, and the partners in these projects, for discussions on the models analysed in this paper.

References

  1. 1.
    Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1–6:39 (2018).  https://doi.org/10.1145/3158668MathSciNetCrossRefGoogle Scholar
  2. 2.
    Aiello, M., Pratt-Hartmann, I.E., van Benthem, J.F.A.K.: Handbook of Spatial Logics. Springer, Dordrecht (2007).  https://doi.org/10.1007/978-1-4020-5587-4CrossRefzbMATHGoogle Scholar
  3. 3.
    Arcaini, P., Jezek, P., Kofron, J.: Modelling the hybrid ERTMS/ETCS Level 3 case study in Spin. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 277–291. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-91271-4_19CrossRefGoogle Scholar
  4. 4.
    Bartholomeus, M., Luttik, B., Willemse, T.: Modelling and analysing ERTMS hybrid Level 3 with the mCRL2 toolset. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 98–114. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-00244-2_7CrossRefGoogle Scholar
  5. 5.
    Bartocci, E., Gol, E.A., Haghighi, I., Belta, C.: A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Trans. Control. Netw. Syst. 5(1), 308–320 (2018).  https://doi.org/10.1109/tcns.2016.2609138MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    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_2CrossRefGoogle Scholar
  7. 7.
    Basile, D., Chiaradonna, S., Di Giandomenico, F., Gnesi, S.: A stochastic model-based approach to analyse reliable energy-saving rail road switch heating systems. J. Rail Transp. Plan. Manag. 6(2), 163–181 (2016).  https://doi.org/10.1016/j.jrtpm.2016.03.003CrossRefGoogle Scholar
  8. 8.
    Basile, D., Di Giandomenico, F., Gnesi, S.: Tuning energy consumption strategies in the railway domain: a model-based approach. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 315–330. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47169-3_23CrossRefGoogle Scholar
  9. 9.
    Basile, D., Di Giandomenico, F., Gnesi, S.: A refinement approach to analyse critical cyber-physical systems. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 267–283. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-74781-1_19CrossRefGoogle Scholar
  10. 10.
    Basile, D., Di Giandomenico, F., Gnesi, S.: Statistical model checking of an energy-saving cyber-physical system in the railway domain. In: Proceedings of the 32nd Symposium on Applied Computing (SAC 2017), pp. 1356–1363. ACM (2017).  https://doi.org/10.1145/3019612.3019824
  11. 11.
    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
  12. 12.
    ter Beek, M.H., Gnesi, S., Knapp, A.: Formal methods for transport systems. Int. J. Softw. Tools Technol. Transf. 20(3) (2018).  https://doi.org/10.1007/s10009-018-0487-4CrossRefGoogle Scholar
  13. 13.
    ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: A framework for quantitative modeling and analysis of highly (re)configurable systems. IEEE Trans. Softw. Eng. (2018).  https://doi.org/10.1109/TSE.2018.2853726
  14. 14.
    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
  15. 15.
    Belmonte, G., Ciancia, V., Latella, D., Massink, M.: From collective adaptive systems to human centric computation and back: spatial model checking for medical imaging. In: ter Beek, M.H., Loreti, M. (eds.) Proceedings of the Workshop on FORmal Methods for the Quantitative Evaluation of Collective Adaptive SysTems (FORECAST 2016). Electronic Proceedings in Theoretical Computer Science, vol. 217, pp. 81–92 (2016).  https://doi.org/10.4204/EPTCS.217.10CrossRefGoogle Scholar
  16. 16.
    Belmonte, G., et al.: A topological method for automatic segmentation of glioblastoma in MR FLAIR for radiotherapy. Magn. Reson. Mater. Phys. Biol. Med. 30(Suppl. 1), 437 (2017).  https://doi.org/10.1007/s10334-017-0634-zCrossRefGoogle Scholar
  17. 17.
    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
  18. 18.
    Boulanger, J.L. (ed.): Formal Methods Applied to Industrial Complex Systems - Implementation of the B Method. Wiley, Hoboken (2014).  https://doi.org/10.1002/9781119002727CrossRefGoogle Scholar
  19. 19.
    Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 260–275. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-35632-2_25CrossRefGoogle Scholar
  20. 20.
    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. 20(3) (2018).  https://doi.org/10.1007/s10009-018-0483-8CrossRefGoogle Scholar
  21. 21.
    Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Bianculli, D., Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9509, pp. 297–311. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-49224-6_24CrossRefGoogle Scholar
  22. 22.
    Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model checking spatial logics for closure spaces. Log. Methods Comput. Sci. 12(4), 1–51 (2016).  https://doi.org/10.2168/LMCS-12(4:2)2016MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 156–201. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-34096-8_6CrossRefzbMATHGoogle Scholar
  24. 24.
    Ciancia, V., Latella, D., Massink, M., Paškauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 657–673. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47166-2_46CrossRefGoogle Scholar
  25. 25.
    Clark, G., et al.: The Möbius modeling tool. In: Proceedings of the 9th International Workshop on Petri Nets and Performance Models (PNPM 2001), pp. 241–250. IEEE (2001).  https://doi.org/10.1109/PNPM.2001.953373
  26. 26.
    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-10575-8CrossRefzbMATHGoogle Scholar
  27. 27.
    Cunha, A., Macedo, N.: Validating the hybrid ERTMS/ETCS Level 3 concept with Electrum. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 307–321. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-91271-4_21CrossRefGoogle Scholar
  28. 28.
    David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: UPPAAL SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397–415 (2015).  https://doi.org/10.1007/s10009-014-0361-yCrossRefGoogle Scholar
  29. 29.
    Douglass, B.P.: Real-time UML. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 53–70. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45739-9_4CrossRefGoogle Scholar
  30. 30.
    EEIG ERTMS Users Group: ERTMS/ETCS RAMS Requirements Specification – Chapter 2 - RAM, 30 September 1998. http://www.era.europa.eu/Document-Register/Documents/B1-02s1266-.pdf
  31. 31.
    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
  32. 32.
    European Committee for Electrotechnical Standardization: CENELEC EN 50126–1 – Railway applications - The specification and demonstration of Reliability, Availability, Maintainability and Safety (RAMS) - Part 1: Generic RAMS process, 1 October 2017. https://standards.globalspec.com/std/10262901/cenelec-en-50126-1
  33. 33.
    European Committee for Electrotechnical Standardization: CENELEC EN 50126–2 – Railway applications - The specification and demonstration of Reliability, Availability, Maintainability and Safety (RAMS) - Part 2: Systems approach to safety, 1 October 2017. https://standards.globalspec.com/std/10262978/cenelec-en-50126-2
  34. 34.
    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_13CrossRefGoogle Scholar
  35. 35.
    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_18CrossRefGoogle Scholar
  36. 36.
    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, Hoboken (2013).  https://doi.org/10.1002/9781118459898.ch4CrossRefGoogle Scholar
  37. 37.
    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-1CrossRefGoogle Scholar
  38. 38.
    Fränzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC 2011), pp. 43–52. ACM (2011).  https://doi.org/10.1145/1967701.1967710
  39. 39.
    Ghazel, M.: Formalizing a subset of ERTMS/ETCS specifications for verification purposes. Transp. Res. Part C Emerg. Technol. 42, 60–75 (2014).  https://doi.org/10.1016/j.trc.2014.02.002CrossRefGoogle Scholar
  40. 40.
    Ghazel, M.: A control scheme for automatic level crossings under the ERTMS/ETCS Level 2/3 operation. IEEE Trans. Intell. Transp. Syst. 18(10), 2667–2680 (2017).  https://doi.org/10.1109/TITS.2017.2657695CrossRefGoogle Scholar
  41. 41.
    Ghosh, S., Dasgupta, P., Mandal, C., Katiyar, A.: Formal verification of movement authorities in automatic train control systems. In: Proceedings of the 5th International Conference on Railway Engineering (ICRE 2016), pp. 1–8. IET (2016).  https://doi.org/10.1049/cp.2016.0511
  42. 42.
    Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97–105 (2009).  https://doi.org/10.1145/1467247.1467271CrossRefzbMATHGoogle Scholar
  43. 43.
    Hordvik, S., Øseth, K., Svendsen, H.H., Blech, J.O., Herrmann, P.: Model-based engineering and spatiotemporal analysis of transport systems. In: Maciaszek, L.A., Filipe, J. (eds.) ENASE 2016. CCIS, vol. 703, pp. 44–65. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-56390-9_3CrossRefGoogle Scholar
  44. 44.
    Larsen, K.G., Legay, A.: Statistical model checking past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 135–142. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-45231-8_10CrossRefGoogle Scholar
  45. 45.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16612-9_11CrossRefGoogle Scholar
  46. 46.
    Mammar, A., Frappier, M., Tueno Fotso, S.J., Laleau, R.: An Event-B model of the hybrid ERTMS/ETCS Level 3 standard. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 353–366. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-91271-4_24CrossRefGoogle Scholar
  47. 47.
    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.4CrossRefGoogle Scholar
  48. 48.
    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) (2018).  https://doi.org/10.1007/s10009-018-0488-3CrossRefGoogle Scholar
  49. 49.
    Nardone, R., et al.: Modeling railway control systems in Promela. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 121–136. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-29510-7_7CrossRefGoogle Scholar
  50. 50.
    Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 21–37. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-23820-3_2CrossRefGoogle Scholar
  51. 51.
    Rispoli, F., Castorina, M., Neri, A., Filip, A., Di Mambro, G., Senesi, F.: Recent progress in application of GNSS and advanced communications for railway signaling. In: Proceedings of the 23rd International Conference Radioelektronika (RADIOELEKTRONIKA 2013), pp. 13–22. IEEE (2013).  https://doi.org/10.1109/RadioElek.2013.6530882
  52. 52.
    Selic, B.: The real-time UML standard: definition and application. In: Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE 2002), pp. 770–772 (2002).  https://doi.org/10.1109/DATE.2002.998385
  53. 53.
    Shift2Rail Joint Undertaking: Multi-Annual Action Plan, 26 November 2015. http://ec.europa.eu/research/participants/data/ref/h2020/other/wp/jtis/h2020-maap-shift2rail_en.pdf
  54. 54.
    UNISIG: FIS for the RBC/RBC handover, version 3.1.0, 15 June 2016. http://www.era.europa.eu/Document-Register/Pages/set-2-FIS-for-the-RBC-RBC-handover.aspx

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Davide Basile
    • 1
    • 2
  • Maurice H. ter Beek
    • 1
    Email author
  • Vincenzo Ciancia
    • 1
  1. 1.ISTI–CNRPisaItaly
  2. 2.Department of Statistics, Computer Science and Applications (DISIA)University of FlorenceFlorenceItaly

Personalised recommendations