| 基于流分析与归纳不变式结合的German协议验证 |
| |
| 引用本文： | 张瑜,孙文辉. 基于流分析与归纳不变式结合的German协议验证[J]. 计算机系统应用, 2017, 26(10): 156-160 |
| |
| 作者姓名： | 张瑜 孙文辉 |
| |
| 作者单位： | 北京交通大学 计算机与信息技术学院, 北京 100044,北京交通大学 计算机与信息技术学院, 北京 100044 |
| |
| 基金项目： | 国家自然科学基金（61672503） |
| |
| 摘 要： | German缓存一致性协议是用于共享内存的并发多处理器系统中的缓存一致性协议，对German协议进行形式化验证一直是学术界和工业界的热点.我们生成German协议的流图，对流程图的各个步骤进行详细的描述，并提出了流分析与归纳不变式结合对协议验证的方法，通过辅助不变式与协议流图的对应关系，从而进一步分析和验证German协议的正确性.
|
| 关 键 词： | 缓存一致性协议 流分析 归纳不变式 形式化验证 |
| 收稿时间： | 2017-01-12 |
Verification of German Cache Coherence Protocol by Flow Analysis and Inductive Invariants |
| |
| ZHANG Yu and SUN Wen-Hui. Verification of German Cache Coherence Protocol by Flow Analysis and Inductive Invariants[J]. Computer Systems& Applications, 2017, 26(10): 156-160 |
| |
| Authors: | ZHANG Yu and SUN Wen-Hui |
| |
| Affiliation: | School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China and School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China |
| |
| Abstract: | German cache coherence protocol is used in parallel multi-processor systems, and the verification of German protocol has always been a hot spot in international industry and academia. We generate the flow chart of German protocol and describe each step of the flow chart. Besides, we present a method to verify the cache coherence protocol by flow analysis and inductive invariants in this paper. By searching for the relations between the invariants and the flow chart of German protocol, we can further analyze and verify the correctness of German protocol. |
| |
| Keywords: | cache coherence protocol flow analysis inductive invariants formal verification |
|
| 点击此处可从《计算机系统应用》浏览原始摘要信息 |
|
点击此处可从《计算机系统应用》下载全文 |
