Formal domain-driven system development in Event-B: Application to interactive critical systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Systems Architecture Année : 2023

Formal domain-driven system development in Event-B: Application to interactive critical systems

Résumé

The design of complex and/or critical systems requires handling the environment constraints in which these systems evolve. Formal methods allow system developers to design models of such systems. They provide constructs for modelling components and views of these systems. However, these formal methods do not include built-in constructs for modelling the environment, and more broadly, domain knowledge associated with system models. Although ontologies have demonstrated their efficiency in modelling domain-specific features, they are not available as built-in constructs in formal methods.This paper shows how formal ontologies can be used to model domain-specific knowledge, as well as how system models may refer to these ontologies through annotation. We rely on the Event-B refinement and proof state-based method, and the associated theories, to define a framework in which domain-specific knowledge ontologies are formalised as Event-B theories defining data types used to type Event-B system design models. Finally, this framework is deployed for the specific case of interactive critical systems. To illustrate the proposed approach, a case study of the Traffic Collision Avoidance System (TCAS) is developed.

Dates et versions

hal-03904803 , version 1 (17-12-2022)

Identifiants

Citer

Ismail Mendil, Yamine Aït-Ameur, Neeraj Kumar Singh, Guillaume Dupont, Dominique Méry, et al.. Formal domain-driven system development in Event-B: Application to interactive critical systems. Journal of Systems Architecture, 2023, 135, pp.102798. ⟨10.1016/j.sysarc.2022.102798⟩. ⟨hal-03904803⟩
121 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More