{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T16:25:28Z","timestamp":1764865528395,"version":"3.46.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032107619"},{"type":"electronic","value":"9783032107626"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-10762-6_9","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T16:08:11Z","timestamp":1763222891000},"page":"91-107","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Bridging Formal Verification and\u00a0Domain Validation in\u00a0Railway Systems"],"prefix":"10.1007","author":[{"given":"Asfand","family":"Yar","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2267-3639","authenticated-orcid":false,"given":"Akram","family":"Idani","sequence":"additional","affiliation":[]},{"given":"Yves","family":"Ledru","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Collart-Dutilleul","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"9_CR1","unstructured":"Cenelec - railways and hyperloop systems. https:\/\/www.cencenelec.eu\/areas-of-work\/cenelec-sectors\/transport-and-packaging-cenelec\/railways-and-hyperloop-systems\/. Accessed 06 July 2023"},{"key":"9_CR2","unstructured":"Deliverable d 2.1 specification of formal development demonstrator. https:\/\/projects.shift2rail.org\/download.aspx?id=560cdd44-83e7-4f5d-879e-d8dcdf2e2b1b. Accessed 24 July 2023"},{"key":"9_CR3","unstructured":"Design4Rail (formerly RaIL-AiD). https:\/\/design4rail.com"},{"key":"9_CR4","unstructured":"eulynx.eu. https:\/\/eulynx.eu\/. . Accessed 13 Jan 2023"},{"key":"9_CR5","unstructured":"Industrial Railway CAD software. https:\/\/www.railcomplete.com\/"},{"key":"9_CR6","unstructured":"Safecap platform. http:\/\/safecap.sourceforge.net\/index.shtml. Accessed 15 July 2023"},{"key":"9_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"9_CR8","unstructured":"Bj\u00f8rner, D.: Dynamics of railway nets: on an interface between automatic control and software engineering. In: CTS2003: 10th IFAC Symposium on Control in Transportation Systems, August, Seikei University. Elsevier, United Kingdom (2003)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Bosschaart, M., Quaglietta, E., Janssen, B., Goverde, R.M.: Efficient formalization of railway interlocking data in railml. Inf. Syst. 49, 126\u2013141 (2015)","DOI":"10.1016\/j.is.2014.11.007"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Bouwman, M., van\u00a0der Wal, D., Luttik, B., Stoelinga, M., Rensink, A.: A case in point: verification and testing of a eulynx interface. Formal Aspects Comput. 35(1), 2:1\u20132:38 (2023)","DOI":"10.1145\/3528207"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Chiappini, A., et al.: Formalization and validation of a subset of the European train control system. In: 2010 ACM\/IEEE 32nd International Conference on Software Engineering, vol.\u00a02, pp. 109\u2013118 (2010). https:\/\/doi.org\/10.1145\/1810295.1810312","DOI":"10.1145\/1810295.1810312"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/S1571-0661(05)82534-4","volume":"71","author":"S Eker","year":"2002","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The maude ltl model checker. Electron. Notes Theor. Comput. Sci. 71, 162\u2013187 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"651","DOI":"10.2495\/CR080631","volume":"103","author":"J Endresen","year":"2008","unstructured":"Endresen, J., et al.: Train control language - teaching computers interlocking. WIT Trans. Built Environ. 103, 651\u2013660 (2008)","journal-title":"WIT Trans. Built Environ."},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Graham, B.T.: Formal Methods and Verification. Springer, Boston (1992). https:\/\/doi.org\/10.1007\/978-1-4615-3576-8_1","DOI":"10.1007\/978-1-4615-3576-8_1"},{"key":"9_CR15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2004)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-030-18744-6_2","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"A Idani","year":"2019","unstructured":"Idani, A., Ledru, Y., Ait Wakrime, A., Ben Ayed, R., Bon, P.: Towards a tool-based domain specific approach for railway systems modeling and validation. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 23\u201340. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-18744-6_2"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-030-27008-7_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"A Idani","year":"2019","unstructured":"Idani, A., Ledru, Y., Ait Wakrime, A., Ben\u00a0Ayed, R., Collart-Dutilleul, S.: Incremental development of a safety critical system combining formal methods and DSMLs. In: Larsen, K.G., Willemse, T. (eds.) FMICS 2019. LNCS, vol. 11687, pp. 93\u2013109. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-27008-7_6"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Idani, A., Ledru, Y., Vega, G.: Alliance of model-driven engineering with a proof-based formal approach. Innov. Syst. Softw. Eng. 289\u2013307 (2020). https:\/\/doi.org\/10.1007\/s11334-020-00366-3","DOI":"10.1007\/s11334-020-00366-3"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-40793-2_12","volume-title":"Computer Safety, Reliability, and Security","author":"A Iliasov","year":"2013","unstructured":"Iliasov, A., Lopatkin, I., Romanovsky, A.: The SafeCap platform for modelling railway safety and capacity. In: Bitsch, F., Guiochet, J., Ka\u00e2niche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 130\u2013137. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40793-2_12"},{"key":"9_CR20","unstructured":"Iliasov, A., Romanovsky, A.: The safecap toolset for improving railway capacity while ensuring its safety (2012)"},{"key":"9_CR21","unstructured":"Iliasov, A., Taylor, D., Laibinis, L., Romanovsky, A.: Industrial-strength verification of solid state interlocking programs. arXiv preprint arXiv:2108.10091 (2021)"},{"issue":"1","key":"9_CR22","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1109\/TDSC.2022.3141555","volume":"20","author":"A Iliasov","year":"2023","unstructured":"Iliasov, A., Taylor, D., Laibinis, L., Romanovsky, A.: Practical verification of railway signalling programs. IEEE Trans. Depend. Secure Comput. 20(1), 695\u2013707 (2023). https:\/\/doi.org\/10.1109\/TDSC.2022.3141555","journal-title":"IEEE Trans. Depend. Secure Comput."},{"key":"9_CR23","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2012)"},{"key":"9_CR24","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-319-29510-7_6","volume-title":"Formal Techniques for Safety-Critical Systems","author":"P James","year":"2016","unstructured":"James, P., Lawrence, A., Roggenbach, M., Seisenberger, M.: Towards safety analysis of ERTMS\/ETCS level 2 in real-time maude. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 103\u2013120. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29510-7_6"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/s11786-014-0174-0","volume":"8","author":"P James","year":"2014","unstructured":"James, P., Roggenbach, M.: Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans. Math. Comput. Sci. 8, 11\u201338 (2014)","journal-title":"Math. Comput. Sci."},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-38088-4_30","volume-title":"NASA Formal Methods","author":"P James","year":"2013","unstructured":"James, P., Trumble, M., Treharne, H., Roggenbach, M., Schneider, S.: OnTrack: an open tooling environment for railway verification. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 435\u2013440. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_30"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-66197-1_6","volume-title":"Software Engineering and Formal Methods","author":"B Luteberget","year":"2017","unstructured":"Luteberget, B., Camilleri, J.J., Johansen, C., Schneider, G.: Participatory verification of railway infrastructure by representing regulations in\u00a0RailCNL. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 87\u2013103. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_6"},{"issue":"1","key":"9_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-017-0281-z","volume":"52","author":"B Luteberget","year":"2017","unstructured":"Luteberget, B., Johansen, C.: Efficient verification of railway infrastructure designs against standard regulations. Formal Methods Syst. Des. 52(1), 1\u201332 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0281-z","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR29","unstructured":"Object Managment Group: Unified Modeling Language (UML) (v251) (2017)"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-78800-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PC \u00d6lveczky","year":"2008","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The real-time maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332\u2013336. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_23"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings Eighth Workshop on Model-Based Testing, Rome, Italy, 17 March 2013. Electronic Proceedings in Theoretical Computer Science, vol.\u00a0111, pp. 3\u201328. Open Publishing Association (2013). https:\/\/doi.org\/10.4204\/EPTCS.111.1","DOI":"10.4204\/EPTCS.111.1"},{"key":"9_CR32","unstructured":"railML.org: railml 3 \u2013 the new generation of railway data exchange. railML.org (2023). https:\/\/www.railml.org\/en\/user\/about.html"},{"key":"9_CR33","unstructured":"Ranise, S., Tinelli, C.: The smt-lib standard: Version 1, 2 (2005)"},{"key":"9_CR34","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15, 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-642-25264-8_5","volume-title":"SDL 2011: Integrating System and Software Modeling","author":"A Svendsen","year":"2011","unstructured":"Svendsen, A., Haugen, \u00d8., M\u00f8ller-Pedersen, B.: Synthesizing software models: generating train station models automatically. In: Ober, I., Ober, I. (eds.) SDL 2011. LNCS, vol. 7083, pp. 38\u201353. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25264-8_5"},{"key":"9_CR36","volume-title":"Principles of Database and Knowledge-Base Systems","author":"JD Ullman","year":"1988","unstructured":"Ullman, J.D.: Principles of Database and Knowledge-Base Systems, vol. I. Computer Science Press Inc., Henderson (1988)"},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: A domain-specific language for generic interlocking models and their properties. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, pp. 99\u2013115. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68499-4_7","DOI":"10.1007\/978-3-319-68499-4_7"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133, Part 2, 91\u2013115 (2017)","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"9_CR39","unstructured":"Vu, L., Haxthausen, A., Peleska, J.: A domain-specific language for railway interlocking systems. In: Schnieder, E., Tarnai, G. (eds.) Proceedings of the 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems, FORMS\/FORMAT 2014, pp. 200\u2013209. Technische Universit\u00e4t Braunschweig (2014)"},{"key":"9_CR40","doi-asserted-by":"publisher","unstructured":"van\u00a0der Wal, D., Gerhold, M., Stoelinga, M., Rensink, A.: Conformance in the railway industry: single-input-change testing a eulynx controller. In: Proceedings of FMICS 2023. LNCS, vol. 14291, pp. 115\u2013131. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/s10009-025-00790-5","DOI":"10.1007\/s10009-025-00790-5"},{"key":"9_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction\u2014CADE-18","author":"C Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topi\u0107, D.: Spass Version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 275\u2013279. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_22"}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10762-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T16:23:47Z","timestamp":1764865427000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10762-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107619","9783032107626"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10762-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RSSRail","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reliability, Safety, and Security of Railway Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pisa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rssrail2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rssrail2025.isti.cnr.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}