HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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

Ismail Mendil 1 Yamine Aït-Ameur 1 Neeraj Kumar Singh 1 Dominique Méry 2, 3 Philippe Palanque 4
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 IRIT-ICS - Interactive Critical Systems
IRIT - Institut de recherche en informatique de Toulouse
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.
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03487124
Contributor : Ismail Mendil Connect in order to contact the contributor
Submitted on : Friday, December 17, 2021 - 3:20:54 PM
Last modification on : Tuesday, April 26, 2022 - 3:40:50 AM
Long-term archiving on: : Friday, March 18, 2022 - 7:26:35 PM

File

Ismail_Mendil_SETTA21.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

50

Files downloads

0