基于流分析与归纳不变式结合的German协议验证

摘要

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