{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,7]],"date-time":"2025-07-07T04:02:26Z","timestamp":1751860946523,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030002435"},{"type":"electronic","value":"9783030002442"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00244-2_4","type":"book-chapter","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T04:12:38Z","timestamp":1535602358000},"page":"52-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Safety Interlocking as a Distributed Mutual Exclusion Problem"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Fantechi","sequence":"first","affiliation":[]},{"given":"Anne E.","family":"Haxthausen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,30]]},"reference":[{"key":"4_CR1","unstructured":"FP7 Project INESS - Deliverable D.1.5 report on translation of requirements from text to UML. Technical report (2009)"},{"key":"4_CR2","unstructured":"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\u201391 (2004)"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2004.08.055","volume":"133","author":"M Banci","year":"2005","unstructured":"Banci, M., Fantechi, A.: Geographical versus functional modelling by statecharts of interlocking systems. Electr. Notes Theor. Comput. Sci. 133, 3\u201319 (2005). https:\/\/doi.org\/10.1016\/j.entcs.2004.08.055","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/11946441_32","volume-title":"Parallel and Distributed Processing and Applications","author":"S Basagiannis","year":"2006","unstructured":"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\u2013328. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11946441_32"},{"issue":"2","key":"4_CR5","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"MH Beek ter","year":"2011","unstructured":"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\u2013135 (2011). https:\/\/doi.org\/10.1016\/j.scico.2010.07.002","journal-title":"Sci. Comput. Program."},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-49646-7_23","volume-title":"Computer Safety, Reliability and Security","author":"F Dijk van","year":"1998","unstructured":"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\u2013305. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49646-7_23"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-34032-1_26","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"A Fantechi","year":"2012","unstructured":"Fantechi, A.: Distributing the challenge of model checking interlocking control tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 276\u2013289. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34032-1_26"},{"key":"4_CR8","unstructured":"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)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-319-66197-1_15","volume-title":"Software Engineering and Formal Methods","author":"A Fantechi","year":"2017","unstructured":"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\u2013252. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_15"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"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\u2013286 (2017). https:\/\/doi.org\/10.1109\/PDP.2017.66","DOI":"10.1109\/PDP.2017.66"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14261-1_11","volume-title":"FORMS\/FORMAT","author":"A Ferrari","year":"2010","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS\/FORMAT, pp. 107\u2013115. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14261-1_11"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.1007\/978-3-319-95582-7_16"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Gray, J.N.: Notes on data base operating systems. In: Bayer, R., Graham, R.M., Seegm\u00fcller, G. (eds.) Operating Systems. LNCS, vol. 60, pp. 393\u2013481. Springer, Heidelberg (1978). https:\/\/doi.org\/10.1007\/3-540-08755-9_9 , http:\/\/dl.acm.org\/citation.cfm?id=647433.723863","DOI":"10.1007\/3-540-08755-9_9"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-319-47169-3_19","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"AE Haxthausen","year":"2016","unstructured":"Haxthausen, A.E., \u00d8stergaard, 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\u2013278. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47169-3_19"},{"issue":"8","key":"4_CR15","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1109\/32.879808","volume":"26","author":"AE Haxthausen","year":"2000","unstructured":"Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687\u2013701 (2000)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"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\u20138615 (2006). https:\/\/doi.org\/10.1109\/WCICA.2006.1713661","DOI":"10.1109\/WCICA.2006.1713661"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"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\u2013483 (2011)","DOI":"10.1109\/SOLI.2011.5986608"},{"key":"4_CR18","unstructured":"Kanner, F.W.A.: Control of automatic guided vehicles without wayside interlocking, Patent US 20120323411 A1 (2012)"},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0376-5075(78)90045-4","volume":"2","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: The implementation of reliable distributed multiprocess systems. Comput. Netw. 2, 95\u2013114 (1978). https:\/\/doi.org\/10.1016\/0376-5075(78)90045-4","journal-title":"Comput. Netw."},{"key":"4_CR20","unstructured":"Lampson, B., Sturgis, H.: Crash recovery in a distributed storage system. Technical report, Comput. Sci. Lab., Xerox Parc, Palo Alto, CA (1976)"},{"issue":"2","key":"4_CR21","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/214438.214445","volume":"3","author":"M Maekawa","year":"1985","unstructured":"Maekawa, M.: A $$\\sqrt{N}$$ algorithm for mutual exclusion in decentralized systems. ACM Trans. Comput. Syst. 3(2), 145\u2013159 (1985). https:\/\/doi.org\/10.1145\/214438.214445","journal-title":"ACM Trans. Comput. Syst."},{"key":"4_CR22","unstructured":"Michaut, P.: Method for managing the circulation of vehicles on a railway network and related system, Patent US 8820685 B2 (2014)"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"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\u2013268. IEEE Computer Society Press (2007)","DOI":"10.1109\/SEFM.2007.25"},{"issue":"1","key":"4_CR24","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/358527.358537","volume":"24","author":"G Ricart","year":"1981","unstructured":"Ricart, G., Agrawala, A.K.: An optimal algorithm for mutual exclusion in computer networks. Commun. ACM 24(1), 9\u201317 (1981). https:\/\/doi.org\/10.1145\/358527.358537","journal-title":"Commun. ACM"},{"key":"4_CR25","unstructured":"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"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1109\/TSE.1983.236608","volume":"9","author":"D Skeen","year":"1983","unstructured":"Skeen, D., Stonebraker, M.: A formal model of crash recovery in a distributed systems. IEEE Trans. Softw. Eng. 9, 219\u2013228 (1983)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR27","unstructured":"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)"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"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\u20131930 (1989). https:\/\/doi.org\/10.1109\/PAC.1989.72972","DOI":"10.1109\/PAC.1989.72972"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00244-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T17:44:30Z","timestamp":1751823870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00244-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030002435","9783030002442"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00244-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}