Event-B formalization of a variability-aware component model patterns framework

In the domain of model-driven engineering, patterns have emerged as a ubiquitous structuring mechanism. Patterns are used for instance at the requirement analysis level, during system design, and during the deployment and code generation phases. We focus on formalizing the operational semantics of pattern application on component-based system designs. More precisely, our ultimate goal is to provide a semantic framework to support the use of patterns for the production of correct-by-construction architectures, i.e., the structural (static) correctness of the architectures obtained through the formal application of patterns. To that end, we propose an Event-B framework for patterns specification, instantiation and application. This model is built incrementally through horizontal refinements which introduce components, ports, and connectors. Patterns with variability are defined, instantiated and can be applied to user models. We show that these operations preserve the structural properties of hierarchical component models. (C) 2020 Elsevier B.V. All rights reserved.