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

David Geleßus; Sebastian Stock; Fabian Vu; Michael Leuschel; Atif Mashkoor

doi:10.1007/978-3-031-33163-3_22

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

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

LIT Secure and Correct Systems Lab

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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.

Original language	English
Title of host publication	Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Proceedings
Editors	Uwe Glässer, Jose Creissac Campos, Dominique Méry, Philippe Palanque
Pages	284-302
Number of pages	19
Volume	14010
DOIs	https://doi.org/10.1007/978-3-031-33163-3_22
Publication status	Published - May 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14010 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Fields of science

102 Computer Sciences

JKU Focus areas

Digital Transformation
Sustainable Development: Responsible Technologies and Management

Access to Document

10.1007/978-3-031-33163-3_22

Cite this

Geleßus, D., Stock, S., Vu, F., Leuschel, M., & Mashkoor, A. (2023). Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. In U. Glässer, J. Creissac Campos, D. Méry, & P. Palanque (Eds.), Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Proceedings (Vol. 14010, pp. 284-302). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14010 LNCS). https://doi.org/10.1007/978-3-031-33163-3_22

Geleßus, David ; Stock, Sebastian ; Vu, Fabian et al. / Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Proceedings. editor / Uwe Glässer ; Jose Creissac Campos ; Dominique Méry ; Philippe Palanque. Vol. 14010 2023. pp. 284-302 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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",

}

Geleßus, D, Stock, S, Vu, F, Leuschel, M & Mashkoor, A 2023, Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. in U Glässer, J Creissac Campos, D Méry & P Palanque (eds), Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Proceedings. vol. 14010, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14010 LNCS, pp. 284-302. https://doi.org/10.1007/978-3-031-33163-3_22

Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. / Geleßus, David; Stock, Sebastian; Vu, Fabian et al.
Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Proceedings. ed. / Uwe Glässer; Jose Creissac Campos; Dominique Méry; Philippe Palanque. Vol. 14010 2023. p. 284-302 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14010 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

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

AU - Geleßus, David

AU - Stock, Sebastian

AU - Vu, Fabian

AU - Leuschel, Michael

AU - Mashkoor, Atif

PY - 2023/5

Y1 - 2023/5

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85161169708

U2 - 10.1007/978-3-031-33163-3_22

DO - 10.1007/978-3-031-33163-3_22

M3 - Conference proceedings

SN - 978-3-031-33162-6

VL - 14010

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 284

EP - 302

BT - Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Proceedings

A2 - Glässer, Uwe

A2 - Creissac Campos, Jose

A2 - Méry, Dominique

A2 - Palanque, Philippe

ER -

Geleßus D, Stock S, Vu F, Leuschel M, Mashkoor A. Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. In Glässer U, Creissac Campos J, Méry D, Palanque P, editors, Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Proceedings. Vol. 14010. 2023. p. 284-302. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-33163-3_22

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

Abstract

Publication series

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this