Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
Rigorous State-Based Methods
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations
David Geleßus, Sebastian Stock, Fabian Vu, Michael Leuschel & Atif Mashkoor
Conference paper
First Online: 15 May 2023
210 Accesses
1 Citations
Part of the Lecture Notes in Computer Science book series (LNCS,volume 14010)
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?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.
Forschungs-