AIPUB归智期刊联盟

WeChat

Mobile website

2025-4-3- 6
Home > Archive>Volume 26, Issue 10, 2017 >156-160. DOI:10.15888/j.cnki.csa.006020
PDF HTML XML Export Cite reminder
Verification of German Cache Coherence Protocol by Flow Analysis and Inductive Invariants
CSTR:
[cstr]
Author:
  • Article
    • | |
  • Metrics
    • |
  • Reference [10]
    • |
  • Related [20]
    • | | |
  • Comments
    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.

    Reference
    [1] Clarke EM, Grumberg O, Peled DA. Model Checking. Cambridge: The MIT Press, 1999.
    [2] Nipkow T, Paulson LC, Wenzel M. Isabelle/HOL: A proof assistant for higher-order logic. Berlin Heidelberg: Springer, 2002.
    [3] Lv Y, Lin HM, Pan H. Computing invariants for parameter abstraction. Proc. of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign. Nice, France. 2007. 29-38.
    [4] Baukus K, Lakhnech Y, Stahl K. Parameterized verification of a cache coherence protocol: Safety and liveness. Proc. of the 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation. Venice, Italy. 2002. 317-330.
    [5] Bingham J, Hu AJ. Empirically efficient verification for a class of infinite-state systems. Proc. of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin Heidelberg, Germany. 2005. 77-92.
    [6] 曹燊, 李勇坚. 基于不变量查找的German协议验证. 计算机系统应用, 2015, 24(11): 173-178.[DOI:10.3969/j.issn.1003-3254.2015.11.028]
    [7] German SM. Tutorial on verification of distributed cache memory protocols. Formal Methods in Computer-Aided Design. 2004. 1-77.
    [8] Dill DL. The Murphi verification system. Proc. of the 8th International Conference on Computer Aided Verification. Berlin Heidelberg, Germany. 1996. 390-393.
    [9] 周琰. Godson-T缓存一致性协议的Murphi建模和验证. 计算机系统应用, 2013, 22(10): 124-128.[DOI:10.3969/j.issn.1003-3254.2013.10.024]
    [10] All auxiliary invariants of German protocol. https://github.com/zy311/German/blob/master/invariants.[2017].
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:1387
  • PDF: 1832
  • HTML: 0
  • Cited by: 0
History
  • Received:January 12,2017
  • Online: October 31,2017
Article QR Code
Links:Journal of Software中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会
You are the first990356Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-3
Address：4# South Fourth Street, Zhongguancun,Haidian, Beijing,Postal Code：100190
Phone：010-62661041 Fax： Email：csa (a) iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063