模态接口自动机
Modal Interface Automata
摘要：
De Alfaro和Henzinger的接口自动机（IA）和Nyman等人。最近的IOMTS的IA和拉森的模态转换系统（MTS）的组合建立的框架，指定系统组件的接口。然而，IA和IOMTS都没有考虑在实际中当一个组件需要满足多个接口时所需要的合取，而Larsen的MTS合取不是封闭的，Beneidor等。的合取在析取MTS不处理内部转换。此外，IOMTS平行组合物表现出组合性缺陷。本文定义了IA和析取MTS上的合取（以及析取），并证明了运算符是“正确的”，即，最大下界（最小上界）wrt。IA-和resp. MTS细化。作为其主要贡献，一种新的接口理论称为模态接口自动机（MIA）的介绍：MIA是一个丰富的子集IOMTS具有明确的输出必须转换，而输入转换总是允许隐式，配备了合成并行，合取和析取算子，并允许一个简单的嵌入IA比尼曼的。因此，它修复了相关工作的缺点，而不像Raclet等人那样将设计师限制在确定性接口上。的模态界面理论。
英文摘要：
De Alfaro and Henzinger's Interface Automata (IA) and Nyman et al.'s recent combination IOMTS of IA and Larsen's Modal Transition Systems (MTS) are established frameworks for specifying interfaces of system components. However, neither IA nor IOMTS consider conjunction that is needed in practice when a component shall satisfy multiple interfaces, while Larsen's MTS-conjunction is not closed and Beneš et al.'s conjunction on disjunctive MTS does not treat internal transitions. In addition, IOMTS-parallel composition exhibits a compositionality defect. This article defines conjunction (and also disjunction) on IA and disjunctive MTS and proves the operators to be 'correct', i.e., the greatest lower bounds (least upper bounds) wrt. IA- and resp. MTS-refinement. As its main contribution, a novel interface theory called Modal Interface Automata (MIA) is introduced: MIA is a rich subset of IOMTS featuring explicit output-must-transitions while input-transitions are always allowed implicitly, is equipped with compositional parallel, conjunction and disjunction operators, and allows a simpler embedding of IA than Nyman's. Thus, it fixes the shortcomings of related work, without restricting designers to deterministic interfaces as Raclet et al.'s modal interface theory does.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
