一句话：将一阶关系逻辑嵌入 MOF/Ecore，用静态语义自动检测不一致并补全模型。
本文提出 AlloyInEcore，一个面向元建模与模型推理的工具。软件开发中系统常由需求、架构、测试等多种模型刻画，因此需要对其一致性与完整性进行形式化推理。AlloyInEcore 将一阶关系逻辑嵌入 Meta-Object Facility（MOF/Ecore），使用户能在定义元模型的同时声明其静态语义；基于这些语义，工具可自动检测不一致模型并补全部分模型，从而支持自动化、形式化的模型推理。作者在汽车领域的三个工业案例研究上评估了该工具。
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/).
@inproceedings{paperbot4596,
title = {AlloyInEcore: embedding of first-order relational logic into meta-object facility for automated model reasoning},
author = {Ferhat Erata and Arda Goknil and Ivan Kurtev and Bedir Tekinerdogan},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3264588}
}