{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T23:16:40Z","timestamp":1770938200202,"version":"3.50.1"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"name":"\u201cDeutsche Forschungsgemeinschaft\u201d (DFG) and the Austrian Science Fund","award":["I 4744-N"],"award-info":[{"award-number":["I 4744-N"]}]},{"name":"LIT Secure and Correct Systems Lab"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>\n                    This article presents an Event-B model and an interactive GUI prototype for an air traffic control system called the arrival manager (AMAN). AMAN is a safety-critical interactive system designed for air traffic controllers to manage landings at an airport. The presented formal model consists of a human-machine interface comprising interactive and autonomous parts. Safety properties of the system were proven using the Rodin platform, while validation was carried out using the ProB tool. We turned the formal model into an executable AMAN prototype by combining interactive domain-specific visualizations and automatic simulation using the\n                    <jats:sc>VisB<\/jats:sc>\n                    and\n                    <jats:sc>SimB<\/jats:sc>\n                    components of\n                    <jats:sc>ProB<\/jats:sc>\n                    . We used validation obligations (VOs) to systematically validate the model\u2019s and the prototype\u2019s compliance with the requirements and uncovered some contradictions and ambiguities in the case study.\n                  <\/jats:p>","DOI":"10.1145\/3774647","type":"journal-article","created":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T11:53:15Z","timestamp":1763380395000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Development and Validation of a Formal Model and Prototype for an Air Traffic Control System"],"prefix":"10.1145","volume":"38","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6722-6296","authenticated-orcid":false,"given":"David","family":"Gele\u00dfus","sequence":"first","affiliation":[{"name":"Heinrich-Heine-Universit\u00e4t","place":["Dusseldorf, Germany"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2231-8656","authenticated-orcid":false,"given":"Sebastian","family":"Stock","sequence":"additional","affiliation":[{"name":"Johannes Kepler Universit\u00e4t","place":["Linz, Austria"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2556-5553","authenticated-orcid":false,"given":"Fabian","family":"Vu","sequence":"additional","affiliation":[{"name":"Heinrich-Heine-Universit\u00e4t","place":["Dusseldorf, Germany"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[{"name":"Heinrich-Heine-Universit\u00e4t","place":["Dusseldorf, Germany"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1210-5953","authenticated-orcid":false,"given":"Atif","family":"Mashkoor","sequence":"additional","affiliation":[{"name":"College of Computing, Grand Valley State University","place":["Allendale, United States"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,2,12]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Jean-Raymond Abrial Michael Butler Stefan Hallerstede Thai Son Hoang Farhad Mehta and Laurent Voisin. 2010. Rodin: An open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer 12 6 (Nov.2010) 447\u2013466. DOI:10.1007\/s10009-010-0145-y","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_3_2_4_2","series-title":"LNCS","first-page":"1","volume-title":"Proceedings of the TPHOLs","author":"Agerholm Sten","year":"1996","unstructured":"Sten Agerholm. 1996. Translating specifications in VDM-SL to PVS. In Proceedings of the TPHOLs(LNCS, 5674). Springer, 1\u201316. DOI:10.1007\/BFb0105393"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Yamine A\u00eft-Ameur Idir A\u00eft-Sadoune Mickael Baron and Jean-Marc Mota. 2014. V\u00e9rification et validation formelles de syst\u00e8mes interactifs fond\u00e9es sur la preuve : Application aux syst\u00e8mes Multi-Modaux. Journal d\u2019Interaction Personne-Syst\u00e8me 1 (102014) 1\u201330. DOI:10.46298\/jips.59","DOI":"10.46298\/jips.59"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"R\u00e9mi Bastide David Navarre and Philippe Palanque. 2003. A tool-supported design framework for safety critical interactive systems. Interacting with Computers 15 3 (2003) 309\u2013328. DOI:10.1016\/S0953-5438(03)00011-0. Computer-Aided Design of User Interface.","DOI":"10.1016\/S0953-5438(03)00011-0"},{"key":"e_1_3_2_7_2","volume-title":"Hamsters - A New Task Model for Interactive Systems","author":"Amor Mohamed Ben","year":"2009","unstructured":"Mohamed Ben Amor. 2009. Hamsters - A New Task Model for Interactive Systems. Master\u2019s thesis. Universitaire Notre Dame de la Paix. Retrieved from https:\/\/pure.unamur.be\/ws\/portalfiles\/portal\/36772355\/2009_BenAmorM_memoire.pdf"},{"key":"e_1_3_2_8_2","series-title":"LNCS","first-page":"193","volume-title":"Proceedings of the FMICS","author":"Bendisposto Jens","year":"2021","unstructured":"Jens Bendisposto, David Gele\u00dfus, Yumiko Jansing, Michael Leuschel, Antonia P\u00fctz, Fabian Vu, and Michelle Werth. 2021. ProB2-UI: A Java-based user interface for ProB. In Proceedings of the FMICS(LNCS, 12863). Springer, 193\u2013201. DOI:10.1007\/978-3-030-85248-1_12"},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/3-540-09541-1_33","volume-title":"Proceedings of the Mathematical Studies of Information Processing","author":"Bj\u00f8rner Dines","year":"1979","unstructured":"Dines Bj\u00f8rner. 1979. The vienna development method (VDM). In Proceedings of the Mathematical Studies of Information Processing, E. K. Blum, M. Paul, and S. Takasu (Eds.). Springer Berlin, Berlin,, 326\u2013359. DOI:10.1007\/3-540-09541-1_33"},{"key":"e_1_3_2_10_2","series-title":"LNCS","first-page":"340","volume-title":"Proceedings of the ABZ","author":"Bombarda Andrea","year":"2023","unstructured":"Andrea Bombarda, Silvia Bonfanti, and Angelo Gargantini. 2023. formal MVC: A pattern for the integration of ASM specifications in UI development. In Proceedings of the ABZ(LNCS, 14010). Springer, 340\u2013357. DOI:10.1007\/978-3-031-33163-3_25"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Jos\u00e9 Creissac Campos Camille Fayollas Michael D. Harrison C\u00e9lia Martinie Paolo Masci and Philippe A. Palanque. 2020. Supporting the analysis of safety critical user interfaces: An exploration of three formal tools. ACM Transactions on Computer-Human Interaction 27 5 (2020) 35:1\u201335:48. DOI:10.1145\/3404199","DOI":"10.1145\/3404199"},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/978-3-540-70569-7_6","volume-title":"Proceedings of the Interactive Systems. Design, Specification, and Verification","author":"Campos J. Creissac","year":"2008","unstructured":"J. Creissac Campos and M. D. Harrison. 2008. Systematic analysis of control panel interfaces using formal tools. In Proceedings of the Interactive Systems. Design, Specification, and Verification, T. C. Nicholas Graham and Philippe Palanque (Eds.). Springer Berlin, Berlin,, 72\u201385. DOI:10.1007\/978-3-540-70569-7_6"},{"key":"e_1_3_2_13_2","series-title":"EPTCS","first-page":"14","volume-title":"Proceedings of the F-IDE","volume":"187","author":"Couto Lu\u00eds Diogo","year":"2015","unstructured":"Lu\u00eds Diogo Couto, Peter Gorm Larsen, Miran Hasanagi\u0107, Georgios Kanakis, Kenneth Lausdahl, and Peter W. V. Tran-J\u00f8rgensen. 2015. Towards enabling overture as a platform for formal notation IDEs. In Proceedings of the F-IDE(EPTCS, Vol. 187), Catherine Dubois, Paolo Masci, and Dominique M\u00e9ry (Eds.). Open Publishing Association, 14\u201327. DOI:10.4204\/EPTCS.187.2"},{"key":"e_1_3_2_14_2","first-page":"303","volume-title":"Proceedings of the ABZ","author":"Cunha Alcino","year":"2023","unstructured":"Alcino Cunha, Nuno Macedo, and Eunsuk Kang. 2023. Task model design and analysis with alloy. In Proceedings of the ABZ, Uwe Gl\u00e4sser, Jose Creissac Campos, Dominique M\u00e9ry, and Philippe Palanque (Eds.). Springer Nature Switzerland, Cham, 303\u2013320. DOI:10.1007\/978-3-031-33163-3_23"},{"key":"e_1_3_2_15_2","first-page":"242","volume-title":"Proceedings of the Design, Specification and Verification of Interactive Systems\u201998","author":"d\u2019Ausbourg Bruno","year":"1998","unstructured":"Bruno d\u2019Ausbourg. 1998. Using model checking for the automatic validation of user interfaces systems. In Proceedings of the Design, Specification and Verification of Interactive Systems\u201998, Panos Markopoulos and Peter Johnson (Eds.). Springer Vienna, Vienna, 242\u2013260. DOI:10.1007\/978-3-7091-3693-5_16"},{"key":"e_1_3_2_16_2","first-page":"9","volume-title":"Proceedings of the Perspectives on HCI: Diverse Approaches","author":"Dix A. J.","year":"1995","unstructured":"A. J. Dix. 1995. Formal methods. In Proceedings of the Perspectives on HCI: Diverse Approaches. Academic Press, London, 9\u201343. Retrieved from https:\/\/www.alandix.com\/academic\/papers\/formal-chapter-95\/formal-chapter-95.pdf"},{"key":"e_1_3_2_17_2","first-page":"465","volume-title":"Proceedings of the Handbook of Formal Methods in Human-Computer Interaction","author":"Fayollas Camille","year":"2017","unstructured":"Camille Fayollas, C\u00e9lia Martinie, Philippe Palanque, Eric Barboni, Racim Fahssi, and Arnaud Hamon. 2017. Exploiting action theory as a framework for analysis and design of formal methods approaches: Application to the circus integrated development environment. In Proceedings of the Handbook of Formal Methods in Human-Computer Interaction, Benjamin Weyers, Judy Bowen, Alan Dix, and Philippe Palanque (Eds.). Springer International Publishing, Cham, 465\u2013504. DOI:10.1007\/978-3-319-51838-1_17"},{"key":"e_1_3_2_18_2","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/978-3-662-44811-3_9","volume-title":"Proceedings of the Human-Centered Software Engineering","author":"Forbrig Peter","year":"2014","unstructured":"Peter Forbrig, C\u00e9lia Martinie, Philippe Palanque, Marco Winckler, and Racim Fahssi. 2014. Rapid task-models development using sub-models, sub-routines and generic components. In Proceedings of the Human-Centered Software Engineering. Springer Berlin, Berlin,, 144\u2013163. DOI:10.1007\/978-3-662-44811-3_9"},{"key":"e_1_3_2_19_2","first-page":"373","volume-title":"Proceedings of the 3rd International Conference on Software Engineering Advances","author":"Gargantini Angelo","year":"2008","unstructured":"Angelo Gargantini, Elvinia Riccobene, and Patrizia Scandurra. 2008. Model-driven language engineering: The ASMETA case study. In Proceedings of the 3rd International Conference on Software Engineering Advances. IEEE, 373\u2013378. DOI:10.1109\/ICSEA.2008.62"},{"key":"e_1_3_2_20_2","first-page":"1","volume-title":"Proceedings of the 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)","author":"Ge Ning","year":"2017","unstructured":"Ning Ge, Arnaud Dieumegard, Eric Jenn, Bruno d\u2019Ausbourg, and Yamine A\u00eft-Ameur. 2017. Formal development process of safety-critical embedded human machine interface systems. In Proceedings of the 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE, 1\u20138. DOI:10.1109\/TASE.2017.8285636"},{"key":"e_1_3_2_21_2","series-title":"LNCS","first-page":"284","volume-title":"Proceedings of the ABZ","author":"Gele\u00dfus David","year":"2023","unstructured":"David Gele\u00dfus, Sebastian Stock, Fabian Vu, Michael Leuschel, and Atif Mashkoor. 2023. Modeling and analysis of a safety-critical interactive system through validation obligations. In Proceedings of the ABZ(LNCS, 14010). Springer, 284\u2013302. DOI:10.1007\/978-3-031-33163-3_22"},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/978-3-030-04771-9_19","volume-title":"Proceedings of the Software Technologies: Applications and Foundations","author":"Geniet Romain","year":"2018","unstructured":"Romain Geniet and Neeraj Kumar Singh. 2018. Refinement based formal development of human-machine interface. In Proceedings of the Software Technologies: Applications and Foundations, Manuel Mazzara, Iulian Ober, and Gwen Sala\u00fcn (Eds.). Springer International Publishing, Cham, 240\u2013256. DOI:10.1007\/978-3-030-04771-9_19"},{"key":"e_1_3_2_23_2","volume-title":"Towards Infinite-State Symbolic Model Checking for B and Event-B","author":"Krings Sebastian","year":"2017","unstructured":"Sebastian Krings. 2017. Towards Infinite-State Symbolic Model Checking for B and Event-B. Ph. D. Dissertation. Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf."},{"key":"e_1_3_2_24_2","series-title":"LNCS","first-page":"153","volume-title":"Proceedings of the ICFEM","author":"Ladenberger Lukas","year":"2015","unstructured":"Lukas Ladenberger and Michael Leuschel. 2015. Mastering the visualization of larger state spaces with projection diagrams. In Proceedings of the ICFEM(LNCS, 9407). Springer, 153\u2013169. DOI:10.1007\/978-3-319-25423-4_10"},{"key":"e_1_3_2_25_2","series-title":"LNCS","first-page":"162","volume-title":"Proceedings of the CHARME","author":"Lamport Leslie","year":"2005","unstructured":"Leslie Lamport. 2005. Real-time model checking is really simple. In Proceedings of the CHARME(LNCS, 3725). Springer, 162\u2013175. DOI:10.1007\/11560548_14"},{"key":"e_1_3_2_26_2","series-title":"LNCS","first-page":"129","volume-title":"Proceedings of the iFM","author":"Leuschel Michael","year":"2022","unstructured":"Michael Leuschel. 2022. Operation caching and state compression for model checking of high-level models - how to have your cake and eat it. In Proceedings of the iFM(LNCS, 13274). Springer, 129\u2013145. DOI:10.1007\/978-3-031-07727-2_8"},{"key":"e_1_3_2_27_2","first-page":"855","volume-title":"Proceedings of the International Symposium of Formal Methods Europe","author":"Leuschel Michael","year":"2003","unstructured":"Michael Leuschel and Michael Butler. 2003. ProB: A model checker for B. In Proceedings of the International Symposium of Formal Methods Europe. Springer, 855\u2013874. DOI:10.1007\/978-3-540-45236-2_46"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Michael Leuschel and Michael J. Butler. 2008. ProB: An automated analysis toolset for the B method. STTT 10 2 (2008) 185\u2013203. DOI:10.1007\/s10009-007-0063-9","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_3_2_29_2","series-title":"LNCS","first-page":"321","volume-title":"Proceedings of the ABZ","author":"Mammar Amel","year":"2023","unstructured":"Amel Mammar and Michael Leuschel. 2023. Modeling and verifying an arrival manager using Event-B. In Proceedings of the ABZ(LNCS, 14010). Springer, 321\u2013339. DOI:10.1007\/978-3-031-33163-3_24"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","first-page":"589","DOI":"10.1007\/978-3-642-23765-2_40","volume-title":"Proceedings of the Human-Computer Interaction \u2013 INTERACT 2011","author":"Martinie C\u00e9lia","year":"2011","unstructured":"C\u00e9lia Martinie, Philippe Palanque, and Marco Winckler. 2011. Structuring and composition mechanisms to address scalability issues in task models. In Proceedings of the Human-Computer Interaction \u2013 INTERACT 2011. Springer Berlin, Berlin,, 589\u2013609. DOI:10.1007\/978-3-642-23765-2_40"},{"key":"e_1_3_2_31_2","series-title":"LNCS","first-page":"155","volume-title":"Proceedings of the TAP@STAF 2020","author":"Masci Paolo","year":"2020","unstructured":"Paolo Masci and C\u00e9sar A. Mu\u00f1oz. 2020. A graphical toolkit for the validation of requirements for detect and avoid systems. In Proceedings of the TAP@STAF 2020(LNCS, 12165). Springer, 155\u2013166. DOI:10.1007\/978-3-030-50995-8_9"},{"key":"e_1_3_2_32_2","first-page":"1","volume-title":"Proceedings of the ICSE\u201921 NIER","author":"Mashkoor Atif","year":"2021","unstructured":"Atif Mashkoor, Michael Leuschel, and Alexander Egyed. 2021. Validation obligations: A novel approach to check compliance between requirements and their formal specification. In Proceedings of the ICSE\u201921 NIER. IEEE, 1\u20135. DOI:10.1109\/ICSE-NIER52604.2021.00009"},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1109\/APSEC51365.2020.00022","volume-title":"Proceedings of the 2020 27th Asia-Pacific Software Engineering Conference (APSEC)","author":"Mendil Ismail","year":"2020","unstructured":"Ismail Mendil, Neeraj Kumar Singh, Yamine Ait-Ameur, Dominique M\u00e9ry, and Philippe Palanque. 2020. An integrated framework for the formal analysis of critical interactive systems. In Proceedings of the 2020 27th Asia-Pacific Software Engineering Conference (APSEC). IEEE, 139\u2013148. DOI:10.1109\/APSEC51365.2020.00022"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/3-540-45522-1_6","volume-title":"Proceedings of the Interactive Systems: Design, Specification, and Verification","author":"Navarre David","year":"2001","unstructured":"David Navarre, Philippe Palanque, Fabio Patern\u00f2, Carmen Santoro, and R\u00e9mi Bastide. 2001. A tool suite for integrating task and system models through scenarios. In Proceedings of the Interactive Systems: Design, Specification, and Verification. Springer Berlin, Berlin,, 88\u2013113. DOI:10.1007\/3-540-45522-1_6"},{"key":"e_1_3_2_35_2","first-page":"399","volume-title":"Proceedings of the ICSEA","author":"Nunes Carlos","year":"2011","unstructured":"Carlos Nunes and Ana Cristina Ramada Paiva. 2011. Automatic generation of graphical user interfaces from VDM++ specifications. In Proceedings of the ICSEA. IARIA XPS Press, 399\u2013404. Retrieved from https:\/\/www.thinkmind.org\/articles\/icsea_2011_17_20_10244.pdf"},{"key":"e_1_3_2_36_2","first-page":"5","volume-title":"Proceedings of the 18th International Overture Workshop","author":"Oda Tomohiro","year":"2020","unstructured":"Tomohiro Oda, Keijiro Araki, Yasuhiro Yamamoto, Kumiyo Nakakoji, Han-Myung Chang, and Peter Larsen. 2020. Specifying abstract user interface in VDM-SL. In Proceedings of the 18th International Overture Workshop, John S Fitzgerald and Tomohiro Oda (Eds.). 5\u201319. arXiv:2101.07261. Retrieved from https:\/\/arxiv.org\/abs\/2101.07261DOI:10.48550\/arXiv.2101.07261"},{"key":"e_1_3_2_37_2","series-title":"LNCS","first-page":"748","volume-title":"Proceedings of the Automated Deduction\u2014CADE-11","author":"Owre S.","year":"1992","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. 1992. PVS: A prototype verification system. In Proceedings of the Automated Deduction\u2014CADE-11(LNCS, 607). Springer, 748\u2013752. DOI:10.1007\/3-540-55602-8_217"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-33163-3_21"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Maurizio Palmieri Cinzia Bernardeschi and Paolo Masci. 2020. A framework for FMI-based co-simulation of human-machine interfaces. Software and Systems Modeling 19 3 (2020) 601\u2013623. DOI:10.1007\/S10270-019-00754-9","DOI":"10.1007\/S10270-019-00754-9"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Daniel Plagge and Michael Leuschel. 2010. Seven at one stroke: LTL model checking for high-level specifications in B Z CSP and more. STTT 12 1 (2010) 9\u201321. DOI:10.1007\/s10009-009-0132-3","DOI":"10.1007\/s10009-009-0132-3"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Joris Rehm. 2010. Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method. STTT 12 1 (2010) 39\u201351. DOI:10.1007\/s10009-009-0130-5","DOI":"10.1007\/s10009-009-0130-5"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Neeraj Singh Yamine A\u00eft-Ameur Ismail Mendil Dominique Mery David Navarre Philippe Palanque and Marc Pantel. 2022. F3FLUID: A formal framework for developing safety-critical interactive systems in FLUID. Journal of Software: Evolution and Process 35 (032022) e2439. DOI:10.1002\/smr.2439","DOI":"10.1002\/smr.2439"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Neeraj Kumar Singh Yamine A\u00eft-Ameur Romain Geniet Dominique M\u00e9ry and Philippe Palanque. 2021. On the benefits of using MVC pattern for structuring event-b models of WIMP interactive applications. Interacting with Computers 33 1 (052021) 92\u2013114. DOI:10.1093\/iwcomp\/iwab016","DOI":"10.1093\/iwcomp\/iwab016"},{"key":"e_1_3_2_44_2","series-title":"LNCS","first-page":"191","volume-title":"Proceedings of the ICFEM","author":"Stock Sebastian","year":"2023","unstructured":"Sebastian Stock, Atif Mashkoor, and Alexander Egyed. 2023. Validation-driven development. In Proceedings of the ICFEM(LNCS, 14308). Springer, 191\u2013207. DOI:10.1007\/978-981-99-7584-6_12"},{"key":"e_1_3_2_45_2","series-title":"LNCS","first-page":"160","volume-title":"Proceedings of the ABZ","author":"Stock Sebastian","year":"2023","unstructured":"Sebastian Stock, Fabian Vu, David Gele\u00dfus, Michael Leuschel, Atif Mashkoor, and Alexander Egyed. 2023. Validation by abstraction and refinement. In Proceedings of the ABZ(LNCS, 14010). Springer, 160\u2013178. DOI:10.1007\/978-3-031-33163-3_12"},{"key":"e_1_3_2_46_2","unstructured":"Sebastian Stock Fabian Vu Atif Mashkoor Michael Leuschel and Alexander Egyed. 2022. IVOIRE deliverable 1.1: Classification of existing VOs & tools and formalization of VOs semantics. arXiv:2205.06138. Retrieved from https:\/\/arxiv.org\/abs\/2205.06138. (2022)."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Casper Thule Kenneth Lausdahl Cl\u00e1udio Gomes Gerd Meisl and Peter Gorm Larsen. 2019. Maestro: The INTO-CPS co-simulation framework. Simulation Modelling Practice and Theory 92 (2019) 45\u201361. DOI:10.1016\/j.simpat.2018.12.005","DOI":"10.1016\/j.simpat.2018.12.005"},{"key":"e_1_3_2_48_2","series-title":"LNCS","first-page":"59","volume-title":"Proceedings of the ABZ","author":"Vu Fabian","year":"2023","unstructured":"Fabian Vu and Michael Leuschel. 2023. Validation of formal models by interactive simulation. In Proceedings of the ABZ(LNCS, 14010). Springer, 59\u201369. DOI:10.1007\/978-3-031-33163-3_5"},{"key":"e_1_3_2_49_2","series-title":"LNCS","first-page":"81","volume-title":"Proceedings of the ABZ","author":"Vu Fabian","year":"2021","unstructured":"Fabian Vu, Michael Leuschel, and Atif Mashkoor. 2021. Validation of formal models by timed probabilistic simulation. In Proceedings of the ABZ(LNCS, 12709). Springer, 81\u201396. DOI:10.1007\/978-3-030-77543-8_6"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-91603-7_9"},{"key":"e_1_3_2_51_2","first-page":"95","volume-title":"Proceedings of the F-IDE (EPTCS 284)","author":"Watson Nathaniel","year":"2018","unstructured":"Nathaniel Watson, Steve Reeves, and Paolo Masci. 2018. Integrating user design and formal models within PVSio-Web. In Proceedings of the F-IDE (EPTCS 284). Open Publishing Association, 95\u2013104. DOI:10.4204\/EPTCS.284.8"},{"key":"e_1_3_2_52_2","series-title":"LNCS","first-page":"260","volume-title":"Proceedings of the ABZ","author":"Werth Michelle","year":"2020","unstructured":"Michelle Werth and Michael Leuschel. 2020. VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics. In Proceedings of the ABZ(LNCS, 12071). Springer, 260\u2013265. DOI:10.1007\/978-3-030-48077-6_21"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3774647","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T22:20:29Z","timestamp":1770934829000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3774647"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,12]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3774647"],"URL":"https:\/\/doi.org\/10.1145\/3774647","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,12]]},"assertion":[{"value":"2024-11-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-30","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}