面向DO-333的襟缝翼控制单元安全性分析  

Safety Analysis of Slat and Flap Control Unit for DO-333

作　　者：陈光颖 黄志球[1] 陈哲[1] 阚双龙[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016

出　　处：《计算机科学》2016年第5期150-156,161,共8页Computer Science

基　　金：国家自然科学基金(61100034;61170043);中国博士后科学基金(20110491411);江苏省普通高校研究生科研创新计划资助项目;中央高校基本科研业务费专项资金(CXZZ11_0218)资助

摘　　要：DO-333是对机载软件安全性标准DO-178C关于形式化方法的补充,为机载软件开发过程中形式化方法的使用提供指导。模型检验作为一种形式化方法,可以应用于对软件需求和设计阶段制品的严格验证。基于DO-333,使用模型检验对飞控系统中襟缝翼控制单元不同阶段的软件制品进行验证与分析,判断其是否满足DO-178C的相关验证目标并提供证据支持。首先,对控制单元中襟翼与缝翼必须互斥更新的高级需求进行规约和验证;其次,对单个机翼控制逻辑的低级需求进行规约和验证。通过以上验证与分析,分别为标准中关于高级和低级需求的验证目标提供证据。文中展示了模型检验在一个机载软件认证中的应用实例,该工作将为机载软件的安全性保障和适航认证提供技术支持。DO-333 is the formal supplement to the aircraft software＇s safety standard DO-178C,which provides guidance for the use of formal methods in the development process of aircraft software.Model checking,as a kind of formal methods,can be applied for the strict verification of the software artifacts in the requirement and design phase.Based on DO-333,this paper used model checking to formally verify the software artifacts of different development phases for a slats and flaps control unit,one component of the flight control system,aiming to justify whether the software artifact satisfies the related objectives or not in DO-178C and provide the evidence support.Firstly,model checking is applied to the specification and verification of the high_level requirements for the mutual updating operation between flap and slat.Then,it is applied to the low_level requirements for the control logic in a single wing.Based on the verification and analysis above,evidence is provided for the verification objectives about high_level and low_level requirements in DO-178C.This paper illustrated an application example of model checking in an aircraft software＇s certification and could provide technical support for the safety assurance and airworthiness certification of aircraft software.

关 键 词：适航认证 形式化方法 模型检验 机载软件 SPIN 

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