本文已被：浏览 1535次 下载 2168次
Received:March 10, 2015 Revised:April 17, 2015
Received:March 10, 2015 Revised:April 17, 2015
中文摘要: 提出了一种通过查找缓存一致性协议不变量来验证带参协议正确性的新方法.缓存一致性协议验证的难点在于必须证明协议对于任意大小的带参系统都成立.我们通过寻找不变量和协议规则之间的对应关系来计算辅助不变量,从而帮助推导验证缓存一致性协议.我们设计实现了一个不变量查找工具并将该工具应用到German协议上计算它们的辅助不变量并成功地验证了协议的安全性质.
Abstract:We present a new method for computing invariants for cache coherence protocol in this paper. The verification of cache coherence protocols is always a challenge as we have to check the safety properties of cache coherence protocol with arbitrary nodes. By searching the relations between the invariants and the rules of cache coherence protocol, we can verify the cache coherence protocol with circular reasoning. Besides, we implement a tool to help us computing invariants for cache coherence protocol. We also have experiments on how to apply our method to the German protocol with both control property and data property.
文章编号： 中图分类号： 文献标志码：
基金项目:
引用文本：
曹燊,李勇坚.基于不变量查找的German协议验证.计算机系统应用,2015,24(11):173-178
CAO Shen,LI Yong-Jian.Verification of German Cache Coherence Protocol by Searching Invariants.COMPUTER SYSTEMS APPLICATIONS,2015,24(11):173-178
曹燊,李勇坚.基于不变量查找的German协议验证.计算机系统应用,2015,24(11):173-178
CAO Shen,LI Yong-Jian.Verification of German Cache Coherence Protocol by Searching Invariants.COMPUTER SYSTEMS APPLICATIONS,2015,24(11):173-178
