程序验证的并行化方法研究与实现

目录

第一个书签之前

摘要

ABSTRACT

插图索引

表格索引

缩略语对照表

第一章 绪论

1.1 研究背景和意义

1.2 国内外研究现状

1.2.1 基于抽象解释理论的验证技术

1.2.2 基于谓词抽象的验证技术

1.2.3 基于动态执行的运行时验证技术

1.3 论文研究内容和组织结构

第二章 相关理论和技术

2.1 建模仿真验证语言MSVL

2.1.1 MSVL语法

2.1.2 MSVL语义

2.2 命题投影时序逻辑PPTL

2.2.1 PPTL语法

2.2.2 PPTL语义

2.2.3 有效性和可满足性

2.3 运行时验证

2.3.1 验证原理

2.3.2 运行时验证与模型检测

第三章 UMC4MSVL验证器的研究

3.1 UMC4MSVL验证器

3.2 验证原理和验证过程

3.2.1 验证原理

3.2.2 验证过程

3.3 选择语句的处理

3.4 可执行文件的生成

3.4.1 编译过程

3.4.2 语法树节点类型和结构

3.5 部分模块细节

3.5.1 执行入口函数

3.5.2 性质线程执行体

3.5.3 程序线程执行体

3.6 本章小结

第四章 基于UMC4MSVL的并行化验证设计与实现

4.1 并行化验证设计框架

4.2 多线程模块

4.2.1 多线程工作流程

4.2.2 线程池实现

4.2.3 线程池任务

4.3 语法树处理模块

4.3.1 全局变量定义

4.3.2 全局变量使用

4.3.3 算法调用规则

4.3.4 副本号的确定和映射

4.3.5 验证性质的等价转换

4.4 选择语句处理模块

4.5 并行性语句处理模块

4.6 反例输出模块

4.7 本章小结

第五章 实验与分析

5.1 验证工具使用说明

5.2 并行化验证效率测试

5.3 反例路径输出测试

5.4 本章小结

第六章 总结与展望

6.1 总结

6.2 展望

参考文献

致谢

附录A 测试代码

作者简介

1. 基本情况

2. 教育背景