{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T09:15:09Z","timestamp":1725527709162},"reference-count":128,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T00:00:00Z","timestamp":1667260800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T00:00:00Z","timestamp":1667260800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T00:00:00Z","timestamp":1667260800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["881775 (4SECURail)"],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010679","name":"H2020 Energy","doi-asserted-by":"publisher","award":["777561 (ASTRail)"],"id":[{"id":"10.13039\/100010679","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2022,11,1]]},"DOI":"10.1109\/tse.2021.3124677","type":"journal-article","created":{"date-parts":[[2021,11,2]],"date-time":"2021-11-02T21:38:26Z","timestamp":1635889106000},"page":"4675-4691","source":"Crossref","is-referenced-by-count":20,"title":["Systematic Evaluation and Usability Analysis of Formal Methods Tools for Railway Signaling System Design"],"prefix":"10.1109","volume":"48","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-0636-5663","authenticated-orcid":false,"given":"Alessio","family":"Ferrari","sequence":"first","affiliation":[{"name":"Institute of Information Science and Technologies (ISTI), Italian National Research Council (CNR), Pisa, Italy"}]},{"ORCID":"http:\/\/orcid.org\/0000-0003-4562-8777","authenticated-orcid":false,"given":"Franco","family":"Mazzanti","sequence":"additional","affiliation":[{"name":"Institute of Information Science and Technologies (ISTI), Italian National Research Council (CNR), Pisa, Italy"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-7196-6609","authenticated-orcid":false,"given":"Davide","family":"Basile","sequence":"additional","affiliation":[{"name":"Institute of Information Science and Technologies (ISTI), Italian National Research Council (CNR), Pisa, Italy"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"additional","affiliation":[{"name":"Institute of Information Science and Technologies (ISTI), Italian National Research Council (CNR), Pisa, Italy"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0482-9"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.268.4"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70848-5_6"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2017.2657695"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2017.10"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99130-6_7"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.10.011"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_24"},{"key":"ref34","first-page":"98","article-title":"Modeling and analysing ERTMS hybrid level 3 with the mCRL2 toolset","author":"bartholomeus","year":"2018","journal-title":"Proc 23rd Int Conf Formal Methods Ind Crit Syst"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29510-7_7"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2014.11.007"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3019612.3019824"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0446-x"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0172-1"},{"key":"ref21","first-page":"619","article-title":"Formal methods: Theory becoming practice","volume":"13","author":"abrial","year":"2007","journal-title":"J Universal Comput Sci"},{"key":"ref24","first-page":"193","article-title":"Defining and model checking abstractions of complex railway models using CSP$\\parallel$?B","author":"moller","year":"2013","journal-title":"Proc Revised Sel Papers 8th Int Haifa Verification Conf"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.44"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_3"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0304-7"},{"key":"ref100","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00562-3"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.trc.2014.02.002"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0488-3"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33951-1_12"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0487-4"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1145\/3241743"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5679726"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_46"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_2"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1049\/cce:19970304"},{"key":"ref53","article-title":"Formal methods in railways: A systematic mapping study","author":"ferrari","year":"2021","journal-title":"CoRR"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_21"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-27008-7_1"},{"key":"ref4","first-page":"309","article-title":"Modelling large railway interlockings and model checking small ones","author":"winter","year":"2003","journal-title":"Proc 26th Australasian Comput Sci Conf"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0143-6"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47169-3_18"},{"key":"ref5","first-page":"167","article-title":"Twenty-five years of formal methods and railways: What next?","volume":"8368","author":"fantechi","year":"2013","journal-title":"Revised Selected Papers of the SEFM 2013 Collocated Workshops BEAT2 WS-FMDS FM-RAIL-Bok MoKMaSD and OpenCert"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_30"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00543-1"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00551-6"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-50086-3_1"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00542-2"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00539-x"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00525-3"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00548-w"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00540-4"},{"key":"ref127","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_5"},{"key":"ref126","first-page":"14","article-title":"The use of formal methods in specification and demonstration of ERTMS Hybrid Level 3","volume":"260","author":"bartholomeus","year":"2019","journal-title":"IRSE News"},{"key":"ref125","first-page":"1","article-title":"The use of formal methods in standardisation of interfaces of signalling systems","volume":"256","author":"van der werff","year":"2019","journal-title":"IRSE News"},{"key":"ref124","article-title":"Lessons from twenty years of industrial formal methods","author":"miller","year":"2012","journal-title":"Proc 20th High Confidence Softw Syst Conf"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.002"},{"key":"ref71","author":"holzmann","year":"2003","journal-title":"The SPIN Model Checker Primer and Reference Manual"},{"key":"ref128","article-title":"Formal methods: From academia to industrial practice. A travel guide","author":"huisman","year":"2020","journal-title":"CoRR"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_5"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91908-9_23"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0361-y"},{"key":"ref60","author":"duffy","year":"1991","journal-title":"Principles of automated theorem proving"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"ref61","author":"robinson","year":"2001","journal-title":"Handbook of Automated Reasoning"},{"key":"ref63","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref64","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0377-y"},{"key":"ref67","year":"2002","journal-title":"Atelier B User Manual Version 4 0"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_3"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.04.003"},{"key":"ref69","author":"paulson","year":"1994","journal-title":"Isabelle A Generic Theorem Prover"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1810295.1810312"},{"key":"ref95","article-title":"New results and trends in formal techniques & tools for the development of software for transportation systems: A review","author":"bj\u00f8rner","year":"2003","journal-title":"Proc 4th Symp Formal Methods Railway Operation Control Syst"},{"key":"ref109","first-page":"2","article-title":"ERTMS level 3: the game-changer","volume":"232","author":"furness","year":"2017","journal-title":"IRSE News"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050003"},{"key":"ref108","doi-asserted-by":"publisher","DOI":"10.1145\/1735223.1735255"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_1"},{"key":"ref107","doi-asserted-by":"publisher","DOI":"10.1080\/10447310802205776"},{"key":"ref106","doi-asserted-by":"publisher","DOI":"10.1145\/3239372.3239400"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1109\/MoDRE.2018.00008"},{"key":"ref105","first-page":"29","article-title":"SUS: A retrospective","volume":"8","author":"brooke","year":"2013","journal-title":"J usability Stud"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1109\/32.508312"},{"key":"ref104","first-page":"189","article-title":"SUS: A ‘quick and dirty’ usability scale","author":"brooke","year":"1996","journal-title":"Usability Evaluation in Industry"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1109\/52.251198"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.17730\/humo.56.2.x335923511444655"},{"key":"ref102","article-title":"Procedures for performing systematic reviews","author":"kitchenham","year":"0"},{"key":"ref111","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"ref112","year":"0"},{"key":"ref110","article-title":"Deliverable D2.1: Determine the long-term changes in future needs","author":"stroh","year":"2018"},{"key":"ref98","doi-asserted-by":"crossref","DOI":"10.1002\/9781119002727","author":"boulanger","year":"2014","journal-title":"Formal Methods Applied to Complex Systems Implementation of the B Method"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_17"},{"key":"ref96","first-page":"61","article-title":"Some trends in formal methods applications to railway signaling","author":"fantechi","year":"2013","journal-title":"FMICS A Survey of Applications"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.4018\/978-1-4666-1643-1"},{"key":"ref10","article-title":"Formal methods for safe and secure computer systems","author":"garavel","year":"2013"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22348-9_12"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-18744-6_15"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.08.009"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"ref15","year":"0","journal-title":"Railway Applications—Communication Signalling and Processing Systems—Software for Railway Control and Protection Systems"},{"key":"ref118","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66266-4_14"},{"key":"ref16","first-page":"63","article-title":"Study on the barriers to the industrial adoption of formal methods","author":"davis brussels","year":"2013","journal-title":"Proc 18th Int Workshop Formal Methods Ind Crit Syst"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"ref117","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2011.09.023"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_14"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9946.001.0001"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380373"},{"key":"ref84","author":"lamport","year":"2002","journal-title":"Specifying Systems The TLA+ Language and Tools for Hardware and Software Engineers"},{"key":"ref119","doi-asserted-by":"publisher","DOI":"10.1145\/3357231"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_20"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.37"},{"key":"ref114","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-009-0131-4"},{"key":"ref113","doi-asserted-by":"publisher","DOI":"10.1201\/9781315218168"},{"key":"ref116","doi-asserted-by":"publisher","DOI":"10.1145\/336512.336546"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0244-z"},{"key":"ref115","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE.2013.6612276"},{"key":"ref120","article-title":"Technology readiness assessment guide: Best practices for evaluating the readiness of technology for use in acquisition programs and projects","year":"2020"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09836-5"},{"key":"ref121","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_4"},{"key":"ref122","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"ref123","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33170-1_7"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0038-x"},{"key":"ref86","doi-asserted-by":"crossref","DOI":"10.1002\/9781118989166","author":"fritzson","year":"2014","journal-title":"Principles of Object Oriented Modeling and Simulation With Modelica 3 3 A Cyber-Physical Approach"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-6254-4_2"},{"key":"ref88","author":"dabney","year":"2003","journal-title":"Mastering SIMULINK"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/9946941\/09599463.pdf?arnumber=9599463","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,12]],"date-time":"2023-11-12T04:56:25Z","timestamp":1699764985000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9599463\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,1]]},"references-count":128,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tse.2021.3124677","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"},{"value":"2326-3881","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,1]]}}}