{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T03:36:16Z","timestamp":1770348976947,"version":"3.49.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986840","type":"print"},{"value":"9783031986857","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this paper we describe an industrial experience in\u00a0the verification of the logic of a Railway Protection System (RPS). The RPS is designed within AIDA, a structured model-based design workflow and toolset. The RPS is written in a domain specific language amenable to signaling engineers, that is converted\u00a0into Extended Finite State Machines (EFSM), and then into executable code. The RPS is parameterized, i.e., it can be applied,\u00a0after configuration, in different operational scenarios. The logic\u00a0is divided in classes, that are instantiated depending on the specific application. The verification challenge is to ensure that the required properties hold <jats:italic>for all possible instantiations<\/jats:italic>. We follow a verification approach based on the use of deductive methods, leveraging the Dafny framework. The AIDA environment is used to translate the RPS logic into Dafny, and also\u00a0to <jats:italic>automatically generate<\/jats:italic> the contracts summarizing the methods implementing the guards and effects of the EFSM transitions. This approach greatly limits the need for human interaction with\u00a0the underlying Dafny proof engine. In addition to domain specific optimizations, it results in an automated and efficient proof of the RPS properties.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_17","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:32:29Z","timestamp":1753155149000},"page":"364-376","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Automated Parameterized Verification of\u00a0a\u00a0Railway Protection System with\u00a0Dafny"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Cavada","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1315-6990","authenticated-orcid":false,"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3311-0893","authenticated-orcid":false,"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3719-7682","authenticated-orcid":false,"given":"Christian","family":"Lidstr\u00f6m","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2856-5236","authenticated-orcid":false,"given":"Gianluca","family":"Redondi","sequence":"additional","affiliation":[]},{"given":"Giuseppe","family":"Scaglione","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Tessi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-3868-866X","authenticated-orcid":false,"given":"Dylan","family":"Trenti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-030-61467-6_16","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"A Amendola","year":"2020","unstructured":"Amendola, A., et al.: A model-based approach to the design, verification and deployment of railway interlocking system. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 240\u2013254. Springer International Publishing, Cham (2020)"},{"key":"17_CR2","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, http:\/\/frama-c.com\/download\/acsl.pdf"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-031-65630-9_11","volume-title":"Computer Aided Verification","author":"A Becchi","year":"2024","unstructured":"Becchi, A., Cimatti, A., Scaglione, G.: Testing the migration from analog to software-based railway interlocking systems. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 219\u2013232. Springer Nature Switzerland, Cham (2024)"},{"issue":"2","key":"17_CR4","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1145\/2951860.2951873","volume":"47","author":"R Bloem","year":"2016","unstructured":"Bloem, R., et al.: Decidability in parameterized verification. SIGACT News 47(2), 53\u201364 (2016). https:\/\/doi.org\/10.1145\/2951860.2951873","journal-title":"SIGACT News"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M.: Validation process for railway interlocking systems. Sci. Comput. Program. 128, 2\u201321 (2016)","DOI":"10.1016\/j.scico.2016.04.004"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Griggio, A., Susi, A.: A formal IDE for railways: research challenges. In: Masci, P., Bernardeschi, C., Graziani, P., Koddenbrock, M., Palmieri, M. (eds.) Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, pp. 107\u2013115. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-26236-4_9"},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1016\/j.scico.2013.09.019","volume":"80","author":"A Classen","year":"2014","unstructured":"Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.: Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80, 416\u2013439 (2014)","journal-title":"Sci. Comput. Program."},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Cok, D.R.: JML and OpenJML for Java 16. In: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs, pp. 65\u201367. ACM, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3464971.3468417","DOI":"10.1145\/3464971.3468417"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Ferrari, A., Beek, M.H.T.: Formal methods in railways: a systematic mapping study. ACM Comput. Surv. 55(4) (2022). https:\/\/doi.org\/10.1145\/3520480","DOI":"10.1145\/3520480"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-94-011-1793-7_4","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19, 19\u201332 (1967). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4","journal-title":"Math. Aspects Comput. Sci."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Frenkel, E., Chajed, T., Padon, O., Shoham, S.: Efficient implementation of an abstract domain of quantified first-order formulas. In: International Conference on Computer Aided Verification, pp. 86\u2013108. Springer (2024)","DOI":"10.1007\/978-3-031-65630-9_5"},{"key":"17_CR12","first-page":"91","volume-title":"Computer Safety, Reliability, and Security","author":"A Iliasov","year":"2018","unstructured":"Iliasov, A., Taylor, D., Laibinis, L., Romanovsky, A.: Formal verification of signalling programs with safecap. In: Gallina, B., Skavhaug, A., Bitsch, F. (eds.) Computer Safety, Reliability, and Security, pp. 91\u2013106. Springer International Publishing, Cham (2018)"},{"issue":"1","key":"17_CR13","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. Dependable Secure Comput. 20(1), 695\u2013707 (2023). https:\/\/doi.org\/10.1109\/TDSC.2022.3141555","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Jin-hua, L., Qiong, L., Jing, L.: The w-model for testing software product lines. In: 2008 International Symposium on Computer Science and Computational Technology, vol. 1, pp. 690\u2013693 (2008). https:\/\/api.semanticscholar.org\/CorpusID:16758610","DOI":"10.1109\/ISCSCT.2008.34"},{"key":"17_CR15","unstructured":"Leino, K.R.M.: This is boogie 2, June 2008"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348\u2013370. Springer Berlin Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: PLDI, pp. 333\u2013344. ACM (1998)","DOI":"10.1145\/277650.277752"},{"issue":"4","key":"17_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3686153","volume":"25","author":"G Redondi","year":"2024","unstructured":"Redondi, G., Cimatti, A., Griggio, A., Mcmillan, K.L.: Invariant checking for smt-based systems with quantifiers. ACM Trans. Comput. Log. 25(4), 1\u201337 (2024)","journal-title":"ACM Trans. Comput. Log."},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Schaefer, I., Kuhlemann, M., Apel, S.: Proof composition for deductive verification of software product lines. In: ICST Workshops, pp. 270\u2013277. IEEE Computer Society (2011)","DOI":"10.1109\/ICSTW.2011.48"},{"key":"17_CR21","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-319-68499-4_7"},{"key":"17_CR22","unstructured":"Zhou, Y., Bosamiya, J., Takashima, Y., Li, J.G., Heule, M., Parno, B.: Mariposa: measuring SMT instability in automated program verification. In: Nadel, A., Rozier, K.Y. (eds.) Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2023, pp. 178\u2013188. TU Wien Academic Press (2023)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:55:12Z","timestamp":1760086512000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This work has been funded by project 8275061C5A, supported by RFI (Rete Ferroviaria Italiana).","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}