Abstract
In the railway signalling domain, a railway interlocking system (RIS) is responsible for controlling the movement of trains by allowing or denying their routing according to safety rules. Relay diagrams are a commonly used abstraction in order to model relay-based RIS, describing these systems by graph-like schemata that present the connections between electrical components. The verification of these diagrams regarding safety, however, is a challenging task, due to their complexity and the lack of tools for the automatic proof and animation. The analysis of relay diagrams by a specialist is the main method to verify the correctness and the safety of these systems. Nonetheless, human manual analysis is error prone. This paper presents an approach for formally specifying the behaviour of the systems described in relay diagrams in the B-method formal language. Considering that each relay has only two states, it is possible to describe the rules for the state evolution of a system by logical propositions. Furthermore, it is possible to use ProB in order to animate and model-check the specification.
Supported by the LCHIP (Low Cost High Integrity Platform) project.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)
Beer, H.: The LTL Checker Plugins: A Reference Manual. Eindhoven University of Technology, Eindhoven (2004)
Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48119-2_22
Cavada, R., Cimatti, A., Sessa, M.: Analysis of relay interlocking systems via SMT-based model checking of switched multi-domain Kirchhoff networks. In: The Eighteenth in a Series of Conferences on the Theory and Applications of Formal Methods in Hardware and System Verification (FMCAD 2018), vol. 18, pp. 179–187. IEEE (2018)
ClearSy: B Language Reference Manual, version 1.8.5
Fantechi, A., Fokkink, W., Morzenti, A.: B-specification of relay-based railway interlocking systems based on the propositional logic of the system state evolution. In: Formal Methods for Industrial Critical Systems: A Survey of Applications, pp. 61–84 (2013)
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 (2017)
Gjaldbæk, T., Haxthausen, A.E.: Modelling and verification of interlocking systems for railway lines. IFAC Proc. Vol. 36(14), 233–238 (2003)
Guiho, G., Hennebert, C.: SACEM software validation. In: 1990 Proceedings of the 12th International Conference on Software Engineering, pp. 186–191. IEEE (1990)
Hansen, K.M.: Formalising railway interlocking systems. In: Nordic Seminar on Dependable Computing Systems, pp. 83–94. Citeseer (1998)
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 (2010). https://doi.org/10.1007/978-3-642-12566-9_8
Lecomte, T., Servat, T., Pouzancre, G., et al.: Formal methods in safety-critical railway systems. In: 10th Brasilian Symposium on Formal Methods, pp. 29–31 (2007)
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46
Rétiveau, R.: La signalisation ferroviaire. Presse de l’école nationale des Ponts et Chaussées (1987)
Schneider, S.: The B-Method: An Introduction. Palgrave, Basingstoke (2001)
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)
Winter, K.: Model checking railway interlocking systems. In: Australian Computer Science Communications, vol. 24, pp. 303–310. Australian Computer Society, Inc. (2002)
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
de Almeida Pereira, D.I., Deharbe, D., Perin, M., Bon, P. (2019). 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) 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_16
Download citation
DOI: https://doi.org/10.1007/978-3-030-18744-6_16
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)