带参协议形式化验证的研究

发布时间：2023-01-09 11:32

　　随着计算机技术、网络技术以及电子信息技术在各行各业的日益发展,多处理器体系以及多核架构在计算机系统结构中应用得越来越频繁,其正确性、可靠性等问题也越来越突出。带参协议在计算机系统多处理器体系的核心结构中广泛存在,面对日趋复杂的设计,带参协议正确性的验证越来越成为设计流程中的关键,细微的错误可能引发严重的后果。因此,带参协议设计正确性的验证问题成为了学术界和工业界研究的热点和重点。形式化验证方法通过符号描述带参协议的系统行为及其性质,基于各种数学逻辑推理算法进行验证,验证覆盖率高,且具有完备性,目前已经成为带参协议验证的重要方法。在带参协议形式化验证领域,虽然己经存在多种形式化验证方法,但是每种方法都存在一定的缺点,例如定理证明技术的自动化程度不高,需要人为主动干预,模型检测技术在带参协议规模较大的情况下会出现状态空间爆炸的问题,这些都成为了限制带参协议形式化验证有效性的重要因素。本论文对现有的带参协议的形式化验证方法进行了分类整理和深入分析,主要从提高定理证明技术的自动化程度和缓解模型检测技术状态空间的爆炸现象两个角度入手,提出了两种验证方法,并且在MESI、MutualEx、GERM... 

【文章页数】：63 页

【学位级别】：硕士

【文章目录】：
致谢
摘要
ABSTRACT
1 引言
    1.1 研究背景与意义
    1.2 国内外研究现状
    1.3 论文主要研究内容
    1.4 论文组织结构
2 带参协议验证相关理论
    2.1 带参协议简介
    2.2 带参协议形式化验证
    2.3 带参协议模型
        2.3.1 Murphi模型组成
        2.3.2 Murphi验证过程
    2.4 本章小结
3 基于归纳不变式与流分析结合的验证方法
    3.1 相关定义
    3.2 方法的详细设计
        3.2.1 整体框架
        3.2.2 因果关系判定算法
        3.2.3 归纳不变式查找算法
        3.2.4 流分析
    3.3 实验结果
        3.3.1 典型带参协议简介
        3.3.2 实验结果展示
        3.3.3 GERMAN协议实验结果分析
    3.4 本章小结
4 基于CVC4的谓词抽象的验证方法
    4.1 相关定义
    4.2 方法的详细设计
        4.2.1 整体框架
        4.2.2 抽象状态查找算法
    4.3 实验结果
    4.4 本章小结
5 结论
    5.1 论文总结
    5.2 论文展望
参考文献
作者简历及攻读硕士学位期间取得的研究成果
学位论文数据集


【参考文献】：
期刊论文
[1]一种基于广播的cache一致性协议的设计和验证[J]. 李俊,袁爱东,高剑刚.  计算机科学与探索. 2008(05)
[2]CMP中Cache一致性协议的验证[J]. 李崇民,王海,李兆麟.  电子技术应用. 2005(12)



本文编号：3729111