论文部分内容阅读
DO-333是对机载软件安全性标准DO-178C关于形式化方法的补充,为机载软件开发过程中形式化方法的使用提供指导。模型检验作为一种形式化方法,可以应用于对软件需求和设计阶段制品的严格验证。基于DO-333,使用模型检验对飞控系统中襟缝翼控制单元不同阶段的软件制品进行验证与分析,判断其是否满足DO-178C的相关验证目标并提供证据支持。首先,对控制单元中襟翼与缝翼必须互斥更新的高级需求进行规约和验证;其次,对单个机翼控制逻辑的低级需求进行规约和验证。通过以上验证与分析,分别为标准中关于高级和低级需求