| 面向DO-333的襟缝翼控制单元安全性分析 |
| |
| 引用本文： | 陈光颖,黄志球,陈哲,阚双龙.面向DO-333的襟缝翼控制单元安全性分析[J].计算机科学,2016,43(5):150-156, 161. |
| |
| 作者姓名： | 陈光颖 黄志球 陈哲 阚双龙 |
| |
| 作者单位： | 南京航空航天大学计算机科学与技术学院 南京210016,南京航空航天大学计算机科学与技术学院 南京210016,南京航空航天大学计算机科学与技术学院 南京210016,南京航空航天大学计算机科学与技术学院 南京210016 |
| |
| 基金项目： | 本文受国家自然科学基金(61100034,3),中国博士后科学基金(20110491411),江苏省普通高校研究生科研创新计划资助 |
| |
| 摘 要： | DO-333是对机载软件安全性标准DO-178C关于形式化方法的补充,为机载软件开发过程中形式化方法的使用提供指导。模型检验作为一种形式化方法,可以应用于对软件需求和设计阶段制品的严格验证。基于DO-333,使用模型检验对飞控系统中襟缝翼控制单元不同阶段的软件制品进行验证与分析,判断其是否满足DO-178C的相关验证目标并提供证据支持。首先,对控制单元中襟翼与缝翼必须互斥更新的高级需求进行规约和验证；其次,对单个机翼控制逻辑的低级需求进行规约和验证。通过以上验证与分析,分别为标准中关于高级和低级需求的验证目标提供证据。文中展示了模型检验在一个机载软件认证中的应用实例,该工作将为机载软件的安全性保障和适航认证提供技术支持。
|
| 关 键 词： | 适航认证 形式化方法 模型检验 机载软件 SPIN |
| 收稿时间： | 2015/4/28 0:00:00 |
| 修稿时间： | 8/7/2015 12:00:00 AM |
Safety Analysis of Slat and Flap Control Unit for DO-333 |
| |
| CHEN Guang-ying,HUANG Zhi-qiu,CHEN Zhe and KAN Shuang-long.Safety Analysis of Slat and Flap Control Unit for DO-333[J].Computer Science,2016,43(5):150-156, 161. |
| |
| Authors: | CHEN Guang-ying HUANG Zhi-qiu CHEN Zhe and KAN Shuang-long |
| |
| Affiliation: | College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China,College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China,College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China and College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China |
| |
| Abstract: | |
| |
| Keywords: | Airworthiness certification Formal methods Model checking Aircraft software SPIN |
|
|
点击此处可从《计算机科学》下载全文 |
|
