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/).

翻译：我们提出AlloyInEcore工具，用于规范元模型及其静态语义，以支持对模型进行自动化形式化推理。软件开发项目要求软件系统通过多种模型（如需求模型、架构模型、测试模型及源代码）进行规范。对这些模型进行推理对于确保系统规格的正确性与完整性至关重要。AlloyInEcore允许用户指定元模型及其静态语义，并利用该语义自动检测不一致模型，同时补全部分模型。该工具已在汽车领域的三个工业案例研究中得到评估（https://modelwriter.github.io/AlloyInEcore/）。