Abstract
One promising option to improve performance and contain costs of current tramway signalling systems is to introduce an Autonomous Positioning System (APS) in substitution of traditional occupancy detecting sensors. APS is an onboard system that uses a plurality of sensors (such as GPS or inertial platform) and a Sensor Fusion Algorithm (SFA) to autonomously estimate the position of the tram with the needed levels of uncertainty and protection. Autonomous positioning however introduces, even in absence of faults, a quantitative uncertainty with respect to traditional sensors. This paper investigates this issue in the context of an industrial project: a model of the envisaged solution is adopted, and the Uppaal Statistical Model Checker is used to study possible hazards induced by the substitution of legacy track circuits with on-board satellite positioning equipment.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
https://gssc.esa.int/navipedia/index.php/Integrity#Protection_Level
Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1–6:39 (2018)
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_23
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)
Basile, D., ter Beek, M.H., Ciancia, V.: Statistical model checking of a moving block railway signalling scenario with Uppaal SMC. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 372–391. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03421-4_24
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
Basile, D., Di Giandomenico, F., Gnesi, S.: On quantitative assessment of reliability and energy consumption indicators in railway systems. In: Kharchenko, V., Kondratenko, Y., Kacprzyk, J. (eds.) Green IT Engineering: Social, Business and Industrial Applications. SSDC, vol. 171, pp. 423–447. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-00253-4_18
Basile, D., Giandomenico, F.D., Gnesi, S.: Dependable dynamic routing for urban transport systems through integer linear programming. In: Fantechi et al. [15], pp. 221–237
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)
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)
Biagi, M., Carnevali, L., Paolieri, M., Vicario, E.: Performability evaluation of the ERTMS/ETCS - level 3. Transp. Res. Part C: Emerg. Technol. 82, 314–336 (2017)
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_25
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_46
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppall SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397–415 (2015)
Fantechi, A., Lecomte, T., Romanovsky, A.B. (eds.): RSSRail 2017. LNCS, vol. 10598. Springer, Heidelberg (2017)
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_10
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_11
Legrand, C., Beugin, J., Conrard, B., Marais, J., Berbineau, M., El-Miloudi, E.K.: Approach for evaluating the safety of a satellite-based train localisation system through the extended integrity concept. In: Proceedings of ESREL 2015 - European Safety and Reliability Conference (2015)
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
Vicario, E., Sassoli, L., Carnevali, L.: Using stochastic state classes in quantitative evaluation of dense-time reactive systems. IEEE Trans. Softw. Eng. 35(5), 703–719 (2009)
Zimmermann, A., Hommel, G.: Towards modeling and evaluation of ETCS real-time communication and operation. J. Syst. Softw. 77(1), 47–54 (2005)
Aknowledgements
This work has been partially supported by the Tuscany Region project POR FESR 2014-2020 SISTER “SIgnaling & Sensing Technologies in Railway application”.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Basile, D., Fantechi, A., Rucher, L., Mandò, G. (2019). Statistical Model Checking of Hazards in an Autonomous Tramway Positioning System. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2019. Lecture Notes in Computer Science(), vol 11495. Springer, Cham. https://doi.org/10.1007/978-3-030-18744-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-18744-6_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-18743-9
Online ISBN: 978-3-030-18744-6
eBook Packages: Computer ScienceComputer Science (R0)