David Geleßus, Sebastian Stock, Fabian Vu, Michael Leuschel, Atif Mashkoor,
"Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations"
: Rigorous State-Based Methods, Serie Lecture Notes in Computer Science (LNCS), Vol. 14010, Seite(n) 284-302, 5-2023, ISBN: 978-3-031-33162-6
Original Titel:
Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations
Sprache des Titels:
Englisch
Original Buchtitel:
Rigorous State-Based Methods
Original Kurzfassung:
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?s compliance with the requirements. To capture the AMAN?s human-machine interaction, we implement an interactive domain-specific visualization and an automatic simulation using the VisB and SimB components of ProB.