{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:17:30Z","timestamp":1725902250285},"reference-count":129,"publisher":"Association for Computing Machinery (ACM)","issue":"4","funder":[{"name":"ASTRail and 4SECURail"},{"name":"European Union\u2019s Horizon 2020","award":["777561, 881775"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2023,4,30]]},"abstract":"Formal methods are mathematically based techniques for the rigorous development of software-intensive systems. The railway signaling domain is a field in which formal methods have traditionally been applied, with several success stories. This article reports on a mapping study that surveys the landscape of research on applications of formal methods to the development of railway systems. Following the guidelines of systematic reviews, we identify 328 relevant primary studies, and extract information about their demographics, the characteristics of formal methods used and railway-specific aspects. Our main results are as follows: (i)\u00a0we identify a total of 328 primary studies relevant to our scope published between 1989 and 2020, of which 44% published during the last 5 years and 24% involved industry; (ii)\u00a0the majority of studies are evaluated through Examples\u00a0(41%) and Experience Reports\u00a0(38%), while full-fledged Case Studies are limited\u00a0(1.5%); (iii)\u00a0Model checking is the most commonly adopted technique\u00a0(47%), followed by simulation\u00a0(27%) and theorem proving\u00a0(19.5%); (iv)\u00a0the dominant languages are UML\u00a0(18%) and B\u00a0(15%), while frequently used tools are ProB\u00a0(9%), NuSMV\u00a0(8%), and UPPAAL\u00a0(7%); however, a diverse landscape of languages and tools is employed; (v)\u00a0the majority of systems are interlocking products\u00a0(40%), followed by models of high-level control logic\u00a0(27%); and (vi)\u00a0most of the studies focus on the Architecture\u00a0(66%) and Detailed Design\u00a0(45%) development phases. Based on these findings, we highlight current research gaps and expected actions. In particular, the need to focus on more empirically sound research methods, such as Case Studies and Controlled Experiments, and to lower the degree of abstraction, by applying formal methods and tools to development phases that are closer to software development. Our study contributes with an empirically based perspective on the future of research and practice in formal methods applications for railways. It can be used by formal methods researchers to better focus their scientific inquiries, and by railway practitioners for an improved understanding of the interplay between formal methods and their specific application domain.<\/jats:p>","DOI":"10.1145\/3520480","type":"journal-article","created":{"date-parts":[[2022,3,4]],"date-time":"2022-03-04T12:29:59Z","timestamp":1646396999000},"page":"1-37","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Formal Methods in Railways: A Systematic Mapping Study"],"prefix":"10.1145","volume":"55","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-0636-5663","authenticated-orcid":false,"given":"Alessio","family":"Ferrari","sequence":"first","affiliation":[{"name":"Istituto di Scienza e Tecnologie dell\u2019Informazione, Consiglio Nazionale delle Ricerche (ISTI\u2013CNR), Pisa, Italy"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H. Ter","family":"Beek","sequence":"additional","affiliation":[{"name":"Istituto di Scienza e Tecnologie dell\u2019Informazione, Consiglio Nazionale delle Ricerche (ISTI\u2013CNR), Pisa, Italy"}]}],"member":"320","published-online":{"date-parts":[[2022,11,21]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"221","volume-title":"Proceedings of the SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD, and OpenCert. Lecture Notes in Computer Science (LNCS)","volume":"8368","author":"Abo Robert","year":"2013","unstructured":"Robert Abo and Laurent Voisin. 2013. Formal implementation of data validation for railway safety-related systems with OVADO. In Proceedings of the SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD, and OpenCert. Lecture Notes in Computer Science (LNCS), Steve Counsell and Manuel N\u00fa\u00f1ez (Eds.), Vol. 8368. Springer, 221\u2013236."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134406"},{"issue":"5","key":"e_1_3_2_4_2","first-page":"619","article-title":"Formal methods: Theory becoming practice","volume":"13","author":"Abrial Jean-Raymond","year":"2007","unstructured":"Jean-Raymond Abrial. 2007. Formal methods: Theory becoming practice. J. Univers. Comput. Sci. 13, 5 (2007), 619\u2013628.","journal-title":"J. Univers. Comput. Sci."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2018.10.006"},{"key":"e_1_3_2_7_2","first-page":"65","volume-title":"Proceedings of the 8th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS\/FORMAT\u201910)","author":"Antoni Marc","year":"2010","unstructured":"Marc Antoni. 2010. Complementarity between axle counters and tracks circuits. In Proceedings of the 8th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS\/FORMAT\u201910), Eckehard Schnieder and G\u00e9za Tarnai (Eds.). Springer, 65\u201376."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/11415787_20"},{"key":"e_1_3_2_9_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2017.2681076"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85248-1_11"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_30"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_2"},{"key":"e_1_3_2_14_2","first-page":"762","volume-title":"Proceedings of the 3rd World Congress on Formal Methods: The Next 30 Years (FM\u201919). Lecture Notes in Computer Science (LNCS)","volume":"11800","author":"Beek Maurice H. ter","year":"2019","unstructured":"Maurice H. ter Beek, Arne Bor\u00e4lv, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi, Christer L\u00f6fving, and Franco Mazzanti. 2019. Adopting formal methods in an industrial setting: The railways case. In Proceedings of the 3rd World Congress on Formal Methods: The Next 30 Years (FM\u201919). Lecture Notes in Computer Science (LNCS), Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N. Oliveira (Eds.), Vol. 11800. Springer, 762\u2013772."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_22"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.10.011"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/1550723"},{"key":"e_1_3_2_18_2","volume-title":"Proceedings of the 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS\u201903)","author":"Bj\u00f8rner Dines","year":"2003","unstructured":"Dines Bj\u00f8rner. 2003. New results and trends in formal techniques and tools for the development of software for transportation systems: A review. In Proceedings of the 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS\u201903), G\u00e9za Tarnai and Eckehard Schnieder (Eds.). L\u2019Harmattan."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_4"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40891-6_19"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.04.004"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2014.11.007"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781118561829"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781118561829"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/2840195"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1996.488298"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.391826"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.375178"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.35"},{"key":"e_1_3_2_30_2","first-page":"71","volume-title":"Computing Handbook","author":"Bowen Jonathan P.","year":"2014","unstructured":"Jonathan P. Bowen and Michael G. Hinchey. 2014. Formal methods. In Computing Handbook, Teofilo F. Gonzalez, Jorge Diaz-Herrera, and Allen Tucker (Eds.). CRC, Chapter 71, 71\u201325."},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0024646"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11737-9_25"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_8"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6656-1"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2010.12.006"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/1810295.1810312"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48249-0_35"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-009-0130-7"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377659"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-18744-6_13"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60218-6_24"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48234-2_6"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/203034"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.5555\/647280.722639"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.345825"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011279932612"},{"key":"e_1_3_2_49_2","first-page":"199","volume-title":"Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201992) (IFIP Transactions)","volume":"10","author":"DaSilva Clara","year":"1992","unstructured":"Clara DaSilva, Babak Dehbonei, and Fernando Mejia. 1992. Formal specification in the development of industrial applications: Subway speed control system. In Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201992) (IFIP Transactions), Michel Diaz and Roland Groz (Eds.), Vol. C-10. North-Holland, 199\u2013213."},{"key":"e_1_3_2_50_2","unstructured":"Marian Daun Carolin H\u00fcbscher and Thorsten Weyer. 2017. Controlled experiments with student participants in software engineering: Preliminary results from a systematic mapping study. arxiv:1708.04662"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41010-9_5"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(01)00242-0"},{"key":"e_1_3_2_53_2","unstructured":"(LNCS) Proceedings of the 3rd International Workshop and Tutorial on Formal Methods Teaching (FMTea\u201919) 11758 Brijesh Dongol Luigia Petre Graeme Smith 2019"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2008.01.006"},{"key":"e_1_3_2_55_2","unstructured":"European Committee for Electrotechnical Standardization. 2011. CENELEC EN 50128\u2014Railway applications \u2013 Communication signalling and processing systems \u2013 Software for railway control and protection systems. https:\/\/standards.globalspec.com\/std\/1678027\/cenelec-en-50128."},{"key":"e_1_3_2_56_2","unstructured":"European Committee for Electrotechnical Standardization. 2021. CENELEC CLC\/TS 50701\u2014Railway applications \u2013 Cybersecurity. https:\/\/standards.cencenelec.eu\/dyn\/www\/f?p=CENELEC:110:0::::FSP_PROJECT:67491&cs=10ADCDA886163E20D48884DEEF0C2D72B."},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-017-9523-3"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0318-1"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2015.2446985"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.4018\/978-1-4666-1643-1.ch012"},{"key":"e_1_3_2_61_2","series-title":"LNCS","first-page":"167","volume-title":"Revised Selected Papers of the SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD, and OpenCert. Lecture Notes in Computer Science","author":"Fantechi Alessandro","year":"2013","unstructured":"Alessandro Fantechi. 2013. Twenty-five years of formal methods and railways: What next? In Revised Selected Papers of the SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD, and OpenCert. Lecture Notes in Computer Science (LNCS), Steve Counsell and Manuel N\u00fa\u00f1ez (Eds.), Vol. 8368. Springer, 167\u2013183."},{"key":"e_1_3_2_62_2","first-page":"61","volume-title":"Formal Methods for Industrial Critical Systems: A Survey of Applications","author":"Fantechi Alessandro","year":"2013","unstructured":"Alessandro Fantechi, Wan Fokkink, and Angelo Morzenti. 2013. Some trends in formal methods applications to railway signaling. In Formal Methods for Industrial Critical Systems: A Survey of Applications, Stefania Gnesi and Tiziana Margaria (Eds.). Wiley, Chapter 4, 61\u201384."},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_5"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.44"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.04.003"},{"key":"e_1_3_2_66_2","article-title":"Systematic evaluation and usability analysis of formal methods tools for railway signaling system design","author":"Ferrari Alessio","year":"2021","unstructured":"Alessio Ferrari, Franco Mazzanti, Davide Basile, and Maurice H. ter Beek. 2021. Systematic evaluation and usability analysis of formal methods tools for railway signaling system design. IEEE Trans. Softw. Eng. (2021).","journal-title":"IEEE Trans. Softw. Eng."},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380373"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-18744-6_15"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.04.010"},{"key":"e_1_3_2_70_2","volume-title":"Formal Methods for Safe and Secure Computer Systems","author":"Garavel Hubert","year":"2013","unstructured":"Hubert Garavel and Susanne Graf. 2013. Formal Methods for Safe and Secure Computer Systems. BSI Study 875. Bundesamt f\u00fcr Sicherheit in der Informationstechnik. https:\/\/www.bsi.bund.de\/SharedDocs\/Downloads\/DE\/BSI\/Publikationen\/Studien\/formal_methods_study_875\/formal_methods_study_875.html."},{"key":"e_1_3_2_71_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/978-3-030-22348-9_12","volume-title":"Models, Mindsets, Meta: The What, the How, and the Why Not?","author":"Garavel Hubert","year":"2019","unstructured":"Hubert Garavel and Radu Mateescu. 2019. Reflections on bernhard steffen\u2019s physics of software tools. In Models, Mindsets, Meta: The What, the How, and the Why Not?, Tiziana Margaria, Susanne Graf, and Kim Larsen (Eds.). Lecture Notes in Computer Science (LNCS), Vol. 11200. Springer, 186\u2013207."},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1145\/383876.383877"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.251198"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09836-5"},{"key":"e_1_3_2_76_2","volume-title":"Formal Methods for Industrial Critical Systems: A Survey of Applications","author":"Gnesi Stefania","year":"2013","unstructured":"Stefania Gnesi and Tiziana Margaria (Eds.). 2013. Formal Methods for Industrial Critical Systems: A Survey of Applications."},{"key":"e_1_3_2_77_2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-319-29510-7_5","volume-title":"Proceedings of the 4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS\u201915) (CCIS)","volume":"596","author":"Gruner Stefan","year":"2015","unstructured":"Stefan Gruner, Apurva Kumar, and Tom Maibaum. 2015. Towards a body of knowledge in formal methods for the railway domain: Identification of settled knowledge. In Proceedings of the 4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS\u201915) (CCIS), Cyrille Artho and Peter C. \u00d6lveczky (Eds.), Vol. 596. Springer, 87\u2013102."},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.5555\/100296.100321"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"issue":"5","key":"e_1_3_2_80_2","first-page":"669","article-title":"Realising the benefits of formal methods","volume":"13","author":"Hall Anthony","year":"2007","unstructured":"Anthony Hall. 2007. Realising the benefits of formal methods. J. Univers. Comput. Sci. 13, 5 (2007), 669\u2013678.","journal-title":"J. Univers. Comput. Sci."},{"key":"e_1_3_2_81_2","series-title":"Proceedings of the 9th International Conference of Z Users (ZUM\u201995). Lecture Notes in Computer Science","first-page":"237","volume":"967","author":"Hall Anthony","year":"1995","unstructured":"Anthony Hall, David Lorge Parnas, Nico Plat, John M. Rushby, and Chris T. Sennett. 1995. The future of formal methods in industry. In Proceedings of the 9th International Conference of Z Users (ZUM\u201995). Lecture Notes in Computer Science (LNCS), Jonathan P. Bowen and Michael G. Hinchey (Eds.), Vol. 967. Springer, 237\u2013242."},{"key":"e_1_3_2_82_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2016.09.027"},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00551-6"},{"key":"e_1_3_2_84_2","volume-title":"An Introduction to Formal Methods for the Development of Safety-critical Applications","author":"Haxthausen Anne E.","year":"2010","unstructured":"Anne E. Haxthausen. 2010. An Introduction to Formal Methods for the Development of Safety-critical Applications. Technical Report. Technical University of Denmark. https:\/\/orbit.dtu.dk\/files\/137536957\/FormalMethodsNoteTS.pdf."},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1994.342724"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0523-7"},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2014.2366512"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2004.95746"},{"key":"e_1_3_2_90_2","volume-title":"IEC 62290-1\u20133: Railway applications \u2013 Urban guided transport management and command\/control systems \u2013 Parts 1\u20133.","author":"Commission International Electrotechnical","year":"2019","unstructured":"International Electrotechnical Commission. 2019. IEC 62290-1\u20133: Railway applications \u2013 Urban guided transport management and command\/control systems \u2013 Parts 1\u20133.http:\/\/webstore.iec.ch\/publication\/28078."},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_1"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0304-7"},{"key":"e_1_3_2_93_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58555-9_86"},{"key":"e_1_3_2_94_2","volume-title":"Procedures for Performing Systematic Reviews","author":"Kitchenham Barbara","year":"2004","unstructured":"Barbara Kitchenham. 2004. Procedures for Performing Systematic Reviews. Technical Report TR\/SE-0401. Keele University."},{"key":"e_1_3_2_95_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-013-9279-3"},{"key":"e_1_3_2_96_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70848-5_6"},{"key":"e_1_3_2_97_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0172-1"},{"key":"e_1_3_2_98_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejor.2017.07.044"},{"key":"e_1_3_2_99_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72003-2_4"},{"key":"e_1_3_2_100_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2017.2658179"},{"key":"e_1_3_2_101_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0488-3"},{"key":"e_1_3_2_102_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICFEM.1998.730572"},{"key":"e_1_3_2_103_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2020.2978567"},{"key":"e_1_3_2_104_2","volume-title":"Proceedings of the 20th High Confidence Software and Systems Conference (HCSS\u201912)","author":"Miller Steven P.","year":"2012","unstructured":"Steven P. Miller. 2012. Lessons from twenty years of industrial formal methods. In Proceedings of the 20th High Confidence Software and Systems Conference (HCSS\u201912). http:\/\/cps-vo.org\/node\/3434."},{"key":"e_1_3_2_105_2","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"key":"e_1_3_2_106_2","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2015.7295465"},{"key":"e_1_3_2_107_2","doi-asserted-by":"publisher","DOI":"10.5555\/2161638"},{"key":"e_1_3_2_108_2","first-page":"189","volume-title":"Proceedings of the 6th IFIP TC6\/WG6.1 International Conference on Formal Description Techniques (FORTE\u201993) (IFIP Transactions)","volume":"22","author":"Parkin Graeme I. P.","year":"1993","unstructured":"Graeme I. P. Parkin and Stephen Austin. 1993. Overview: Survey of formal methods in industry. In Proceedings of the 6th IFIP TC6\/WG6.1 International Conference on Formal Description Techniques (FORTE\u201993) (IFIP Transactions), Richard L. Tenney, Paul D. Amer, and M. \u00dcmit Uyar (Eds.), Vol. C-22. North-Holland, 189\u2013203."},{"key":"e_1_3_2_109_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.111.1"},{"key":"e_1_3_2_110_2","first-page":"629","volume-title":"Proceedings of the IFIP 18th World Computer Congress: Topical Sessions (WCC\u201904) (IFIP Advances in Information and Communication Technology)","volume":"156","author":"Penicka Martin","year":"2004","unstructured":"Martin Penicka and Dines Bj\u00f8rner. 2004. From railway resource planning to train operation: A brief survey of complementary formalisations. In Proceedings of the IFIP 18th World Computer Congress: Topical Sessions (WCC\u201904) (IFIP Advances in Information and Communication Technology), Ren\u00e9 Jacquart (Ed.), Vol. 156. Springer, 629\u2013636."},{"key":"e_1_3_2_111_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2015.03.007"},{"key":"e_1_3_2_112_2","volume-title":"Handbook of Automated Reasoning","author":"Robinson John A.","year":"2001","unstructured":"John A. Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier."},{"key":"e_1_3_2_113_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781118181034"},{"key":"e_1_3_2_114_2","volume-title":"Formal Methods and the Certification of Critical Systems","author":"Rushby John","year":"1993","unstructured":"John Rushby. 1993. Formal Methods and the Certification of Critical Systems. Technical Report SRI-CSL-93-7. Computer Science Laboratory, SRI International. http:\/\/www.csl.sri.com\/papers\/csl-93-7\/."},{"key":"e_1_3_2_115_2","volume-title":"The Coding Manual for Qualitative Researchers","author":"Salda\u00f1a Johnny","year":"2021","unstructured":"Johnny Salda\u00f1a. 2021. The Coding Manual for Qualitative Researchers. SAGE."},{"key":"e_1_3_2_116_2","unstructured":"Muhammad Saqib Nawaz Moin Malik Yi Li Meng Sun and Muhammad Ikram Ullah Lali. 2019. A Survey on Theorem Provers in Formal Methods. arXiv:1912.03028."},{"key":"e_1_3_2_117_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2020.101833"},{"key":"e_1_3_2_118_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2018.2819799"},{"key":"e_1_3_2_119_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0446-x"},{"key":"e_1_3_2_120_2","doi-asserted-by":"publisher","DOI":"10.1016\/0141-9331(90)90127-H"},{"key":"e_1_3_2_121_2","doi-asserted-by":"publisher","DOI":"10.1016\/0141-9331(93)90091-K"},{"key":"e_1_3_2_122_2","volume-title":"Foundations of Constraint Satisfaction","author":"Tsang Edward","year":"1993","unstructured":"Edward Tsang. 1993. Foundations of Constraint Satisfaction. Academic Press."},{"key":"e_1_3_2_123_2","first-page":"7308604:1\u201373086","article-title":"A survey of channel measurements and models for current and future railway communication systems","volume":"2016","author":"Unterhuber Paul","year":"2016","unstructured":"Paul Unterhuber, Stephan Pfletschinger, Stephan Sand, Mohammad Soliman, Thomas Jost, Aitor Arriola, I\u00f1aki Val, Cristina Cruces, Juan Moreno, Juan Pablo Garc\u00eda-Nieto, Carlos Rodr\u00edguez, Marion Berbineau, Eneko Echeverr\u00eda, and Imanol Baz. 2016. A survey of channel measurements and models for current and future railway communication systems. Mob. Inf. Syst. 2016 (2016), 7308604:1\u20137308604:14.","journal-title":"Mob. Inf. Syst."},{"key":"e_1_3_2_124_2","doi-asserted-by":"publisher","DOI":"10.1109\/MVT.2017.2736098"},{"key":"e_1_3_2_125_2","doi-asserted-by":"publisher","DOI":"10.1109\/MITS.2018.2842230"},{"key":"e_1_3_2_126_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_3_2_127_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29044-2"},{"key":"e_1_3_2_128_2","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_3_2_129_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-016-0517-1"},{"key":"e_1_3_2_130_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.comcom.2016.04.003"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3520480","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,19]],"date-time":"2023-11-19T08:36:08Z","timestamp":1700382968000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3520480"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,21]]},"references-count":129,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,4,30]]}},"alternative-id":["10.1145\/3520480"],"URL":"https:\/\/doi.org\/10.1145\/3520480","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,21]]},"assertion":[{"value":"2021-07-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-02-22","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}