Leveraging Event-B Theories for Handling Domain Knowledge in Design Models - Archive ouverte HAL Access content directly
Conference Papers Year : 2021

Leveraging Event-B Theories for Handling Domain Knowledge in Design Models

(1) , (1) , (1) , (2, 3) , (4)
1
2
3
4

Abstract

Formal system modelling languages lack explicit constructs to model domain knowledge, hindering clear separation of this knowledge from system design models. Indeed, in many cases, this knowledge is hardcoded in the system formal specification or is simply overlooked. Providing explicit domain knowledge constructs and properties would yield a significant improvement in the robustness and confidence of the system design models. Therefore, it speeds up formal verification of safety properties and advances system certification since certification standards and requirements rely on domain knowledge models. The purpose of this paper is to show how formal system design models can benefit from explicit handling of domain knowledge, represented as ontologies. To this end, state-based Event-B modelling language and theories are used to model system models and domain knowledge ontologies, respectively. Our proposition is exemplified by the TCAS (Traffic Collision Avoidance System) system, a critical airborne avionic component. Finally, we provide an assessment highlighting the overall approach.
Fichier principal
Vignette du fichier
Ismail_Mendil_SETTA21.pdf (806.7 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03487124 , version 1 (17-12-2021)

Identifiers

Cite

Ismail Mendil, Yamine Aït-Ameur, Neeraj Kumar Singh, Dominique Méry, Philippe Palanque. Leveraging Event-B Theories for Handling Domain Knowledge in Design Models. 7th International Symposium on Dependable Software Engineering. Theories, Tools, and Applications (SETTA 2021), Nov 2021, Beijing/Online, China. pp.40-58, ⟨10.1007/978-3-030-91265-9_3⟩. ⟨hal-03487124⟩
104 View
22 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More