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

• 作者: 阚双龙 陈光颖 陈哲 黄志球
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 适航认证 形式化方法 模型检验 机载软件 SPIN
• 年，卷（期）: 2016,（5）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 150-156,161
• 页数: 8页
• 分类号: TP311
• 字数: 9446字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2016.5.028

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄志球	南京航空航天大学计算机科学与技术学院	183	1755	20.0	33.0
2	陈哲	南京航空航天大学计算机科学与技术学院	25	189	7.0	13.0
3	阚双龙	南京航空航天大学计算机科学与技术学院	15	132	5.0	11.0
4	陈光颖	南京航空航天大学计算机科学与技术学院	4	21	3.0	4.0