Abstract
In several large scale systems (e.g. robotic plants or transportation systems) safety is guaranteed by granting to some process or physical object an exclusive access to a particular set of physical areas or objects before starting its own action: some mechanism should in this case interlock the action of the former with the availability of the latter. A typical example is the railway interlocking problem, in which a train is granted the authorisation to move only if the tracks in front of the train are free. Although centralised control solutions have been implemented since decades, the current quest for autonomy and the possibility of distributing computational elements without wired connection for communication or energy supply has raised the interest in distributed solutions, that have to take into account the physical topology of the controlled areas and guarantee the same level of safety. In this paper the interlocking problem is formalised as a particular class of distributed mutual exclusion problems, addressing simultaneous locking of a pool of distributed objects, focusing on the formalisation and verification of the required safety properties. A family of distributed algorithms solving this problem is envisioned, with variants related to where the data defining the pool’s topology reside, and to how such data rules the communication between nodes. The different variants are exemplified with references to different distributed railway interlocking algorithms proposed in the literature. A final discussion is devoted to the steps needed to convert the proposed definitions into a generic plug-and-play safety-certified solution.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This feature allows for partial release of the pool of nodes, at the advantage of other processes that want to request those nodes, so increasing availability.
References
FP7 Project INESS - Deliverable D.1.5 report on translation of requirements from text to UML. Technical report (2009)
Banci, M., Fantechi, A., Gnesi, S.: The role of formal methods in developing a distribuited railway interlocking system. In: Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems, FORMS/FORMAT, Braunschweig, Germany, pp. 79–91 (2004)
Banci, M., Fantechi, A.: Geographical versus functional modelling by statecharts of interlocking systems. Electr. Notes Theor. Comput. Sci. 133, 3–19 (2005). https://doi.org/10.1016/j.entcs.2004.08.055
Basagiannis, S., Katsaros, P., Pombortsis, A.: Interlocking control by distributed signal boxes: design and verification with the SPIN model checker. In: Guo, M., Yang, L.T., Di Martino, B., Zima, H.P., Dongarra, J., Tang, F. (eds.) ISPA 2006. LNCS, vol. 4330, pp. 317–328. Springer, Heidelberg (2006). https://doi.org/10.1007/11946441_32
ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011). https://doi.org/10.1016/j.scico.2010.07.002
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
Fantechi, A.: Distributing the challenge of model checking interlocking control tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 276–289. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34032-1_26
Fantechi, A., Gnesi, S., Haxthausen, A., van de Pol, J., Roveri, M., Treharne, H.: SaRDIn - A safe reconfigurable distributed interlocking. In: Proceedings of 11th World Congress on Railway Research, WCRR. Ferrovie dello Stato Italiane, Milano (2016)
Fantechi, A., Haxthausen, A.E., Macedo, H.D.: Compositional verification of interlocking systems for large stations. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 236–252. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66197-1_15
Fantechi, A., Haxthausen, A.E., Nielsen, M.B.R.: Model checking geographically distributed interlocking systems using UMC. In: 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing, PDP, pp. 278–286 (2017). https://doi.org/10.1109/PDP.2017.66
Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT, pp. 107–115. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14261-1_11
Geisler, S., Haxthausen, A.E.: Stepwise development and model checking of a distributed interlocking system - using RAISE. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) Formal Methods. FM 2018. Lecture Notes in Computer Science, vol. 10951. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95582-7_16
Gray, J.N.: Notes on data base operating systems. In: Bayer, R., Graham, R.M., Seegmüller, G. (eds.) Operating Systems. LNCS, vol. 60, pp. 393–481. Springer, Heidelberg (1978). https://doi.org/10.1007/3-540-08755-9_9, http://dl.acm.org/citation.cfm?id=647433.723863
Haxthausen, A.E., Østergaard, P.H.: On the use of static checking in the verification of interlocking systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 266–278. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_19
Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687–701 (2000)
Hei, X., Takahashi, S., Nakamura, H.: Distributed interlocking system and its safety verification. In: Proceedings of 6th World Congress on Intelligent Control and Automation, Dalian, China, vol. 2, pp. 8612–8615 (2006). https://doi.org/10.1109/WCICA.2006.1713661
Hei, X., Ma, W., Gao, J., Xie, G.: A concurrent scheduling model of distributed train control system. In: Proceedings of IEEE International Conference on Service Operations, Logistics, and Informatics, SOLI, pp. 478–483 (2011)
Kanner, F.W.A.: Control of automatic guided vehicles without wayside interlocking, Patent US 20120323411 A1 (2012)
Lamport, L.: The implementation of reliable distributed multiprocess systems. Comput. Netw. 2, 95–114 (1978). https://doi.org/10.1016/0376-5075(78)90045-4
Lampson, B., Sturgis, H.: Crash recovery in a distributed storage system. Technical report, Comput. Sci. Lab., Xerox Parc, Palo Alto, CA (1976)
Maekawa, M.: A \(\sqrt{N}\) algorithm for mutual exclusion in decentralized systems. ACM Trans. Comput. Syst. 3(2), 145–159 (1985). https://doi.org/10.1145/214438.214445
Michaut, P.: Method for managing the circulation of vehicles on a railway network and related system, Patent US 8820685 B2 (2014)
Perna, J.I., George, C.: Model checking RAISE applicative specifications. In: Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods, SEFM, pp. 257–268. IEEE Computer Society Press (2007)
Ricart, G., Agrawala, A.K.: An optimal algorithm for mutual exclusion in computer networks. Commun. ACM 24(1), 9–17 (1981). https://doi.org/10.1145/358527.358537
Shift2Rail Joint Undertaking: Multi-annual action plan, November 2015. http://ec.europa.eu/research/participants/data/ref/h2020/other/wp/jtis/h2020-maap-shift2rail_en.pdf
Skeen, D., Stonebraker, M.: A formal model of crash recovery in a distributed systems. IEEE Trans. Softw. Eng. 9, 219–228 (1983)
George, C., Haff, P., Havelund, K., Haxthausen, A.E., Milne, R., Nielsen, C.B., Prehn, S., Wagner, K.R.: The RAISE Language Group. The RAISE Specification Language. The BCS Practitioners Series, Prentice Hall Int. (1992)
Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. (2016). https://doi.org/10.1016/j.scico.2016.05.010
Walz, H.V., Agostini, R.C., Barker, L., Cherkassky, R., Constant, T., Matheson, R.: Distributed supervisory protection interlock system SLC acceleration. Proceedings of the IEEE Particle Accelerator Conference: Accelerator Science and Technology, vol. 3, pp. 1928–1930 (1989). https://doi.org/10.1109/PAC.1989.72972
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Fantechi, A., Haxthausen, A.E. (2018). Safety Interlocking as a Distributed Mutual Exclusion Problem. In: Howar, F., Barnat, J. (eds) Formal Methods for Industrial Critical Systems. FMICS 2018. Lecture Notes in Computer Science(), vol 11119. Springer, Cham. https://doi.org/10.1007/978-3-030-00244-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-00244-2_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00243-5
Online ISBN: 978-3-030-00244-2
eBook Packages: Computer ScienceComputer Science (R0)