DO-333标准形式化方法研究

• 全文链接
• 请求原文

作   者：

郝继锋;  叶宏;  任晓瑞; 

作者机构：

航空工业西安航空计算技术研究所; 

关键词：

机载软件;  DO-178C;  形式化分析;  安全关键系统;  DO-333;  形式化模型;  形式化方法; 

期刊名称：

航空计算技术

基金项目：

面向程序验证的自动定理证明理论、方法与工具研究

i s s n：

1671-654X

年卷期：

2020 年 01 期

页   码：

124-129

摘   要：

安全关键系统的基础软件由于其安全认证、提高软件可信性的需求,必须使用形式化方法。调研了嵌入式操作系统、编译器、网络、文件系统的形式化验证案例,在此基础之上引出机载软件形式化方法 DO-333标准;阐述了形式化模型、形式化分析概念,提炼出DO-333在DO-178C的基础上,针对典型的过程活动、过程目标、其他考虑方面的变化;总结了在工程中使用形式化方法的优点和缺点。