Event-B Formalization of a Variability-Aware Component Model Patterns Framework

Jean-Paul Bodeveix (1, 2) , Arnaud Dieumegard (3, 4) , M Filali (1, 5)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 UT3 - Université Toulouse III - Paul Sabatier
3 IRT Saint Exupéry - Institut de Recherche Technologique
4 DTIS, ONERA, Université de Toulouse [Toulouse]
5 CNRS - Centre National de la Recherche Scientifique

In the domain of model driven engineering, patterns have emerged as an ubiquitous structuring mechanism. Actually, patterns are used for instance at the requirement analysis level, during system design, and during the deployment and code generation phases. In this paper, we are interested in making precise the use of such a notion during system design. More precisely, our ultimate goal is to provide a semantic framework to support correct by construction architectures, i.e., the structural correctness of the architectures obtained through the application of patterns. For this purpose, we propose an Event-B modeling scheme for hierarchical component models. This model is built incrementally through horizontal refinements which introduce components, ports and lastly connectors. Patterns with variability are defined, instantiated and applied to user models. We show that these operations preserve the structural properties of the component model.

Mots clés: Design patterns; Critical systems; Variability; System engineering; Formal refinement

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

Jean-Paul Bodeveix, Arnaud Dieumegard, M Filali. Event-B Formalization of a Variability-Aware Component Model Patterns Framework. 15th International Conference on Formal Aspects of Component Software (FACS 2018), Oct 2018, Pohang, South Korea. pp.54-74, ⟨10.1007/978-3-030-02146-7_3⟩. ⟨hal-02181895⟩