模态接口自动机
计算机科学中的逻辑
2015-07-01 v2 形式语言与自动机理论
软件工程
摘要
De Alfaro 和 Henzinger 的接口自动机 (IA) 以及 Nyman 等人近期提出的结合 IA 与 Larsen 的模态转换系统 (MTS) 的 IOMTS，是指定系统组件接口的成熟框架。然而，IA 和 IOMTS 均未考虑实践中当一个组件需满足多个接口时所必需的合取运算，而 Larsen 的 MTS-合取不封闭，Bene\v{s} 等人关于析取 MTS 的合取则未处理内部转换。此外，IOMTS 的并行组合表现出组合性缺陷。本文定义了 IA 和析取 MTS 上的合取（以及析取）运算，并证明这些算子是“正确”的，即相对于 IA 和 MTS 精化的最大下界（最小上界）。作为主要贡献，本文引入了一种新的接口理论，称为模态接口自动机 (MIA)：MIA 是 IOMTS 的一个丰富子集，具有显式的输出必须转换，而输入转换总是隐式允许；配备了组合性的并行、合取和析取算子；并且比 Nyman 的方法允许更简单的 IA 嵌入。因此，它修复了相关工作的不足，同时不像 Raclet 等人的模态接口理论那样将设计者限制于确定性接口。
引用
@article{arxiv.1306.3050,
title = {Modal Interface Automata},
author = {Gerald Lüttgen and Walter Vogler},
journal= {arXiv preprint arXiv:1306.3050},
year = {2015}
}
备注
28 pages