Towards behavioral consistency in heterogeneous modeling scenarios

TL;DR

This work tackles the challenge of achieving semantic consistency across heterogeneous behavioral models in Model-driven Engineering. It proposes a four-step methodology: align behavioral metamodels (coordinations) and model-level interactions (interactions), transform models into a graph-grammar semantic domain, and verify global consistency using model checking by constructing a Kripke structure. Key contributions include metamodel alignments for common behavioral formalisms, a graph-grammar based semantic domain, and a prototype tool for automated transformation and verification. The approach enables heterogeneous behavioral modeling while providing rigorous consistency checks that can reveal deadlocks and safety violations in integrated multi-model scenarios, benefiting multi-view MDE workflows.

Abstract

Behavioral models play an essential role in Model-driven engineering (MDE). Keeping inter-related behavioral models consistent is critical to use them successfully in MDE. However, consistency checking for behavioral models, especially in a heterogeneous scenario, is limited. We propose a methodology to integrate heterogeneous behavioral models to achieve consistency checking in broader scenarios. It is based on aligning the respective behavioral metamodels by defining possible inter-model relations which carry behavioral meaning. Converting the models and their relations to a behavioral formalism enables analysis of global behavioral consistency using model-checking.

Figures (6)

• Figure 1: Behavioral Consistency Management Process
• Figure 2: Example models $SM^1$, $SM^2$, $SM^3$, $N^1$, and their interactions
• Figure 3: Finite state machine metamodel $M^1$
• Figure 4: Petri net metamodel $M^2$
• Figure 5: Alignment of the metamodels $M^1$ and $M^2$

Theorems & Definitions (4)

• Definition 1: Finite state machine
• Definition 2: Petri net
• Definition 3: Graph grammar
• Definition 4: Production rule