@inproceedings{f81bcd6e52c84527aa35e050390e71db,
title = "Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations",
abstract = "This paper presents insights gained during modeling and analyzing the arrival manager (AMAN) case study in Event-B with validation obligations (VOs). AMAN is a safety-critical interactive system for air traffic controllers to organize the landing of airplanes at airports. The presented model consists of a human-machine interface comprising interactive and autonomous parts. We employ VOs to formalize requirements, uncover contradictions and ambiguities, and validate the model{\textquoteright}s compliance with the requirements. To capture the AMAN{\textquoteright}s human-machine interaction, we implement an interactive domain-specific visualization and an automatic simulation using the VisB and SimB components of ProB.",
author = "David Gele{\ss}us and Sebastian Stock and Fabian Vu and Michael Leuschel and Atif Mashkoor",
year = "2023",
month = may,
doi = "10.1007/978-3-031-33163-3\_22",
language = "English",
isbn = "978-3-031-33162-6",
volume = "14010",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "284--302",
editor = "Uwe Gl{\"a}sser and \{Creissac Campos\}, Jose and Dominique M{\'e}ry and Philippe Palanque",
booktitle = "Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Proceedings",
}