{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:41:16Z","timestamp":1764873676262,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":15,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T00:00:00Z","timestamp":1567987200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,9,9]]},"DOI":"10.1145\/3344948.3344993","type":"proceedings-article","created":{"date-parts":[[2019,9,5]],"date-time":"2019-09-05T12:16:25Z","timestamp":1567685785000},"page":"156-162","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["A formal design of the hybrid European rail traffic management system"],"prefix":"10.1145","author":[{"given":"Paolo","family":"Gaspari","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano - Italy"}]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano - Italy"}]},{"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Bergamo - Italy"}]}],"member":"320","published-online":{"date-parts":[[2019,9,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM","author":"Abrial Jean-Raymond","year":"2018","unstructured":"Jean-Raymond Abrial . 2018. The ABZ-2018 Case Study with Event-B . In Abstract State Machines, Alloy, B, TLA, VDM , and Z, ABZ 2018 , Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817 . Springer , 322--337. Jean-Raymond Abrial. 2018. The ABZ-2018 Case Study with Event-B. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2018, Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817. Springer, 322--337."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.1019"},{"key":"e_1_3_2_1_3_1","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM","author":"Arcaini Paolo","year":"2018","unstructured":"Paolo Arcaini , Pavel Jezek , and Jan Kofron . 2018. Modelling the Hybrid ERTMS\/ETCS Level 3 Case Study in Spin . In Abstract State Machines, Alloy, B, TLA, VDM , and Z, ABZ 2018 , Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817 . Springer , 277--291. Paolo Arcaini, Pavel Jezek, and Jan Kofron. 2018. Modelling the Hybrid ERTMS\/ETCS Level 3 Case Study in Spin. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2018, Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817. Springer, 277--291."},{"key":"e_1_3_2_1_4_1","volume-title":"St\u00e4rk","author":"B\u00f6rger Egon","year":"2003","unstructured":"Egon B\u00f6rger and Robert F . St\u00e4rk . 2003 . Abstract State Machines: A Method for High-Level System Design and Analysis. Springer , Berlin, Heidelberg. Egon B\u00f6rger and Robert F. St\u00e4rk. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Berlin, Heidelberg."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_7"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_29"},{"key":"e_1_3_2_1_7_1","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM","author":"Cunha Alcino","year":"2018","unstructured":"Alcino Cunha and Nuno Macedo . 2018. Validating the Hybrid ERTMS\/ETCS Level 3 Concept with Electrum . In Abstract State Machines, Alloy, B, TLA, VDM , and Z, ABZ 2018 , Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817 . Springer , 307--321. Alcino Cunha and Nuno Macedo. 2018. Validating the Hybrid ERTMS\/ETCS Level 3 Concept with Electrum. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2018, Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817. Springer, 307--321."},{"key":"e_1_3_2_1_8_1","volume-title":"Snook","author":"Dghaym Dana","year":"2018","unstructured":"Dana Dghaym , Michael Poppleton , and Colin F . Snook . 2018 . Diagram-Led Formal Modelling Using iUML-B for Hybrid ERTMS Level 3. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2018, Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817 . Springer , 338--352. Dana Dghaym, Michael Poppleton, and Colin F. Snook. 2018. Diagram-Led Formal Modelling Using iUML-B for Hybrid ERTMS Level 3. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2018, Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817. Springer, 338--352."},{"key":"e_1_3_2_1_9_1","volume-title":"RSSRail 2017, Pistoia, Italy, November 14-16, 2017, Proceedings. Lecture Notes in Computer Science","volume":"10598","author":"Fantechi Alessandro","unstructured":"Alessandro Fantechi , Thierry Lecomte , and Alexander B . Romanovsky (Eds.). 2017. Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification - Second International Conference , RSSRail 2017, Pistoia, Italy, November 14-16, 2017, Proceedings. Lecture Notes in Computer Science , Vol. 10598 . Springer. Alessandro Fantechi, Thierry Lecomte, and Alexander B. Romanovsky (Eds.). 2017. Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification - Second International Conference, RSSRail 2017, Pistoia, Italy, November 14-16, 2017, Proceedings. Lecture Notes in Computer Science, Vol. 10598. Springer."},{"key":"e_1_3_2_1_10_1","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM","author":"Tueno Fotso Steve Jeffrey","year":"2018","unstructured":"Steve Jeffrey Tueno Fotso , Marc Frappier , R\u00e9gine Laleau , and Amel Mammar . 2018. Modeling the Hybrid ERTMS\/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach . In Abstract State Machines, Alloy, B, TLA, VDM , and Z, ABZ 2018 , Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817 . Springer , 262--276. Steve Jeffrey Tueno Fotso, Marc Frappier, R\u00e9gine Laleau, and Amel Mammar. 2018. Modeling the Hybrid ERTMS\/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2018, Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817. Springer, 262--276."},{"key":"e_1_3_2_1_11_1","unstructured":"N. Furness H. van Houten L. Arenas and M. Bartholomeus. 2017. ERTMS level 3: the game-changer. IRSE News View 232 (April 2017).  N. Furness H. van Houten L. Arenas and M. Bartholomeus. 2017. ERTMS level 3: the game-changer. IRSE News View 232 (April 2017)."},{"key":"e_1_3_2_1_12_1","unstructured":"EEIG ERTMS Users Group. {n. d.}. Principles-Hybrid ERTMS\/ETCS Level 3 13\/07\/2018. http:\/\/www.ertms.be\/sites\/default\/files\/2018-07\/16E0421C_HL3-clean.pdf  EEIG ERTMS Users Group. {n. d.}. Principles-Hybrid ERTMS\/ETCS Level 3 13\/07\/2018. http:\/\/www.ertms.be\/sites\/default\/files\/2018-07\/16E0421C_HL3-clean.pdf"},{"key":"e_1_3_2_1_13_1","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM","author":"Hansen Dominik","year":"2018","unstructured":"Dominik Hansen , Michael Leuschel , David Schneider , Sebastian Krings , Philipp K\u00f6rner , Thomas Naulin , Nader Nayeri , and Frank Skowron . 2018. Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains . In Abstract State Machines, Alloy, B, TLA, VDM , and Z, ABZ 2018 , Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817 . Springer , 292--306. Dominik Hansen, Michael Leuschel, David Schneider, Sebastian Krings, Philipp K\u00f6rner, Thomas Naulin, Nader Nayeri, and Frank Skowron. 2018. Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ2018, Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817. Springer, 292--306."},{"key":"e_1_3_2_1_14_1","volume-title":"Steve Jeffrey Tueno Fotso, and R\u00e9gine Laleau","author":"Mammar Amel","year":"2018","unstructured":"Amel Mammar , Marc Frappier , Steve Jeffrey Tueno Fotso, and R\u00e9gine Laleau . 2018 . An Event-B Model of the Hybrid ERTMS\/ETCS Level 3 Standard. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2018, Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817 . Springer , 353--366. Amel Mammar, Marc Frappier, Steve Jeffrey Tueno Fotso, and R\u00e9gine Laleau. 2018. An Event-B Model of the Hybrid ERTMS\/ETCS Level 3 Standard. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2018, Proceedings (Lecture Notes in Computer Science), M. Butler, A. Raschke, T. Son Hoang, and K. Reichl (Eds.), Vol. 10817. Springer, 353--366."},{"key":"e_1_3_2_1_15_1","article-title":"Formal Methods for the Railway Sector","volume":"2018","author":"Beek Maurice H.","year":"2018","unstructured":"Maurice H. ter Beek , Alessandro Fantechi , Alessio Ferrari , Stefania Gnesi , and Riccardo Scopigno . 2018 . Formal Methods for the Railway Sector . ERCIM News 2018 , 112 (2018). https:\/\/ercim-news.ercim.eu\/en112\/r-i\/formal-methods-for-the-railway-sector Maurice H. ter Beek, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi, and Riccardo Scopigno. 2018. Formal Methods for the Railway Sector. ERCIM News 2018, 112 (2018). https:\/\/ercim-news.ercim.eu\/en112\/r-i\/formal-methods-for-the-railway-sector","journal-title":"ERCIM News"}],"event":{"name":"ECSA: European Conference on Software Architecture","acronym":"ECSA","location":"Paris France"},"container-title":["Proceedings of the 13th European Conference on Software Architecture - Volume 2"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3344948.3344993","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3344948.3344993","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:54:28Z","timestamp":1750204468000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3344948.3344993"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,9]]},"references-count":15,"alternative-id":["10.1145\/3344948.3344993","10.1145\/3344948"],"URL":"https:\/\/doi.org\/10.1145\/3344948.3344993","relation":{},"subject":[],"published":{"date-parts":[[2019,9,9]]},"assertion":[{"value":"2019-09-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}