面向适航认证的模型驱动机载软件构件的安全性验证

doi:CNKI:11-1929/V.20120201.0941.002

流体力学与飞行力学

本期目录 | 过刊浏览 | 高级检索

前一篇 | 后一篇

面向适航认证的模型驱动机载软件构件的安全性验证

徐丙凤¹, 黄志球¹, 胡军^1,3, 于笑丰^2,3

1. 南京航空航天大学计算机科学与技术学院, 江苏南京 210016;
2. 南京大学商学院, 江苏南京 210093;
3. 南京大学计算机软件新技术国家重点实验室, 江苏南京 210093

收稿日期:2011-08-10 修回日期:2011-10-26 出版日期:2012-05-25 发布日期:2012-05-24
通讯作者: 黄志球,Tel.: 025-84896490 E-mail: zqhuang@nuaa.edu.cn E-mail:zqhuang@nuaa.edu.cn
基金资助:
江苏省研究生培养创新工程(CXZZ11_0218);国家自然科学基金(61100034,61170043);江苏省博士后科研资助计划项目(1101092C);中国博士后科学基金(20110491411);南京航空航天大学科技创新基金(NS2010095)

Model-driven Safety Dependence Verification for Component-based Airborne Software Supporting Airworthiness Certification

XU Bingfeng¹, HUANG Zhiqiu¹, HU Jun^1,3, YU Xiaofeng^2,3

1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China;
2. School of Business, Nanjing University, Nanjing 210093, China;
3. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China

Received:2011-08-10 Revised:2011-10-26 Online:2012-05-25 Published:2012-05-24
Supported by:
Funding of Jiangsu Innovation Program for Graduate Education (CXZZ11_0218); National Natural Science Foundation of China (61100034, 61170043); Jiangsu Planned Projects for Postdoctoral Research Funds (1101092C); China Postdoctoral Science Foundation (20110491411); Technology Innoviation Funding of Nanjing Univesity of Aeronautics and Astronautics (NS2010095)

摘要/Abstract

摘要： 在软件开发的过程中为适航认证提供证据,已成为机载软件开发的研究热点。现代复杂机载软件多为构件化分布式架构,如何有效验证构件之间安全性依赖关系与适航认证标准当中规定目标的一致性,是机载软件设计阶段的一个重要问题。首先,使用系统建模语言(SysML)块图建立带有安全性特征的系统静态结构模型,将其转换为块依赖图以便进行精确的形式化描述。在此基础上给出形式验证方法,检验系统静态结构模型中的安全性依赖关系与适航认证标准中所规定目标之间是否一致。最后,通过一个飞机导航系统的例子说明如何将该方法应用于机载软件开发的过程中。利用这种方法对系统静态结构模型的安全性依赖关系进行验证,能够提高系统整体的安全性,并为适航认证提供证据。

关键词: 适航认证, 安全性验证, 机载软件, 模型驱动, 形式化方法, SysML

Abstract: Current research of airborne software focuses on providing airworthiness certification evidence in software develop-ment process. As modern complex airborne software architecture is component-based and distributed, this paper considers the issue of checking the safety dependence relationship of software components against objectives that the airworthiness certification standard stipulates, which is one of the key problems of airborne software development in the design phase. Firstly, the static structure of a system is specified by a systems modeling language (SysML) block definition diagram with the description of safety properties. Secondly, the SysML block definition diagram is transformed to a block dependence graph for precise formal description. Thirdly, a method for checking the consistency between the safety dependence relationship in the static system structure and objectives of the airworthiness certification standard is proposed. Finally, an example of an aircraft navigation system is provided to illustrate how to use the method in the airborne software development process. The integrated safety level of a system is promoted by applying this method, and it can be used to provide airworthiness certification evidence.

Key words: airworthiness certification, safety verification, airborne software, model-driven, formal method, SysML

中图分类号:

V328
TP311

徐丙凤, 黄志球, 胡军, 于笑丰. 面向适航认证的模型驱动机载软件构件的安全性验证 [J]. 航空学报, 2012, (5): 796-808.

XU Bingfeng, HUANG Zhiqiu, HU Jun, YU Xiaofeng. Model-driven Safety Dependence Verification for Component-based Airborne Software Supporting Airworthiness Certification[J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2012, (5): 796-808.

参考文献

[1] Kdawson. Software bug halts F-22 flight. (2007-02-25). http://it.slashdot.org/story/07/02/25/2038217/Software-Bug-Halts-F-22-Flight.
[2] Kovach B. Military loses control of helicopter drone near Washington. (2010-08-26). http://articles.cnn.com/2010-08-25/us/runaway.helicopter_1_unmanned-helicopter-drone-aircraft?_s=PM:US.
[3] Yin Y F, Liu B. Research on formal verification technique for aircraft safety-critical software. Journal of Computers, 2010, 5(8): 1152-1159.
[4] DO-178B/ED-12B. Software considerations in airborne systems and equipment certification. RTCA/EUROCAE, 1992.
[5] RTCA. DO-178C Software considerations in airborne systems and equipment certification. Washington, D C: Radio Technical Commission for Aeronautics, Inc.(RTCA), 2008.
[6] Elmqvist J, Nadjm-Tehrani S. Safety-oriented design of component assemblies using safety interfaces. Electronic Notes in Theoretical Computer Science, 2007, 182(29): 57-72.
[7] Sakugawa B, Cury E,Yano E T. Airborne software concerns in civil aviation certification. Dependable Computing, 2005, 3747: 52-60.
[8] Sveda M, Oplustil V. Experience with integration and certification of COTS based embedded system into advanced avionics system. SIES’07, IEEE, 2007: 282-287.
[9] Miller J, Mukerji J. MDA guide version 1.0.1(2003-06-01).http://www.ultradark.com/01mda13-userguide. htm.
[10] Wijbrans K, Buve F, Rijkers R, et al. Software engineering with formal methods: experiences with the development of a storm surge barrier control system. In Proceedings of the 15th International Symposium on Formal Methods (FM 2008). 2008: 419-424.
[11] Object Management Group. OMG systems modeling language (OMG SysML). (2010-06-01). http://www.omg.org/spec/SysML/1.2.
[12] Zoughbi G, Briand L C, Labiche Y. A UML profile for developing airworthiness-compliant (RTCA DO-178B) safety-critical software. In: Proceedings of ACM/IEEE International Conference on Model Driven Engineering Languages and Systems. 2007: 574-588.
[13] Panesar-Walawege R K, Sabetzadeh M, Briand L. Characterizing the chain of evidence for software safety cases: a conceptual model based on the IEC 61508 standard. In: 2010 Third International Conference on Software Testing, Verification and Validation, IEEE. 2010: 335-344.
[14] Bernardi S, Merseguer J, Petriu D C. Adding dependability analysis capabilities to the MARTE profile. MODELS 108. Proceedings of the 11th International Conference on Model Driven Engineering Languages and Systems. 2008: 736-750.
[15] Hungar H, Robbe O, Wirtz B. Safe-UML-Restricting UML for the development of safety-critical systems. Proceedings. FORMS/FORMAT 2007, 2007: 467-475.
[16] Object Management Group. UML profile for modeling and analysis of real-time and embedded systems (MARTE).(2010-06-25).http://www.omgmarte.org/node/88.
[17] Cofer D. Model checking: cleared for take off. model checking software. SPIN 2010, Verlag Berlin Heidelberg, LNCS 6349. 2010: 76-87.
[18] Zhang Y, Mei H. Non-functional attributes oriented description and verification in UML class diagrams. Journal of Software, 2010, 20(6): 1457-1469. (in Chinese) 张岩,梅宏.UML类图中面向非功能属性的描述和检验.软件学报,2010, 20(6):1457-1469.
[19] Esterel Technologies. Scade System.(2011-07-20). http://www.esterel-technologies.com//products/.
[20] Bochot T, Virelizier P, Waeselynck H, et al. Model checking flight control systems: the airbus experience. In Proceedings of the 31st International Conference on Software Engineering (ICSE 2009), Companion Volume, IEEE. 2009: 18-27.
[21] Kornecki A, Zalewski J. Certification of software for real-time safety-critical systems: state of the art. Innovations in Systems and Software Engineering, 2009, 5:149-161.
[22] Huhn M, Hungar H.UML for software safety and certfication. MBEERTS, LNCS 6100, 2010: 201-237.
[23] Zoughbi G, Briand L, Labiche Y. Modeling safety and airworthiness (RTCA DO-178B) information: conceptual model and uml profile. Software and Systems Modeling, 2010: 1-31.
[24] Hause M C, Thom F. An integrated safety strategy to model driven development with sysml. Proceedings of System Safety, 2007 2nd Institution of Engineering and Technology International Conference. London: IEEE, 2007: 124-129.
[25] Fujiwara T, Estevez J M, Satoh Y, et al. A calculation method for software safety integrity level. CARS’10 Proceedings of the 1st Workshop on Critical Automotive Applications: Robustness & Safety. ACM New York: NY, USA, 2010: 31-34.
[26] Papadopoulos Y, Walker M, Reiser M O, et al. Automatic allocation of safety integrity levels. CARS’10 Proceedings of the 1st Workshop on Critical Automotive Applications: Robustness & Safety. ACM New York: NY, USA, 2010: 7-10.
[27] Zhu Y, Huang Z Q, Cao Z N, et al. Method for generating software architecture models from formal specifications. Journal of Software, 2010, 21(11): 2738-2715. (in Chinese) 祝义, 黄志球, 曹子宁, 等.一种基于形式化规约生成软件体系结构模型的方法.软件学报, 2010, 21(11): 2738-2751.
[28] Hun J, Huang Z Q, Cao D, et al. Formal analysis and verification of resource adaptability for internetware. Journal of Software, 2008,19(5):1186-1200. (in Chinese) 胡军, 黄志球, 曹东, 等.网构软件的资源自适应性的形式化分析与验证.软件学报,2008, 19(5): 1186-1200.
[29] Liu Y S, Jiang Y Q, Gao S M. Model-driven modeling for system design of complex products: a survey. China Mechanical Engineering, 2010, 21(6): 741-749. (in Chinese) 刘玉生, 蒋玉芹, 高曙明.模型驱动的复杂产品系统设计建模综述. 中国机械工程, 2010, 21(6): 741-749.
[30] Iwu F, Galloway A, McDermid J, et al. Integrating safety and formal analyses using UML and PFS. Reliability Engineering and System Safety, 2007, 92(2): 156-170.
[31] Yi S H, Yang Y, Miao X W, et al. SysML-based safety analysis of thrust reverser. Journal of Aerospace Power, 2011, 26(3): 498-504. (in Chinese) 尹树悦, 杨云, 苗学问, 等. 基于SysML的反推力系统安全性分析. 航空动力学报, 2011, 26(3): 498-504.
[32] David P, Idasiak V, Kratz F. Reliability study of complex physical systems using SysML. Reliability Engineering and System Safety, 2010, 95(4): 431-450.

E-mail：hkxb@buaa.edu.cn

关于我们

期刊社服务

专业学科

封面文章

友情链接

主管单位：中国科学技术协会主办单位：中国航空学会北京航空航天大学

面向适航认证的模型驱动机载软件构件的安全性验证

Model-driven Safety Dependence Verification for Component-based Airborne Software Supporting Airworthiness Certification

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 4

编辑推荐

Metrics

本文评价

[1]	胡晓义, 王如平, 王鑫, 付永涛. 基于模型的复杂系统安全性和可靠性分析技术发展综述[J]. 航空学报, 2020, 41(6): 523436-523436.
[2]	黄斌达, 周来水, 安鲁陵, 卫炜, 王小平, 卜庆奎. 工序模型驱动的航空发动机零件机加夹具变型设计方法[J]. 航空学报, 2017, 38(1): 420091-420091.
[3]	朱和铨, 徐浩军, 张鹏, 张登成, 孙曦. 模型驱动的软件构件研制保证水平验证方法[J]. 航空学报, 2015, 36(3): 907-920.
[4]	宋利康;崔德刚;周儒荣. 企业模型与ERP系统间映射技术[J]. 航空学报, 2007, 28(6): 1513-1520.