{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T17:00:48Z","timestamp":1783530048420,"version":"3.55.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            The substitution of traditional occupancy detecting sensors with an\nAutonomous Positioning System (APS) is a promising solution to\ncontain costs and improve performance of current tramway signalling\nsystems. APS is an onboard system using satellite positioning and\nother inertial platforms to autonomously estimate the position of\nthe tram  with the needed levels of uncertainty and protection.\nHowever, autonomous positioning  introduces, even in absence of\nfaults, a quantitative uncertainty with respect to traditional\nsensors. This paper investigates this issue in the context of an\nindustrial project: a model of the envisaged solution is proposed,\nand it is analysed using\n            <jats:sc>Uppaal<\/jats:sc>\n            Statistical Model Checker.\nA novel model-driven hazard analysis approach to the exploration of\nemerging hazards is proposed. The analysis emphasises how the\nvirtualisation of legacy track circuits and on-board satellite\npositioning equipment may give rise to new hazards, not present in\nthe traditional system.\n          <\/jats:p>","DOI":"10.1007\/s00165-021-00556-1","type":"journal-article","created":{"date-parts":[[2021,7,29]],"date-time":"2021-07-29T09:02:37Z","timestamp":1627549357000},"page":"957-987","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Analysing an autonomous tramway positioning system with the\n            <scp>Uppaal<\/scp>\n            Statistical Model Checker"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7196-6609","authenticated-orcid":false,"given":"Davide","family":"Basile","sequence":"first","affiliation":[{"name":"Institute of Information Science and Technologies \u201cAlessandro Faedo\u201d - ISTI, National Research Council, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[{"name":"Department of Information Engineering, University of Florence, Florence, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luigi","family":"Rucher","sequence":"additional","affiliation":[{"name":"Thales Italia S.p.A., Florence, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gianluca","family":"Mand\u00f2","sequence":"additional","affiliation":[{"name":"Thales Italia S.p.A., Florence, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Arcaini P Kofro\u0148 J Je\u017eek P (2020) Validation of the hybrid ERTMS\/ETCS level 3 using spin. Int J Softw Tools Technol Transf\n22(3):265\u2013279","DOI":"10.1007\/s10009-019-00539-x"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Agha G Palmskog K (2018) A survey of statistical model checking. ACM Trans Model Comput Simul 28(1):6:1\u20136:39","DOI":"10.1145\/3158668"},{"key":"#cr-split#-e_1_2_1_2_3_2.1","unstructured":"Arenis SF Vujinovic M Westphal B (2020) On implementable timed automata. In: Formal techniques for distributed objects components and systems-40th IFIP WG 6.1 international conference FORTE 2020 held as part of the 15th international"},{"key":"#cr-split#-e_1_2_1_2_3_2.2","unstructured":"federated conference on distributed computing techniques DisCoTec 2020 Valletta Malta June 15-19 2020 proceedings"},{"key":"e_1_2_1_2_4_2","unstructured":"Basile D (2021) Repository for reproducing the experiments. https:\/\/github.com\/davidebasile\/faoc2020"},{"key":"e_1_2_1_2_5_2","unstructured":"Behrmann G David A Larsen KG H\u00e5kansson J Pettersson P Yi W Hendriks M (2006) UPPAAL 4.0. In: Proceedings of\nthe 3rd international conference on the quantitative evaluation of sysTems (QEST\u201906). IEEE pp 125\u2013126"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bulychev P David A Larsen KG Legay A Li G Poulsen DB (2013) Rewrite-based statistical model checking of WMTL.\nIn: Qadeer S Tasiran S (eds) Runtime verification\u2014revised selected papers of the 3rd international conference on runtime\nverification (RV\u201912) volume 7687 of lecture notes in computer science. Springer pp 260\u2013275","DOI":"10.1007\/978-3-642-35632-2_25"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Basile D Fantechi A Rucher L Mand\u00f2 G (2019) Statistical model checking of hazards in an autonomous tramway positioning\nsystem. In: Reliability safety and security of railway systems. Modelling analysis verification and certification\u2014third\ninternational conference RSSRail 2019 Lille France June 4\u20136 2019 proceedings pp 41\u201358","DOI":"10.1007\/978-3-030-18744-6_3"},{"key":"#cr-split#-e_1_2_1_2_8_2.1","doi-asserted-by":"crossref","unstructured":"Basile D Di Giandomenico F Gnesi S (2017) Dependable dynamic routing for urban transport systems through integer linear","DOI":"10.1007\/978-3-319-68499-4_15"},{"key":"#cr-split#-e_1_2_1_2_8_2.2","doi-asserted-by":"crossref","unstructured":"programming. In: FantechiA Lecomte T Romanovsky AB(eds)Reliability safety and security of railway systems. Modelling analysis verification and certification-second international conference RSSRail 2017 Pistoia Italy November 14-16 2017 proceedings volume 10598 of lecture notes in computer science. Springer pp 221-237","DOI":"10.1007\/978-3-319-68499-4"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Barbot B Haddad S Picaronny C (2012) Coupling and importance sampling for statistical model checking. In: Flanagan C K\u00f6nig B (eds) Tools and algorithms for the construction and analysis of systems volume 7214 of LNCS. Springer pp 331\u2013346","DOI":"10.1007\/978-3-642-28756-5_23"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Berger U James P Lawrence A Roggenbach M Seisenberger M (2018) Verification of the European rail traffic management\nsystem in real-time maude. Sci Comput Program 154:61\u201388","DOI":"10.1016\/j.scico.2017.10.011"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Bartholomeus M Luttik B Willemse T (2018) Modelling and analysing ERTMS hybrid level 3 with the mCRL2 toolset. In:\nHowar F Barnat J (eds) Proceedings of the 23rd international conference on formal methods for industrial critical systems\n(FMICS\u201918) volume 11119 of LNCS. Springer","DOI":"10.1007\/978-3-030-00244-2_7"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Beugin J Marais J (2012) Simulation-based evaluation of dependability and safety properties of satellite technologies for\nrailway localization. Transp Res C-Emerg 22:42\u201357","DOI":"10.1016\/j.trc.2011.12.002"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Boulanger JL (2015) Tool qualification. In: CENELEC 50128 and IEC 62279 Standards chap. 9. Wiley pp 287\u2013308","DOI":"10.1002\/9781119005056.ch9"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Basile D ter Beek MH Ciancia V (2018) Statistical model checking of amoving block railway signalling scenario with UPPAAL\nSMC\u2014experience and outlook. In: Leveraging applications of formal methods verification and validation. Verification\u20148th\ninternational symposium ISoLA 2018 Limassol Cyprus November 5\u20139 2018 proceedings Part II pp 372\u2013391","DOI":"10.1007\/978-3-030-03421-4_24"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Basile D ter Beek MH Ferrari A Legay A (2019) Modelling and analysing ERTMS L3 moving block railway signalling\nwith simulink and UPPAAL SMC. In: Formal methods for industrial critical systems\u201424th international conference FMICS\n2019 Amsterdam The Netherlands August 30\u201331 2019 proceedings pp 1\u201321","DOI":"10.1007\/978-3-030-27008-7_1"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Basile D ter Beek MH Legay A (2020) Strategy synthesis for autonomous driving in a moving block railway system with\nUPPAAL stratego. In: Formal techniques for distributed objects components and systems\u201440th IFIPWG 6.1 international\nconference FORTE 2020 held as part of the 15th international federated conference on distributed computing techniques DisCoTec 2020 Valletta Malta June 15\u201319 2020 proceedings pp 3\u201321","DOI":"10.1007\/978-3-030-50086-3_1"},{"key":"#cr-split#-e_1_2_1_2_17_2.1","unstructured":"Ceccarelli A Basile D Bondavalli A Falai L Fantechi A Ferrari S Mand\u00f2 G Nostro N Rucher L (2019) The SISTER approach"},{"key":"#cr-split#-e_1_2_1_2_17_2.2","doi-asserted-by":"crossref","unstructured":"for verification and validation: a lightweight process for reusable results. In: Computer safety reliability and security-SAFECOMP 2019 workshops ASSURE DECSoS SASSUR STRIVE and WAISE Turku Finland September 10 2019 proceedings pp 185-197","DOI":"10.1007\/978-3-030-26250-1_15"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Cappart Q Limbr\u00e9e C Schaus P Quilbeuf J Traonouez L-M Legay A (2017) Verification of interlocking systems using\nstatistical model checking. In: HASE. IEEE pp 61\u201368","DOI":"10.1109\/HASE.2017.10"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Cunha A Macedo N (2020) Validating the hybrid ERTMS\/ETCS level 3 concept with Electrum. Int J Softw Tools Technol\nTransf 22(3):281\u2013296","DOI":"10.1007\/s10009-019-00540-4"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Dghaym D Dalvandi M Poppleton M Snook C (2020) Formalising the hybrid ERTMS level 3 specification in iUML-B and\nEvent-B. Int J Softw Tools Technol Transf 22(3):297\u2013313","DOI":"10.1007\/s10009-019-00548-w"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"David A Larsen KG Legay A Miku\u010dionis M Poulsen DB (2015) Uppaal SMC tutorial. Int J Softw Tools Technol Transf\n17(4):397\u2013415","DOI":"10.1007\/s10009-014-0361-y"},{"key":"e_1_2_1_2_22_2","unstructured":"Ericson CA et al (2015) Hazard analysis techniques for system safety. Wiley Hoboken"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"El-Rahman S Attiya A Mamoud H Kader H (2018) Passive rfid tag for railway application. Open J Antennas Propag\n06:15\u201324","DOI":"10.4236\/ojapr.2018.62002"},{"key":"e_1_2_1_2_24_2","unstructured":"ESA (2018) Navipedia - Integrity. https:\/\/gssc.esa.int\/navipedia\/index.php\/Integrity#Protection_Level page last edited July"},{"key":"e_1_2_1_2_25_2","unstructured":"European Committee for Electrotechnical Standardization (2010) CENELEC EN 50159\u2014railway applications\u2014communication signalling and processing systems\u2014safety-related communication in transmission systems"},{"key":"e_1_2_1_2_26_2","unstructured":"European Committee for Electrotechnical Standardization (2011) CENELEC EN 50128\u2014railway applications\u2014communication signalling and processing systems\u2014Software for railway control and protection systems 01 06"},{"key":"e_1_2_1_2_27_2","unstructured":"European Committee for Electrotechnical Standardization (2017) CENELEC EN 50126-1\u2014railway applications\u2014the specification\nand demonstration of reliability availability maintainability and safety (RAMS)\u2014part 1: generic RAMS process 01\n10"},{"key":"e_1_2_1_2_28_2","unstructured":"European Committee for Electrotechnical Standardization (2017) CENELEC EN 50126-2\u2014-Railway applications\u2014the specification\nand demonstration of reliability availability maintainability and safety (RAMS)\u2014part 2: systems approach to safety 01 10"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Fantechi A(2019) Connected or autonomous trains? In: Reliability safety and security of railway systems. Modelling analysis verification and certification\u2014third international conference RSSRail 2019 Lille France June 4\u20136 2019 proceedings pp\n3\u201319","DOI":"10.1007\/978-3-030-18744-6_1"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Falco G Nicola M Falletti E (2018) An HW-in-the-loop approach for the assessment of GNSS local channel effects in the\nrailway environment. In: Proceedings of the 31st International technical meeting of the Satellite Division of The Institute of\nNavigation (ION GNSS+ 2018). Institute of Navigation pp 3463\u20133477","DOI":"10.33012\/2018.15866"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Geisler S Haxthausen AE (2021) Stepwise development and model checking of a distributed interlocking system using raise.\nForm Asp Comput 33(1):87\u2013125","DOI":"10.1007\/s00165-020-00507-2"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Glynn PW Iglehart DL (1989) Importance sampling for stochastic simulations. Manag Sci 35(11):1367\u20131392","DOI":"10.1287\/mnsc.35.11.1367"},{"key":"e_1_2_1_2_33_2","unstructured":"Groves PD Jiang Z Rudi M Strode P (2013) A portfolio approach to NLOS and multipath mitigation in dense urban areas.\nIn: Proceedings of the 26th international technical meeting of the Satellite Division of The Institute of Navigation (ION\nGNSS+ 2013). Institute of Navigation pp 3231\u20133247"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Garavel H ter Beek MH van de Pol J (2020) The 2020 expert survey on formal methods. In: ter Beek MH Ni\u010dkovi\u0107 D (eds)\nProceedings of the 25th international conference on formal methods for industrial critical systems (FMICS\u201920) volume 12327\nof LNCS Springer pp 3\u201369","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Hili N Dingel J Beaulieu A (2017) Modelling and code generation for real-time embedded systems with uml-rt and papyrus-rt.\nIn: Proceedings of the 39th international conference on software engineering companion ICSE-C \u201917. IEEE Press pp 509\u2013510","DOI":"10.1109\/ICSE-C.2017.168"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Tomas Hotzel E Ken P Golightly D Palacin R (2021) Modelling train driver behaviour in railway co-simulations. In Cleophas\nL Massink M (eds) Software engineering and formal methods. SEFM 2020 collocated workshops. Springer International\nPublishing Cham pp 249\u2013262","DOI":"10.1007\/978-3-030-67220-1_19"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Haxthausen AE Hede K (2019) Formal verification of railway timetables - using the UPPAAL Model Checker. In: From\nsoftware engineering to formal methods and tools and back volume 11865 of LNCS pp 433\u2013448","DOI":"10.1007\/978-3-030-30985-5_25"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Huang J Lv J Feng Y Luo Z Liu H Chai M (2020) A novel method on probability evaluation of zc handover scenario based\non smc. In: Qian J Liu H Cao J Zhou D (eds) Robotics and rehabilitation intelligence. Springer Singapore Singapore pp\n319\u2013333","DOI":"10.1007\/978-981-33-4929-2_22"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Hansen D Leuschel M K\u00f6rner P Krings S Naulin T Nayeri N Schneider D Skowron F (2020) Validation and real-life\ndemonstration of ETCS hybrid level 3 principles using a formal B model. Int J Softw Tools Technol Transf 22(3):315\u2013332","DOI":"10.1007\/s10009-020-00551-6"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Jegourel C Larsen KG Legay A Miku\u010dionis M Poulsen DB Sedwards S (2016) Importance sampling for stochastic timed\nautomata. In: Fr\u00e4nzle M Kapur D Zhan N(eds) Dependable software engineering: theories tools and applications. Springer\nInternational Publishing Cham pp 163\u2013178","DOI":"10.1007\/978-3-319-47677-3_11"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Kouzapas D Dardha O Perera R Gay SJ (2016) Typechecking protocols with mungo and stmungo. In: Proceedings of the\n18th international symposium on principles and practice of declarative programming PPDP \u201916. Association for Computing\nMachinery New York NY USA pp 146\u2013159","DOI":"10.1145\/2967973.2968595"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Karra SL Larsen KG FL Srba J (2019) Safe and time-optimal control for railway games. In: RSSRail volume 11495 of\nLNCS pp 106\u2013122","DOI":"10.1007\/978-3-030-18744-6_7"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Legrand C Beugin J Conrard B Marais J BerbineauM El-Miloudi E (2015) Approach for evaluating the safety of a satellitebased\ntrain localisation system through the extended integrity concept. In: Proceedings of ESREL 2015\u2014European safety\nand reliability conference","DOI":"10.1201\/b19094-170"},{"key":"#cr-split#-e_1_2_1_2_44_2.1","doi-asserted-by":"crossref","unstructured":"Larsen KG Lorber F Nielsen B (2018) 20 years of UPPAAL enabled industrial model-based validation and beyond. In:","DOI":"10.1007\/978-3-030-03427-6_18"},{"key":"#cr-split#-e_1_2_1_2_44_2.2","unstructured":"Leveraging applications of formal methods verification and validation. industrial practice-8th international symposium ISoLA 2018 Limassol Cyprus November 5-9 2018 proceedings Part IV pp 212-229"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Legay A Lukina A Traonouez LM Yang J Smolka SA Grosu R (2019) Statistical model checking. In: Steffen B Woeginger\nGJ (eds) Computing and software science: state of the art and perspectives volume 10000 of LNCS. Springer pp 478\u2013504","DOI":"10.1007\/978-3-319-91908-9_23"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Larsen KH Mikucionis M Taankvist JH (2015) Safe and optimal adaptive cruise control. In: Correct system design volume\n9360 of LNCS pp 260\u2013277","DOI":"10.1007\/978-3-319-23506-6_17"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Laursen PL Trinh VAT Haxthausen AE (2020) Formal modelling and verification of a distributed railway interlocking\nsystem using uppaal. In: Margaria T Steffen B (eds) Leveraging applications of formal methods verification and validation:\napplications. Springer International Publishing Cham pp 415\u2013433","DOI":"10.1007\/978-3-030-61467-6_27"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Li R Yin J Zhu H (2020) Modeling and analysis of rabbitmq using uppaal. In: 020 IEEE 19th international conference on\ntrust security and privacy in computing and communications (TrustCom) pp 79\u201386","DOI":"10.1109\/TrustCom50675.2020.00024"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Mammar A Frappier M Tueno Fotso SJ Laleau R (2020) A formal refinement-based analysis of the hybrid ERTMS\/ETCS\nlevel 3 standard. Int J Softw Tools Technol Transf 22(3):333\u2013347","DOI":"10.1007\/s10009-019-00543-1"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Nardone R GentileU Benerecetti M Peron A Vittorini V Marrone S Mazzocca N (2016) Modeling railway control systems\nin Promela. In: Artho C \u00d6lveczky PC (eds) Formal techniques for safety-critical systems\u2014revised selected papers of the\n4th international workshop on formal techniques for safety-critical systems (FTSCS\u201915) volume 596 of communications in\ncomputer and information science. Springer pp 121\u2013136","DOI":"10.1007\/978-3-319-29510-7_7"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Oortwijn W Huisman M (2019) Formal verification of an industrial safety-critical traffic tunnel control system. In: Ahrendt\nW Tapia Tarifa SL (eds) Integrated formal methods. Springer International Publishing pp 418\u2013436","DOI":"10.1007\/978-3-030-34968-4_23"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Puch S Fr\u00e4nzle M Gerwinn S (2018) Quantitative risk assessment of safety-critical systems via guided simulation for rare\nevents. In: Margaria T Steffen B (eds) Leveraging applications of formal methods verification and validation. Verification.\nSpringer International Publishing Cham pp 305\u2013321","DOI":"10.1007\/978-3-030-03421-4_20"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Peleska J Krafczyk N Haxthausen AE Pinger R (2019) Efficient data validation for geographical interlocking systems. In:\nReliability safety and security of railway systems. Modelling analysis verification and certification\u2014third international\nconference RSSRail 2019 Lille France June 4\u20136 2019 proceedings pp 142\u2013158","DOI":"10.1007\/978-3-030-18744-6_9"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Rispoli F Castorina M Neri A Filip A Di Mambro G Senesi F (2013)Recent progress in application of GNSS and advanced\ncommunications for railway signaling. In: Proceedings of the 23rd international conference radioelektronika (RADIOELEKTRONIKA\n2013). IEEE pp 13\u201322","DOI":"10.1109\/RadioElek.2013.6530882"},{"key":"e_1_2_1_2_55_2","unstructured":"Shift2Rail Joint Undertaking (2015) Multi-Annual Action Plan 26 November. http:\/\/ec.europa.eu\/research\/participants\/data\/ref\/h2020\/other\/wp\/jtis\/h2020-maap-shift2rail_en.pdf."},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Shokri-Manninen F Tsiopoulos L Vain J Wald\u00e9n M (2020) Integration of iUML-B and UPPAAL timed automata for\ndevelopment of real-time systems with concurrent processes. In: Raschke A M\u00e9ry D Houdek F (eds) Rigorous state-based\nmethods. Springer International Publishing pp 186\u2013202","DOI":"10.1007\/978-3-030-48077-6_13"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Shokri-Manninen F Vain J Wald\u00e9n M (2020) Formal verification of colreg-based navigation of maritime autonomous systems.\nIn: de Boer F Cerone A (eds) Software engineering and formal methods. Springer International Publishing Cham pp 41\u201359","DOI":"10.1007\/978-3-030-58768-0_3"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"ter Beek MH Gnesi S Knapp A (2018) Formal methods for transport systems. Int J Softw Tools Technol Transf 20(3)","DOI":"10.1007\/s10009-018-0487-4"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Thamilselvam B Kalyanasundaram S Panduranga Rao MV (2019) Coordinated intelligent traffic lights using UPPAAL\nstratego. In: COMSNETS. IEEE pp 789\u2013794","DOI":"10.1109\/COMSNETS.2019.8711457"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00556-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00556-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00556-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00556-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,21]],"date-time":"2022-04-21T20:45:21Z","timestamp":1650573921000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00556-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":63,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["10.1007\/s00165-021-00556-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00556-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"7 August 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 June 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 July 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}