机载软件安全性形式化验证方法研究

摘要

飞机作为一种工作在空中的交通工具，对安全性的要求极高，任何细微的差错都可能造成灾难性的后果，保障飞机的安全至关重要。现代飞机的各项功能都越来越依赖软件系统，然而现代机载软件功能繁多、结构复杂、构件众多，且影响因素多，设计阶段不能完全排除构件间相互影响尤其是软件安全性等级相互依赖而导致的整体安全下降的情况，为保证软件安全，开发人员需要在设计阶段就确保系统设计满足安全性要求。然而目前的方法不能完全满足安全性验证要求，因此亟需一种高效率地系统构件安全性验证方法以确保系统设计满足适航标准安全性要求。SysML语言被广泛用于系统工程建模，借助SysML语言可较好的描述机载软件架构及属性，但是SysML是半形式化的工具，缺乏精确语义的支持同时自身不具备验证的功能。Petri网是一种既有图形化特征也有精确语义的形式化工具，在形式化验证领域得到了广泛应用。通过适当的途径将SysML转化为Petri网模型，在此基础上可进一步验证软件的安全性，从而找出软件设计上的不足避免了后期返工及安全隐患，保证了系统的安全。
　　本文分析了机载软件安全标准，在此基础上定义了一种适于描述机载软件安全一致性验证的扩展Petri网，其次基于SysML块图建立带安全属性的系统静态结构模型，构建SysML到Petri网的转换规则可将SysML块图转化为Petri网从而进行精确的形式化建模。然后，利用可达树图分析了系统安全状况的所有传递路径和所有的安全状态组合，在此基础上给出了安全性验证算法方法，验证软件构件安全等级设计是否符合适航标准。最后通过具体事例说明了方法的可行性，同时通过对比分析了基于Petri的安全验证方法的优势。

目录

注释表

第一章 绪论

1.1研究背景

1.2国内外研究现状

1.3研究目的

1.4论文章节安排

第二章 DO-178C标准及软件形式化验证方法

2.1机载软件安全性保证标准

2.2软件验证理论与形式化方法

2.3Petri网理论

2.4本章小结

第三章 扩展有色Petri网模型

3.1有色Petri网

3.2适用于机载软件安全关系验证的扩展有色Petri网（SSCPN）

3.3本章小结

第四章 基于扩展有色Petri网的SysML块图建模及验证方法

4.1SysML介绍及基于SysML的机载软件建模

4.2SysML到扩展有色Petri网的形式化转换

4.3基于Petri网的验证框架及方法

4.4本章小结

第五章 基于扩展有色Petri网的实例验证分析

5.1转化为扩展有色Petri网模型

5.2不合要求软件的检测

5.3反向推算问题原因

5.4相关工作比较

第六章 总结展望

6.1本文总结

6.2未来展望

参考文献

致谢

在学期间研究成果