Skip to main content

Safety Interlocking as a Distributed Mutual Exclusion Problem

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11119))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 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

  1. FP7 Project INESS - Deliverable D.1.5 report on translation of requirements from text to UML. Technical report (2009)

    Google Scholar 

  2. 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)

    Google Scholar 

  3. 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

    Article  Google Scholar 

  4. 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

    Chapter  Google Scholar 

  5. 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

    Article  MATH  Google Scholar 

  6. 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

    Chapter  Google Scholar 

  7. 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

    Chapter  Google Scholar 

  8. 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)

    Google Scholar 

  9. 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

    Chapter  Google Scholar 

  10. 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

  11. 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

    Chapter  Google Scholar 

  12. 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

  13. 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

  14. 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

    Chapter  Google Scholar 

  15. Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687–701 (2000)

    Article  Google Scholar 

  16. 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

  17. 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)

    Google Scholar 

  18. Kanner, F.W.A.: Control of automatic guided vehicles without wayside interlocking, Patent US 20120323411 A1 (2012)

    Google Scholar 

  19. 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

    Article  MathSciNet  Google Scholar 

  20. Lampson, B., Sturgis, H.: Crash recovery in a distributed storage system. Technical report, Comput. Sci. Lab., Xerox Parc, Palo Alto, CA (1976)

    Google Scholar 

  21. 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

    Article  Google Scholar 

  22. Michaut, P.: Method for managing the circulation of vehicles on a railway network and related system, Patent US 8820685 B2 (2014)

    Google Scholar 

  23. 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)

    Google Scholar 

  24. 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

    Article  MathSciNet  Google Scholar 

  25. 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

  26. Skeen, D., Stonebraker, M.: A formal model of crash recovery in a distributed systems. IEEE Trans. Softw. Eng. 9, 219–228 (1983)

    Article  Google Scholar 

  27. 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)

    Google Scholar 

  28. 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

  29. 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

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Alessandro Fantechi .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics