机载软件建模及其形式化验证方法研究

目录

声明

第一章 绪 论

1.1 研究背景与意义

1.2 国内外研究现状

1.2.1 基于模型的机载软件开发研究现状

1.2.2 形式化验证研究现状

1.3 研究内容

1.4 论文组织结构

第二章 相关理论与方案设计

2.1 引言

2.2 基于模型的软件开发方法

2.3 机载代码与形式化验证

2.3.1 机载代码的特点

2.3.2 形式化验证基本方法对比分析

2.4 基于演绎验证的定理证明

2.4.1 一阶谓词逻辑

2.4.2 Hoare逻辑公理

2.4.3 最弱前置谓词演算

2.4.4 基于演绎验证的定理证明

2.5 验证工具选择与方案设计

2.5.1 验证工具选择

2.5.2 机载代码形式化验证方案设计

2.6 本章小结

第三章 机载代码的形式化验证关键技术研究

3.1 引言

3.2 ACSL形式化规约语言

3.3 机载代码Hoare逻辑规约构建及验证条件提取

3.3.1 顺序结构的规约构建

3.3.2 选择结构的规约构建

3.3.3 循环结构的规约构建

3.3.4 验证条件提取

3.4 基于自主证明的规约构建改进研究

3.4.1 基于自主证明的规约补充方法

3.4.2 改进实验及自动化程度对比

3.5 针对机载代码的安全规约研究

3.5.1 算术溢出

3.5.2 数组越界

3.5.3 空指针引用

3.6 本章小结

第四章 飞控机载软件建模

4.1 引言

4.2 飞控控制律的设计与实现

4.2.1 纵向控制律模块设计与实现

4.2.2 横侧向控制律模块设计与实现

4.3 飞控机载应用软件的设计与实现

4.3.1 姿态解算模块设计与实现

4.3.2 传感器监控模块的设计与实现

4.3.3 导航与大气信号表决模块的设计与实现

4.3.4 交联系统的设计与实现

4.3.5 任务管理模块的设计与实现

4.3.6 遥控遥测模块的设计与实现

4.4 本章小结

第五章 机载软件安全关键模块形式化验证

5.1 引言

5.2 前轮转向电路管理模块形式化验证

5.2.1 Hoare逻辑规约的构建

5.2.2 验证条件证明

5.3 传感器监控模块形式化验证

5.3.1 Hoare逻辑规约的构建

5.3.2 验证条件证明

5.4 姿态解算模块形式化验证

5.4.1 Hoare逻辑规约的构建

5.4.2 验证条件证明

5.5 虚拟飞控仿真实验

5.5.1 虚拟飞控仿真平台

5.5.2 仿真方法与结果分析

5.6 本章小结

第六章 总结与展望

6.1 工作总结

6.2 未来展望

致谢

参考文献