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

Research on Formal Methods of DO-333 Supplement

作　　者：郝继锋[1] 叶宏[1] 任晓瑞[1] HAO Ji-feng;YE Hong;REN Xiao-rui(Xi'an Aeronautics Computing Technique Research Institute,AVIC,Xi'an 710068,China)

机构地区：[1]航空工业西安航空计算技术研究所,陕西西安710068

出　　处：《航空计算技术》2020年第1期124-129,共6页Aeronautical Computing Technique

基　　金：国家自然科学基金项目资助(61732001)。

摘　　要：安全关键系统的基础软件由于其安全认证、提高软件可信性的需求,必须使用形式化方法。调研了嵌入式操作系统、编译器、网络、文件系统的形式化验证案例,在此基础之上引出机载软件形式化方法DO-333标准;阐述了形式化模型、形式化分析概念,提炼出DO-333在DO-178C的基础上,针对典型的过程活动、过程目标、其他考虑方面的变化;总结了在工程中使用形式化方法的优点和缺点。The safety critical systems software must use formal methods based on the safety certification and boost the trust of software.Firstly,the paper investigates the formalization verification cases of embedded operating system,compiler,network and file system,then the DO-333 avionics software supplement of formal methods is introduced.Secondly,we clarify the concept of formal models and formal analysis;process activity,process objective,additional considerations of DO-333 are explained based on DO-178C.Finally,the pros and cons of formal methods using in engineering are summarized.

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]