基于流分析与归纳不变式结合的German协议验证
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金(61672503)


Verification of German Cache Coherence Protocol by Flow Analysis and Inductive Invariants
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    German缓存一致性协议是用于共享内存的并发多处理器系统中的缓存一致性协议,对German协议进行形式化验证一直是学术界和工业界的热点.我们生成German协议的流图,对流程图的各个步骤进行详细的描述,并提出了流分析与归纳不变式结合对协议验证的方法,通过辅助不变式与协议流图的对应关系,从而进一步分析和验证German协议的正确性.

    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.

    参考文献
    相似文献
    引证文献
引用本文

张瑜,孙文辉.基于流分析与归纳不变式结合的German协议验证.计算机系统应用,2017,26(10):156-160

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2017-01-12
  • 最后修改日期:
  • 录用日期:
  • 在线发布日期: 2017-10-31
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号