一种面向安全关键软件的程序证明方法研究

封面

声明

中文摘要

英文摘要

目录

图表清单

缩略词

第一章 绪论

1.1 课题研究背景

1.2 国内外研究现状及选题依据

1.3 论文的组织结构

第二章 面向Safety-C软件的安全性分析

2.1 安全关键软件程序分析

2.2 C语言安全子集（Safety-C）

2.3 面向Safety-C软件的安全性分析框架

2.4 本章小结

第三章 面向操作语义的Safety-C软件建模

3.1 操作表达式形式模型

3.2 Safety-C到操作表达式模型转换

3.3 操作表达式模型分析树的生成

3.4 本章小结

第四章 基于语义谓词的分析树安全性验证

4.1 分析树语义谓词计算

4.2 基于消解原理的分析树语义谓词约简

4.3 基于语义谓词的分析树安全性验证流程

4.4 本章小结

第五章 安全性分析原型工具设计与实现

5.1 安全性分析系统设计

5.2 襟缝翼控制系统实例分析

5.3 本章小结

第六章 总结与展望

6.1 论文总结

6.2 未来工作展望

参考文献

致谢

在学期间的研究成果及发表的学术论文