| 基于不变量查找的German协议验证 |
| |
| 引用本文： | 曹燊,李勇坚.基于不变量查找的German协议验证[J].计算机系统应用,2015,24(11):173-178. |
| |
| 作者姓名： | 曹燊 李勇坚 |
| |
| 作者单位： | 中国科学院软件研究所计算机科学国家重点实验室, 北京 100190;中国科学院大学, 北京 100190,中国科学院软件研究所计算机科学国家重点实验室, 北京 100190 |
| |
| 摘 要： | 提出了一种通过查找缓存一致性协议不变量来验证带参协议正确性的新方法.缓存一致性协议验证的难点在于必须证明协议对于任意大小的带参系统都成立.我们通过寻找不变量和协议规则之间的对应关系来计算辅助不变量,从而帮助推导验证缓存一致性协议.我们设计实现了一个不变量查找工具并将该工具应用到German协议上计算它们的辅助不变量并成功地验证了协议的安全性质.
|
| 关 键 词： | 缓存一致性协议 带参系统 不变量查找 多核处理器 |
| 收稿时间： | 2015/3/10 0:00:00 |
| 修稿时间： | 2015/4/17 0:00:00 |
Verification of German Cache Coherence Protocol by Searching Invariants |
| |
| CAO Shen and LI Yong-Jian.Verification of German Cache Coherence Protocol by Searching Invariants[J].Computer Systems& Applications,2015,24(11):173-178. |
| |
| Authors: | CAO Shen and LI Yong-Jian |
| |
| Affiliation: | Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;University of Chinese Academy of Sciences, Beijing 100190, China and Institute of Software, Chinese Academy of Sciences, Beijing 100190, China |
| |
| 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. |
| |
| Keywords: | cache coherence protocol parameterized system invariant computing multi-processor |
|
| 点击此处可从《计算机系统应用》浏览原始摘要信息 |
|
点击此处可从《计算机系统应用》下载全文 |
|
