Abstract
Interlocking control prevents certain operations from occurring, unless preceded by specific events. It is used in traffic network control systems (e.g. railway interlocking control), piping and tunneling control systems and in other applications like for example communication network control. Interlocking systems have to comply with certain safety properties and this fact elevates formal modeling as the most important concern in their design. This paper introduces an interlocking control algorithm based on the use of what we call Distributed Signal Boxes (DSBs). Distributed control eliminates the intrinsic complexity of centralized interlocking control solutions, which are mainly developed in the field of railway traffic control. Our algorithm uses types of network control units, which do not store state information. Control units are combined according to a limited number of patterns that in all cases yield safe network topologies. Verification of safety takes place by model checking a network that includes all possible interconnections between neighbor nodes. Obtained results can be used to generalize correctness by compositional reasoning for networks of arbitrary complexity that are formed according to the verified interconnection cases.
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
Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. 2(3), 359–385 (1980)
Arozarena, P., et al.: Madeira: A peer-to-peer approach to network management. In: Proceedings of the Wireless World Research Forum (2006)
Basagiannis, S., Katsaros, P., Pombortsis, A.: Interlocking control by distributed signal boxes: Design and verification with the spin model checker. In: Parallel and Distributed Processing and Applications, pp. 317–328 (2006)
Campos, S., Clarke, E., Minea, M.: The verus tool: a quantitative approach to the formal verification of real-time systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 452–455. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_46
Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Formal Aspects of Comput. 10(4), 361–380 (1998)
Cribbens, A.: Microprocessors in railway signalling: the solid-state interlocking. Microprocess. Microsyst. 11(5), 264–272 (1987)
van Dijk, F., Fokkink, W., Kolk, G., van de Ven, P., van Vlijmen, B.: EURIS, a specification method for distributed interlockings. In: Ehrenberger, W. (ed.) SAFECOMP 1998. LNCS, vol. 1516, pp. 296–305. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49646-7_23
Gnesi, S., Latella, D., Lenzini, G., Abbaneo, C., Amendola, A., Marmo, P.: A formal specification and validation of a critical system in presence of byzantine errors. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 535–549. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_36
Hansen, K.M.: Formalizing railway interlocking systems. In: Proceedings of FME Rail Workshop #2. FME: Formal Methods Europe (1998)
Hartonas-Garmhausen, V., Campos, S., Cimatti, A., Clarke, E., Giunchiglia, F.: Verification of a safety-critical railway interlocking system with real-time constraints. Sci. Comput. Programm. 36(1), 53–64 (2000)
Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Soft. Eng. 26(8), 687–701 (2000)
Hecht, M., Agron, J., Hecht, H., Kim, K.H.: A distributed fault tolerant architecture for nuclear reactor and other critical process control applications. In: [1991] Digest of Papers. The 21st International Symposium of Fault-Tolerant Computing, pp. 462–498, June 1991
Hlavaty, T., Preucil, L., Stepan, P., Klapka, S.: Formal methods in development and testing of safety-critical systems : railway interlocking system. In: Conference on Intelligent Methods for Quality Improvement in Industrial Practice, pp. 14–25 (2002)
Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)
Jain, A., Nelson, K., Bryant, R.E.: Verifying nondeterministic implementations of deterministic systems. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 109–125. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0031803
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. SE 7(4), 417–426 (1981)
Roever, W.P., et al.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, New York (2001)
Simpson, A.: Model checking for interlocking safety. In: Proceedings of FME Rail Workshop #2. FME: Formal Methods Europe (1998)
Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Proceedings of 26th Australasian Computer Science Conference, ACSC 2003, vol. 16, pp. 309–316 (2003)
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
Basagiannis, S., Katsaros, P. (2019). Formal Verification of Network Interlocking Control by Distributed Signal Boxes. In: Papadopoulos, Y., Aslansefat, K., Katsaros, P., Bozzano, M. (eds) Model-Based Safety and Assessment. IMBSA 2019. Lecture Notes in Computer Science(), vol 11842. Springer, Cham. https://doi.org/10.1007/978-3-030-32872-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-32872-6_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32871-9
Online ISBN: 978-3-030-32872-6
eBook Packages: Computer ScienceComputer Science (R0)