Automated analysis of integrity constraints in multi-level models

Multi-level modelling is a technology for model-based development that enables the incremental refinement of models in successive meta-levels, which results in simpler and more intentional system descriptions in some scenarios. In this approach, integrity constraints can be placed at any meta-level, and need to indicate the meta-level below at which they should hold. This requires a careful design, as constraints defined at different meta-levels may interact in unexpected ways. Unfortunately, current techniques for the analysis of the satisfiability of constraints are designed for two meta-levels only. Hence, nowadays, the analysis of multi-level solutions is performed by hand, which is tedious and error-prone. In this paper, we define an automated procedure to check the satisfiability of integrity constraints in a multi-level setting, leveraging on "off-the-shelf' model finders. This procedure is supported by our multi-level modelling tool MATADEPTH, which has been extended to reason on the satisfiability of constraints in multi-level models, and to perform automated model completion.