Verification of German Cache Coherence Protocol by Searching Invariants
DOI:
CSTR:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

曹燊,李勇坚.基于不变量查找的German协议验证.计算机系统应用,2015,24(11):173-178

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 10,2015
  • Revised:April 17,2015
  • Adopted:
  • Online: December 03,2015
  • Published:
Article QR Code
You are the firstVisitors
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