AlloyInEcore: Embedding of First-Order Relational Logic into Meta-Object Facility for Automated Model Reasoning

TL;DR

AlloyInEcore addresses the need for automated reasoning over MOF/Ecore conforming models by embedding static semantics in $FOL$ within Ecore and translating to KodKod for SAT-based analysis. The approach supports two core tasks—model consistency checking and partial-model completion—via a unified reasoning engine, enabling automatic inference of missing elements while explaining unsatisfiable parts. Evaluation on three automotive ECAS case studies demonstrates practical usefulness and correctness, with reasonable running times and clear benefits for heterogeneous model environments. The Eclipse-based tool, implemented in Java and backed by KodKod, is publicly available, facilitating adoption in industrial Model-Driven Engineering workflows.

Abstract

We present AlloyInEcore, a tool for specifying metamodels with their static semantics to facilitate automated, formal reasoning on models. Software development projects require that software systems be specified in various models (e.g., requirements models, architecture models, test models, and source code). It is crucial to reason about those models to ensure the correct and complete system specifications. AlloyInEcore allows the user to specify metamodels with their static semantics, while, using the semantics, it automatically detects inconsistent models, and completes partial models. It has been evaluated on three industrial case studies in the automotive domain (https://modelwriter.github.io/AlloyInEcore/).

Figures (5)

• Figure 1: Tool Overview
• Figure 2: The Metamodel for the Theory of Lists
• Figure 3: Example Metamodel Semantics in AlloyInEcore
• Figure 4: Example Inconsistent Model of the Theory of Lists
• Figure 5: Example Completed Model of the Theory of Lists