Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations

Gele{\ss}us, David; Stock, Sebastian; Vu, Fabian; Leuschel, Michael; Mashkoor, Atif

by Geleßus, David, Stock, Sebastian, Vu, Fabian, Leuschel, Michael and Mashkoor, Atif

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.

Reference:

Geleßus, David, Stock, Sebastian, Vu, Fabian, Leuschel, Michael and Mashkoor, Atif: Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations, in Rigorous State-Based Methods (Glässer, Uwe, Creissac Campos, Jose, Méry, Dominique, Palanque, Philippe, eds.), Springer Nature Switzerland, 2023.

Bibtex Entry:

@Conference{Gelessus2023,
  author    = {Gele{\ss}us, David and Stock, Sebastian and Vu, Fabian and Leuschel, Michael and Mashkoor, Atif},
  booktitle = {Rigorous State-Based Methods},
  title     = {Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations},
  year      = {2023},
  address   = {Cham},
  editor    = {Gl{\"a}sser, Uwe and Creissac Campos, Jose and M{\'e}ry, Dominique and Palanque, Philippe},
  pages     = {284--302},
  publisher = {Springer Nature Switzerland},
  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.},
  isbn      = {978-3-031-33163-3},
}