Abstract
Although Formal Methods have been used for decades in the development of industrial critical systems, there are still many products that do not use this technology. The use of Formal Methods in such a context is generally highly recommended, but not mandatory, as other technologies may be used as support to certify the safety of the systems. Relay-based railway interlocking systems, for instance, are legacy systems used in the majority of railway installations and whose safety has been attested through their use for decades. Their maintenance, however, requires analysis to avoid losing their safety features. In previous papers, we have presented the CLEARSY Safety Platform (CSSP) and how it can be used to analyse and replace these legacy interlocking systems in a safety-proved manner using certified industrial tools. In this paper, we extend this discussion to present how the CSSP can be used to monitor the legacy relay-based RIS to improve their safety during their execution. The strategy is to describe the system safety properties using logic and then implement it in the CSSP, which in turn is responsible for monitoring the system components to ensure its correct functioning and raise flags when an unsafe state is found. The benefits of using our approach in industry are discussed as we present how it can be applied in two industrial case studies.
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
Abrial, J.R., Lee, M., Neilson, D., Scharbach, P., Sørensen, I.: The B-method. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 398–405. Springer, Heidelber (1991). https://doi.org/10.1007/BFb0020001
Amendola, A., Becchi, A., et al.: NORMA: a tool for the analysis of relay-based railway interlocking systems. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 125–142. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_7
Bezerra, P.E.R., Oliveira, M.V.M., Lecomte, T., de Almeida Pereira, D.I.: CSP specification and verification of a relay-based railway interlocking system. In: Barbosa, H., Zohar, Y. (eds.) SBMF 2023. LNCS, vol. 14414, pp. 36–54. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-49342-3_3
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
Cavada, R., Cimatti, A., Mover, S., Sessa, M., Cadavero, G., Scaglione, G.: Analysis of relay interlocking systems via SMT-based model checking of switched multi-domain Kirchhoff networks. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1–9. IEEE (2018)
Cenelec, E.N.: 50128-railway applications-communication, signalling and processing systems-software for railway control and protection systems. Book EN, 50128 (2012)
ClearSy. Atelier B User Manual, version 4.0. ClearSy System Engineering, Parc de la Duranne - 320 av. Archimède - Les Pléïades III Bat A - 13857 AIX EN PROVENCE CEDEX 3 - France
de Almeida Pereira, D.I.: Analysis and formal specification of relay-based railway interlocking systems. Ph.D. thesis, Centrale Lille Institut (2020)
de Almeida Pereira, D.I., Debbech, S., Perin, M., Bon, P., Collart-Dutilleul, S.: Formal specification of environmental aspects of a railway interlocking system based on a conceptual model. In: Laender, A., Pernici, B., Lim, E.P., de Oliveira, J. (eds.) ER 2019. LNCS, vol. 11788, pp. 338–351. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-33223-5_28
de Almeida Pereira, D.I., Deharbe, D., Perin, M., Bon, P.: B-specification of relay-based railway interlocking systems based on the propositional logic of the system state evolution. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 242–258. Springer, Heidelberg (2019). https://doi.org/10.1007/978-3-030-18744-6_16
Ghosh, S., Das, A., Basak, N., Dasgupta, P., Katiyar, A.: Formal methods for validation and test point prioritization in railway signaling logic. IEEE Trans. Intell. Transp. Syst. 18(3), 678–689 (2016)
Haxthausen, A.E., Kjær, A.A., Le Bliguet, M.: Formal development of a tool for automated modelling and verification of relay interlocking systems. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 118–132. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_11
Haxthausen, A.E., Le Bliguet, M., Kjær, A.A.: Modelling and verification of relay interlocking systems. In: Choppy, C., Sokolsky, O. (eds.) Monterey Workshop 2008. LNCS, vol. 6028, pp. 141–153. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-642-12566-9_8
Lecomte, T.: Atelier B. In: Formal Methods Applied to Complex Systems: Implementation of the B Method, pp. 35–46 (2014)
Lecomte, T.: Programming the CLEARSY safety platform with B. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 124–138. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_9
Lecomte, T., Deharbe, D., Fournier, P., Oliveira, M.: The CLEARSY safety platform: 5 years of research, development and deployment. Sci. Comput. Program. 199, 102524 (2020)
Lecomte, T., et al.: Low cost high integrity platform. arXiv preprint arXiv:2005.07191 (2020)
Lecomte, T., Lavaud, B., Sabatier, D., Burdy, L.: A safety flasher developed with the CLEARSY safety platform. In: ter Beek, M.H., Ničković, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 210–227. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58298-2_9
Mirabadi, A., Yazdi, M.: Automatic generation and verification of railway interlocking control tables using FSM and NUSMV. Transp. Probl. 4, 103–110 (2009)
Rétiveau, R.: La signalisation ferroviaire. Presse de l’école nationale des Ponts et Chaussées (1987)
Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 3rd edn. Prentice Hall (2010)
She, X., Sha, Y., Chen, Q., Yang, J.: The application of graphic theory on railway yard interlocking control system. In: 2007 IEEE Intelligent Vehicles Symposium, pp. 883–887. IEEE (2007)
Sun, P., Collart-Dutilleul, S., Bon, P.: A model pattern of railway interlocking system by petri nets. In: 2015 International Conference on Models and Technologies for Intelligent Transportation Systems (MT-ITS), pp. 442–449. IEEE (2015)
Theeg, G., Vlasenko, S.: Railway Signalling & Interlocking: International Compendium (2019)
Van Eijk, P.H.J.: Verifying relay circuits using state machines. Logic Group Preprint Ser. 173 (1997)
Winter, K.: Model checking railway interlocking systems. Austral. Comput. Sci. Comm. 24(1), 303–310 (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Almeida, D., Jamain, F., Lecomte, T. (2024). Formal Analysis and Monitoring of Legacy Safety-Critical Interlocking Systems with the Use of Certified Industrial Tools. In: Haxthausen, A.E., Serwe, W. (eds) Formal Methods for Industrial Critical Systems. FMICS 2024. Lecture Notes in Computer Science, vol 14952. Springer, Cham. https://doi.org/10.1007/978-3-031-68150-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-031-68150-9_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-68149-3
Online ISBN: 978-3-031-68150-9
eBook Packages: Computer ScienceComputer Science (R0)