Why Are Modalities Good for Interface Theories?
Why Are Modalities Good for Interface Theories?
复制标题
为什么模态有利于界面理论？
DOI：
10.1109/acsd.2009.22
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Roberto Passerone
中科院分区：
文献类型：
--
作者：
Jean;Éric Badouel;A. Benveniste;B. Caillaud;Roberto Passerone
在本文中，我们重新审视界面理论的基础知识。方法论上的考虑要求支持“方面”和“假设/保证”推理。从这些考虑出发，我们表明，除了接口现在经典的细化和可替代性属性之外，还需要两个额外的操作，即：合取和残差（或商）。我们提请注意处理具有不同字母表的界面的困难——这需要字母表均衡。我们表明，对于不同的操作，必须以不同的方式执行字母均衡。然后，我们展示了根据 Kim Larsen 的原始提案改编的模态接口提供了所需的灵活性。
In this paper we revisit the fundamentals of interface theories. Methodological considerations call for supporting ``aspects'' and ``assume/guarantee'' reasoning. From these considerations, we show that, in addition to the now classical refinement and substitutability properties of interfaces, two additional operations are needed, namely: conjunction and residuation (or quotient). We draw the attention to the difficulty in handling interfaces having different alphabets --- which calls for alphabet equalization. We show that alphabet equalization must be performed differently for the different operations. Then, we show that Modal Interfaces, as adapted from the original proposal by Kim Larsen, offer the needed flexibility.