{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:54:47Z","timestamp":1770339287400,"version":"3.49.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319459424","type":"print"},{"value":"9783319459431","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-45943-1_16","type":"book-chapter","created":{"date-parts":[[2016,9,12]],"date-time":"2016-09-12T17:31:17Z","timestamp":1473701477000},"page":"231-245","source":"Crossref","is-referenced-by-count":2,"title":["Formal Techniques for a Data-Driven Certification of Advanced Railway Signalling Systems"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Fantechi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,13]]},"reference":[{"key":"16_CR1","unstructured":"Bergenhem, C., Pettersson, H., Coelingh, E., Englund, C., Shladover, S., Tsugawa, S.: Overview of platooning systems. In: ITS World Congress, Vienna, 22\u201326 October 2012"},{"issue":"2","key":"16_CR2","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1023\/A:1008645826258","volume":"12","author":"C Bernardeschi","year":"1998","unstructured":"Bernardeschi, C., Fantechi, A., Gnesi, S., Larosa, S., Mongardi, G., Romano, D.: A formal verification environment for railway signaling system design. Formal Methods Syst. Des. 12(2), 139\u2013161 (1998)","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR3","volume-title":"Integrity Considerations for Secure Computer Systems","author":"K Biba","year":"1977","unstructured":"Biba, K.: Integrity Considerations for Secure Computer Systems. MITRE Co, Bedford (1977)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bock, U., Bikker, G.: Design, development of a future freight train concept- \u201cvirtually coupled train formations\u201d. In: Schnieder, E., Becker, U. (eds.): 9th IFAC Symposium Control in Transportation Systems, 13\u201315 June, S. 410\u2013415, Braunschweig (2000)","DOI":"10.1016\/S1474-6670(17)38176-4"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-319-05032-4_18","volume-title":"Software Engineering and Formal Methods","author":"A Bonacchi","year":"2014","unstructured":"Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M., Cipriani, L.: Validation of railway interlocking systems by formal verification, a case study. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 237\u2013252. Springer, Heidelberg (2014)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/978-3-319-23267-6_4","volume-title":"Computer Performance Engineering","author":"L Carnevali","year":"2015","unstructured":"Carnevali, L., Flammini, F., Paolieri, M., Vicario, E.: Non-markovian performability evaluation of ERTMS ETCS level 3. In: Beltr\u00e1n, M., Knottenbelt, W., Bradley, J. (eds.) EPEW 2015. LNCS, vol. 9272, pp. 47\u201362. Springer, Heidelberg (2015)"},{"issue":"2","key":"16_CR7","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1145\/226643.226647","volume":"43","author":"TD Chandra","year":"1996","unstructured":"Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225\u2013267 (1996)","journal-title":"J. ACM"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-3-319-24249-1_24","volume-title":"Computer Safety, Reliability, and Security","author":"B Chen","year":"2015","unstructured":"Chen, B., Schmittner, C., Ma, Z., Temple, W.G., Dong, X., Jones, D.L., Sanders, W.H.: Security analysis of urban railway systems: the need for a cyber-physical perspective. In: Koornneef, F., van Gulijk, C. (eds.) SAFECOMP Workshopps 2015. LNCS, vol. 9338, pp. 277\u2013290. Springer, Heidelberg (2015)"},{"key":"16_CR9","unstructured":"Esposito, R., Lazzaro, A., Marmo, P., Sanseviero, A.: Formal verification of ERTMS Euroradio safety critical protocol. In: Proceedings 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS 2003). L\u2019Harmattan Hongrie, Budapest (2003)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/978-3-642-34032-1_26","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","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, Part II. LNCS, vol. 7610, pp. 276\u2013289. Springer, Heidelberg (2012)"},{"key":"16_CR11","unstructured":"Fantechi, A., Gnesi, S., Haxthausen, A., van de Pol, J., Roveri, M., Treharne, H.: SaRDIn - a safe reconfigurable distributed interlocking. In: WCRR 2016, Milano, May 2016"},{"key":"16_CR12","first-page":"107","volume-title":"FORMS\/FORMAT 2010","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 2010, pp. 107\u2013115. Springer, Heidelberg (2010)"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Groote, J.F., van Vlijmen, S., Koorn, J.: The safety guaranteeing system at station Hoorn-Kersenboogerd. In: Logic Group Preprint Series 121. Utrecht University (1995)","DOI":"10.1109\/CMPASS.1995.521887"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Hase, K.R.: Open proof for railway safety software - a potential way-out of vendor lock-in advancing to standardization, transparency, and software security. In: 8th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS\/FORMAT 2010), 2\u20133 December 2010, Braunschweig, Germany (2010)","DOI":"10.1007\/978-3-642-14261-1_2"},{"issue":"8","key":"16_CR15","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1109\/32.879808","volume":"26","author":"A Haxthausen","year":"2000","unstructured":"Haxthausen, A., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Software Eng. 26(8), 687\u2013701 (2000)","journal-title":"IEEE Trans. Software Eng."},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/978-3-319-05032-4_16","volume-title":"Software Engineering and Formal Methods","author":"AE Haxthausen","year":"2014","unstructured":"Haxthausen, A.E., Peleska, J., Pinger, R.: Applied bounded model checking for interlocking system designs. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 205\u2013220. Springer, Heidelberg (2014)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Hei, X., Ma, W., Gao, J., Xie, G.: A concurrent scheduling model of distributed train control system. In: IEEE International Conference on Service Operations, Logistics, and Informatics (SOLI), pp. 478\u2013483 (2011)","DOI":"10.1109\/SOLI.2011.5986608"},{"issue":"3","key":"16_CR18","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport, L., Shostak, R., Pease, M.: The Byzantine general problem. ACM Trans. Program. Lang. Syst. 4(3), 382\u2013401 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/978-3-319-05032-4_19","volume-title":"Software Engineering and Formal Methods","author":"P James","year":"2014","unstructured":"James, P., Lawrence, A., Moller, F., Roggenbach, M., Seisenberger, M., Setzer, A., Kanso, K., Chadwick, S.: Verification of solid state interlocking programs. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 253\u2013268. Springer, Heidelberg (2014)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-319-05032-4_15","volume-title":"Software Engineering and Formal Methods","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M., Williams, D.: Verification of scheme plans using CSP||B. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 189\u2013204. Springer, Heidelberg (2014)"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 194\u2013206 (1973)","DOI":"10.1145\/512927.512945"},{"key":"16_CR22","unstructured":"DaSilva, C., Dehbonei, B., Mejia, F.: Formal specification in the development of industrial applications: subway speed control system. In: Proceedings 5th IFIP Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 1992), Perros-Guirec, pp. 199\u2013213, North-Holland (1993)"},{"key":"16_CR23","unstructured":"Michaut, P.: Method for managing the circulation of vehicles on a railway network and related system. US patent 8820685 B2 (2014)"},{"key":"16_CR24","unstructured":"Ohmstede, H.: Method for reducing data in railway operation. US patent 7578485 (2009)"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-319-33951-1_4","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"J Ruiter de","year":"2016","unstructured":"de Ruiter, J., Thomas, R.J., Chothia, T.: A formal security analysis of the ERTMS train to trackside protocols. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 53\u201368. Springer, Heidelberg (2016)"},{"issue":"2","key":"16_CR26","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1109\/MSP.2014.31","volume":"12","author":"WH Sanders","year":"2014","unstructured":"Sanders, W.H.: Quantitative security metrics: unattainable holy grail or a vital breakthrough within our reach? IEEE Secur. Priv. 12(2), 67\u201369 (2014)","journal-title":"IEEE Secur. Priv."},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-15651-9_1","volume-title":"Computer Safety, Reliability, and Security","author":"O Schulz","year":"2010","unstructured":"Schulz, O., Peleska, J.: Reliability analysis of safety-related communication architectures. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 1\u201314. Springer, Heidelberg (2010)"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Totel, E., Blanquart, J.-P., Deswarte, Y., Powell, D.: Supporting multiple levels of criticality, digest of papers. In: FTCS-28, The Twenty Eigth Annual International Symposium on Fault-Tolerant Computing, Munich, Germany, 23\u201325 June 1998, pp. 70\u201379. IEEE Computer Society (1998)","DOI":"10.1109\/FTCS.1998.689456"},{"key":"16_CR29","unstructured":"UIC: Virtually coupled trains. http:\/\/www.railway-energy.org\/static\/Virtually_coupled_trains_86.php"},{"issue":"4","key":"16_CR30","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M Weiser","year":"1984","unstructured":"Weiser, M.: Program slicing. IEEE Trans. Software Eng. 10(4), 352\u2013357 (1984)","journal-title":"IEEE Trans. Software Eng."},{"key":"16_CR31","unstructured":"Whitwam, F., Kanner, A.: Control of automatic guided vehicles without wayside interlocking. US patent 20120323411 A1 (2012)"},{"key":"16_CR32","unstructured":"Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Twenty-Sixth Australasian Computer Science Conference (ACSC 2003), pp. 309\u2013316 (2003)"},{"issue":"1","key":"16_CR33","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/j.jss.2003.12.039","volume":"77","author":"A Zimmermann","year":"2005","unstructured":"Zimmermann, A., Hommel, G.: Towards modeling and evaluation of ETCS real-time communication and operation. J. Syst. Softw. 77(1), 47\u201354 (2005)","journal-title":"J. Syst. Softw."}],"container-title":["Lecture Notes in Computer Science","Critical Systems: Formal Methods and Automated Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-45943-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T18:17:06Z","timestamp":1749579426000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-45943-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319459424","9783319459431"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-45943-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}