{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,27]],"date-time":"2024-07-27T12:33:47Z","timestamp":1722083627308},"reference-count":22,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.268.4","type":"journal-article","created":{"date-parts":[[2018,3,30]],"date-time":"2018-03-30T07:42:15Z","timestamp":1522395735000},"page":"104-149","source":"Crossref","is-referenced-by-count":23,"title":["Ten Diverse Formal Models for a CBTC Automatic Train Supervision System"],"prefix":"10.4204","volume":"268","author":[{"given":"Franco","family":"Mazzanti","sequence":"first","affiliation":[{"name":"ISTI-CNR"}]},{"given":"Alessio","family":"Ferrari","sequence":"additional","affiliation":[{"name":"ISTI-CNR"}]}],"member":"2720","published-online":{"date-parts":[[2018,3,23]]},"reference":[{"key":"psl","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/IEEESTD.2010.5446004","article-title":"IEEE Standard for Property Specification Language (PSL)","year":"2010","journal-title":"IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005)"},{"key":"eventb","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000081","volume-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial","year":"2010"},{"key":"mitl","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1145\/112600.112613","article-title":"The Benefits of Relaxing Punctuality","volume-title":"Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 19-21, 1991","author":"Alur","year":"1991"},{"key":"kandi","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-15545-6_20","article-title":"From EU projects to a family of model checkers","volume-title":"Software, Services, and Systems","volume":"8950","author":"ter Beek","year":"2015"},{"key":"nuxmv","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","article-title":"The nuXmv Symbolic Model Checker","volume-title":"CAV","author":"Cavada","year":"2014"},{"issue":"4","key":"uppaalsmc","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","article-title":"Uppaal SMC tutorial","volume":"17","author":"David","year":"2015","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"6","key":"ferrari2014commercial","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10009-013-0298-6","article-title":"From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions","volume":"16","author":"Ferrari","year":"2014","journal-title":"International Journal on Software Tools for Technology Transfer, STTT"},{"issue":"2","key":"cadp","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","article-title":"CADP 2011: a toolbox for the construction and analysis of distributed processes","volume":"15","author":"Garavel","year":"2013","journal-title":"STTT"},{"key":"lnt","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-68270-9_1","article-title":"From LOTOS to LNT","volume-title":"ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday","author":"Garavel","year":"2017"},{"key":"fdr3","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","article-title":"FDR3\u2014 A modern refinement checker for CSP","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Gibson-Robinson","year":"2014"},{"key":"mcrl2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and analysis of communicating systems","author":"Groote","year":"2014"},{"key":"spin","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann","year":"2003"},{"key":"cpn","doi-asserted-by":"publisher","DOI":"10.1007\/b95112","volume-title":"Coloured Petri nets: modelling and validation of concurrent systems","author":"Jensen","year":"2009"},{"key":"kuismin","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-319-03077-7_3","article-title":"Increasing confidence in liveness model checking results with proofs","volume-title":"Haifa Verification Conference","author":"Kuismin","year":"2013"},{"key":"mcl","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-68237-0_12","article-title":"A model checking language for concurrent value-passing systems","volume-title":"International Symposium on Formal Methods","author":"Mateescu","year":"2008"},{"key":"isola","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-319-47169-3_22","article-title":"Experiments in Formal Modelling of a Deadlock Avoidance Algorithm for a CBTC System","volume-title":"International Symposium on Leveraging Applications of Formal Methods - ISoLA 2016, Volune Part II","volume":"9953","author":"Mazzanti","year":"2014"},{"issue":"3","key":"mazzanti2018towards","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0488-3","article-title":"Towards Formal Methods Diversity in Railways: an Experience Report with Seven Frameworks","volume":"20","author":"Mazzanti","year":"2018","journal-title":"International Journal on Software Tools for Technology Transfer, STTT"},{"key":"mazzanti2014deadlock","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-319-10702-8_8","article-title":"Deadlock avoidance in train scheduling: a model checking approach","volume-title":"International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2014","volume":"8718","author":"Mazzanti","year":"2014"},{"key":"nfm14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-319-06200-6_22","article-title":"Designing a deadlock-free train scheduler: A model checking approach","volume-title":"NASA Formal Methods Symposium","volume":"8430","author":"Mazzanti","year":"2014"},{"key":"rebeca","article-title":"Power is Overrated, Go for Friendliness! Expressiveness, Faithfulness and Usability in Modeling - The Actor Experience","volume-title":"Principles of Modeling -Essays dedicated to Edward A. Lee on the Occasion of his 60th Birtday","author":"Sirjani","year":"2017"},{"issue":"2","key":"ter2011state","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","article-title":"A state\/event-based model-checking approach for the analysis of abstract system properties","volume":"76","author":"Ter Beek","year":"2011","journal-title":"Science of Computer Programming"},{"key":"winter2003modelling","first-page":"309","article-title":"Modelling large railway interlockings and model checking small ones","volume-title":"Proceedings of the 26th Australasian computer science conference-Volume 16","author":"Winter","year":"2003"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2019,10,13]],"date-time":"2019-10-13T18:49:51Z","timestamp":1570992591000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1803.10324v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,23]]},"references-count":22,"URL":"https:\/\/doi.org\/10.4204\/eptcs.268.4","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3,23]]}}}