一种基于SMT和BP的多线程程序验证方法

发布时间：2024-07-07 05:12

　　多线程程序是计算机软件设计的核心,如何高效验证多线程程序的安全性问题已成为国内外研究人员的主要研究内容。现有研究表明:多线程程序的安全性问题可简化为良拟序迁移系统(Well-Quasi-Ordered Transition System,WQOTS)的可覆盖性问题。针对良拟序迁移系统的可覆盖性问题,已存在大量的解决方案,它们主要是以显示状态搜索思想设计的。多线程程序的状态空间随程序的规模和线程数目的增加呈指数级增长,导致这些算法都存在低效性或不完备性的问题。如何在验证过程中尽量避免状态空间搜索或降低状态空间的规模是提高多线程程序安全性验证效率的关键。本文主要的研究对象是被无穷个线程并发执行的有限状态布尔程序(Boolean Program,BP),可以通过对多线程程序进行谓词抽象得到。本文根据目前多线程程序验证方法的优势和不足,考虑到基于SMT求解器的符号分析方法能避免对状态空间搜索从而加快验证,以及直接使用布尔程序作为抽象模型能降低状态空间的规模,提出了一种新的多线程程序安全性验证方法。首先研究了基于SMT求解器的符号分析模块,详细分析了如何利用计数抽象从线程迁移系统中构造可覆盖性问...

【文章页数】：71 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
符号对照表
缩略语对照表
第一章 绪论
    1.1 研究背景和意义
    1.2 国内外研究进展
    1.3 研究内容及论文章节安排
        1.3.1 主要研究内容
        1.3.2 组织结构
第二章 相关基础理论
    2.1 模型检测
    2.2 抽象技术
        2.2.1 谓词抽象技术
        2.2.2 常见的谓词抽象工具
    2.3 布尔程序
        2.3.1 顺序布尔程序
        2.3.2 并发布尔程序和无限状态迁移系统
    2.4 良拟序迁移系统
        2.4.1 Petri网系统
        2.4.2 线程迁移系统
    2.5 可达性问题和可覆盖性问题的关联
    2.6 本章小结
第三章 基于SMT和BP的多线程程序的可覆盖性分析
    3.1 TTS上的基于SMT求解器的可覆盖性分析
        3.1.1 基于SMT求解器的符号分析模块思想
        3.1.2 局部状态约束
        3.1.3 共享状态约束
    3.2 基于BP的KM算法模块
        3.2.1 经典的基于TTS的KM算法分析
        3.2.2 布尔程序上的可覆盖性问题
        3.2.3 布尔程序上的KM算法
    3.3 基于SMT和BP的可覆盖性分析过程设计与实现
        3.3.1 工具的设计与实现
        3.3.2 使用改进的KM算法的可覆盖性分析
    3.4 本章小结
第四章 实验结果分析
    4.1 实验环境及测试集
    4.2 实验结果分析
    4.3 本章小结
第五章 总结与展望
    5.1 工作总结
    5.2 未来展望
参考文献
致谢
作者简介



本文编号：4003206