Completeness of fair ASM refinement
Completeness of fair ASM refinement
复制标题
公平 ASM 细化的完整性
DOI：
10.1016/j.scico.2009.10.004
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
G. Schellhorn
中科院分区：
文献类型：
--
作者：
G. Schellhorn
ASM的改进验证使用广义正向模拟，使我们能够细化m个抽象的操作到n个具体的操作与任意的m和n。与数据细化的一个主要区别是，ASM细化考虑了无限次运行和终止。由于反向模拟一般不保留终止性，因此将历史信息添加到具体级别的标准技术不适用于获得完整性证明。幂集构造也增加了无限游程，因此也不适用。本文表明，一个完整性的证明仍然是可能的，通过添加无限的预言信息，有效地移动非决定论的初始状态。添加这样的预言信息不仅可以在语义层面上完成，还可以通过一个简单的句法转换来删除ASM的选择结构。完全性证明也被转化为IO自动机的完全性证明。最后，证明扩展到处理补充谓词，指定公平性和活性假设，通过转移相关的结果Wim Hesselink的细化，使用阿巴迪-Lamport设置。
ASM refinements are verified using generalized forward simulations which allow us to refine m abstract operations to n concrete operations with arbitrary m and n. One main difference from data refinement is that ASM refinement considers infinite runs and termination. Since backward simulation does not preserve termination in general, the standard technique of adding history information to the concrete level is not applicable to get a completeness proof. The power set construction also adds infinite runs and is therefore not applicable either. This paper shows that a completeness proof is nevertheless possible by adding infinite prophecy information, effectively moving nondeterminism to the initial state. Adding such prophecy information can be done not only on the semantic level, but also by a simple syntactic transformation that removes the choose construct of ASMs. The completeness proof is also translated to a completeness proof for IO automata. Finally, the proof is extended to deal with supplementary predicates, that specify fairness and liveness assumptions, by transferring a related result of Wim Hesselink for refinements that use the Abadi–Lamport setting.