{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T21:00:34Z","timestamp":1730322034014,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":63,"publisher":"ACM","funder":[{"name":"European Union","award":["777561, 881775"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,27]]},"DOI":"10.1145\/3377811.3380373","type":"proceedings-article","created":{"date-parts":[[2020,10,1]],"date-time":"2020-10-01T18:25:34Z","timestamp":1601576734000},"page":"62-74","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Comparing formal tools for system design"],"prefix":"10.1145","author":[{"given":"Alessio","family":"Ferrari","sequence":"first","affiliation":[{"name":"ISTI-CNR, Pisa, Italy"}]},{"given":"Franco","family":"Mazzanti","sequence":"additional","affiliation":[{"name":"ISTI-CNR, Pisa, Italy"}]},{"given":"Davide","family":"Basile","sequence":"additional","affiliation":[{"name":"ISTI-CNR, Pisa, Italy"}]},{"given":"Maurice H. ter","family":"Beek","sequence":"additional","affiliation":[{"name":"ISTI-CNR, Pisa, Italy"}]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[{"name":"University of Florence, Florence, Italy"}]}],"member":"320","published-online":{"date-parts":[[2020,10]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3217\/jucs013-05-0619"},{"volume-title":"The B-book: assigning programs to meanings","author":"Abrial Jean-Raymond","key":"e_1_3_2_1_2_1","unstructured":"Jean-Raymond Abrial and Jean-Raymond Abrial. 2005. The B-book: assigning programs to meanings. Cambridge University Press."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_19"},{"volume-title":"Principles of Model Checking","author":"Baier Christel","key":"e_1_3_2_1_4_1","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00244-2_7"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3019612.3019824"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_24"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_2"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-27008-7_1"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_46"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0487-4"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.10.011"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"volume-title":"Automated theorem proving","author":"Bibel Wolfgang","key":"e_1_3_2_1_14_1","unstructured":"Wolfgang Bibel. 2013. Automated theorem proving. Springer Science & Business Media."},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS","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 2003), G\u00e9za Tarnai and Eckehard Schnieder (Eds.). L'Harmattan, Hungary."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2014.11.007"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Jean-Louis Boulanger (Ed.). 2014. Formal Methods Applied to Industrial Complex Systems --- Implementation of the B Method. John Wiley & Sons USA. 10.1002\/9781119002727","DOI":"10.1002\/9781119002727"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2017.10"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1810295.1810312"},{"key":"e_1_3_2_1_20_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Edmund M. Clarke Thomas A. Henzinger Helmut Veith and Roderick Bloem (Eds.). 2018. Handbook of Model Checking. Springer. 10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16561-0_18"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_21"},{"key":"e_1_3_2_1_24_1","unstructured":"James B Dabney and Thomas L Harman. 2004. Mastering simulink. Pearson."},{"key":"e_1_3_2_1_25_1","volume-title":"CENELEC EN 50128 - Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems. (1","author":"European Committee for Electrotechnical Standardization. 2011.","year":"2011","unstructured":"European Committee for Electrotechnical Standardization. 2011. CENELEC EN 50128 - Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems. (1 June 2011). https:\/\/standards.globalspec.com\/std\/1678027\/cenelec-en-50128."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Alessandro Fantechi. 2013. Twenty-Five Years of Formal Methods and Railways: What Next?. In Software Engineering and Formal Methods - Revised Selected Papers of the SEFM 2013 Collocated Workshops: BEAT2 WS-FMDS FM-RAIL-Bok MoKMaSD and OpenCert (Lecture Notes in Computer Science) Steve Counsell and Manuel N\u00fa\u00f1ez (Eds.) Vol. 8368. Springer Germany 167--183. 10.1007\/978-3-319-05032-4_13","DOI":"10.1007\/978-3-319-05032-4_13"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1002\/9781118459898.ch4"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.44"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.04.003"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3375494"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Alessio Ferrari Franco Mazzanti and Andrea Piattino. 2019. ASTRail Deliverable 4.3 Task 4.4 - Supplementary Material. (Aug. 2019). 10.5281\/zenodo.3377823","DOI":"10.5281\/zenodo.3377823"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-18744-6_15"},{"volume-title":"First-order logic and automated theorem proving","author":"Fitting Melvin","key":"e_1_3_2_1_33_1","unstructured":"Melvin Fitting. 2012. First-order logic and automated theorem proving. Springer Science & Business Media."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Francesco Flammini (Ed.). 2012. Railway Safety Reliability and Security: Technologies and Systems Engineering. IGI Global USA. 10.4018\/978-1-4666-1643-1","DOI":"10.4018\/978-1-4666-1643-1"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04293-9"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0244-z"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.trc.2014.02.002"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0377-y"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33951-1_12"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0143-6"},{"volume-title":"The SPIN model checker: Primer and reference manual","author":"Holzmann Gerard J","key":"e_1_3_2_1_41_1","unstructured":"Gerard J Holzmann. 2004. The SPIN model checker: Primer and reference manual. Vol. 1003. Addison-Wesley Reading."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99130-6_7"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0304-7"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1049\/cce:19970304"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70848-5_6"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.4103\/2249-4863.161306"},{"key":"e_1_3_2_1_48_1","volume-title":"Butler","author":"Leuschel Michael","year":"2003","unstructured":"Michael Leuschel and Michael J. Butler. 2003. ProB: A Model Checker for B. In Proceedings of the 12th International Symposium on Formal Methods (FME 2003) (Lecture Notes in Computer Science), Keijiro Araki, Stefania Gnesi, and Dino Mandrioli (Eds.), Vol. 2805. Springer, 855--874. https:\/\/doi.org\/0.1007\/978-3-540-45236-2_46"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0172-1"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_24"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","unstructured":"Franco Mazzanti and Alessio Ferrari. 2018. Ten Diverse Formal Models for a CBTC Automatic Train Supervision System. In Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation (MARS\/VPT 2018) (Electronic Proceedings in Theoretical Computer Science) John P. Gallagher Rob van Glabbeek and Wendelin Serwe (Eds.) Vol. 268. 104--149. 10.4204\/EPTCS.268.4","DOI":"10.4204\/EPTCS.268.4"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0488-3"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_20"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","unstructured":"Roberto Nardone Ugo Gentile Massimo Benerecetti Adriano Peron Valeria Vittorini Stefano Marrone and Nicola Mazzocca. 2016. Modeling Railway Control Systems in Promela. In Formal Techniques for Safety-Critical Systems --- Revised Selected Papers of the 4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2015) (Communications in Computer and Information Science) Cyrille Artho and Peter C. \u00d6lveczky (Eds.) Vol. 596. Springer Germany 121--136. 10.1007\/978-3-319-29510-7_7","DOI":"10.1007\/978-3-319-29510-7_7"},{"issue":"5","key":"e_1_3_2_1_55_1","first-page":"1","article-title":"Unified Modeling Language","volume":"2","author":"Object Management Group (OMG).","year":"2017","unstructured":"Object Management Group (OMG). 2017. Unified Modeling Language, Version 2.5.1. https:\/\/www.omg.org\/spec\/UML\/About-UML\/. (2017).","journal-title":"Version"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03240-0_7"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3241743"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1111\/nhs.12048"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0482-9"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_3_2_1_62_1","volume-title":"Proceedings of the 26th Australasian Computer Science Conference (ACSC 2003)","volume":"16","author":"Winter Kirsten","unstructured":"Kirsten Winter and Neil J. Robinson. 2003. Modelling Large Railway Interlockings and Model Checking Small Ones. In Proceedings of the 26th Australasian Computer Science Conference (ACSC 2003) (Conferences in Research and Practice in Information Technology), Michael J. Oudshoorn (Ed.), Vol. 16. Australian Computer Society, Australia, 309--316. http:\/\/crpit.com\/confpapers\/CRPITV16Winter.pdf."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"}],"event":{"name":"ICSE '20: 42nd International Conference on Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","KIISE Korean Institute of Information Scientists and Engineers","IEEE CS"],"location":"Seoul South Korea","acronym":"ICSE '20"},"container-title":["Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3377811.3380373","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,14]],"date-time":"2024-07-14T22:52:13Z","timestamp":1720997533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3377811.3380373"}},"subtitle":["a judgment study"],"short-title":[],"issued":{"date-parts":[[2020,6,27]]},"references-count":63,"alternative-id":["10.1145\/3377811.3380373","10.1145\/3377811"],"URL":"https:\/\/doi.org\/10.1145\/3377811.3380373","relation":{},"subject":[],"published":{"date-parts":[[2020,6,27]]},"assertion":[{"value":"2020-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}