一句话：为 Event-B 规约语言建立基于 institution 的形式语义，证明其满足性保持与模型合并条件，并统一参数化与精化等模块化构造。
论文针对 Event-B 规约语言缺乏统一形式语义、模块化与精化构造语义基础不足的问题，运用 institution 理论为 Event-B 定义 institution EVT，并证明其满足满足性保持与模型合并等有效性条件。作者提出一组映射函数，将 Event-B 的语言构造对应到 EVT，据此清晰划分出超结构、基础设施与数学三个子语言。基于该语义，论文展示 institution 中通用的规约构建算子（包括参数化与精化）如何涵盖并增强 Event-B 已有模块化机制，并通过实例研究说明其用法。最后实现 EBtoEVT 解析器/翻译器，为 Event-B 规约接入支持异构规约的 Hets 工具链提供入口。
This paper describes a formal semantics for the Event-B specification language using the theory of institutions. We define an institution for Event-B, EVT, and prove that it meets the validity requirements for satisfaction preservation and model amalgamation. We also present a series of functions that show how the constructs of the Event-B specification language can be mapped into our institution. Our semantics sheds new light on the structure of the Event-B language, allowing us to clearly delineate three constituent sub-languages: the superstructure, infrastructure and mathematical languages. One of the principal goals of our semantics is to provide access to the generic modularisation constructs available in institutions, including specification-building operators for parameterisation and refinement. We demonstrate how these features subsume and enhance the corresponding features already present in Event-B through a detailed study of their use in a worked example. We have implemented our approach via a parser and translator for Event-B specifications, EBtoEVT, which also provides a gateway to the Hets toolkit for heterogeneous specification.
@article{paperbot1646,
title = {Building Specifications in the Event-B Institution},
author = {Marie Farrell and Rosemary Monahan and James F. Power},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 4},
year = {2022},
doi = {10.46298/lmcs-18(4:4)2022}
}