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

doi:CNKI:11-1929/V.20120201.0941.002

Abstract

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

CLC Number:

V328
TP311

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.

References

[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.

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

PDF (PC)

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 8

Recommended Articles

Metrics

Comments

[1]	Guochi GAO, Bo ZHANG, Jingze QUAN, Chong YIN, Li DING, Yubiao JIANG. Airworthiness certification technology of normal aircraft natural icing flight test [J]. Acta Aeronautica et Astronautica Sinica, 2024, 45(1): 128531-128531.
[2]	Yong CHEN, Weiliang KONG, Hong LIU. Challenge of aircraft design under operational conditions of supercooled large water droplet icing [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2023, 44(1): 626973-626973.
[3]	ZHANG Lifen, GE Xin, LIU Zhenxia. Experimental study on mechanical properties of artificial hail [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2021, 42(2): 224255-224255.
[4]	HU Xiaoyi, WANG Ruping, WANG Xin, FU Yongtao. Recent development of safety and reliability analysis technology for model-based complex system [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2020, 41(6): 523436-523436.
[5]	MA Zan, ZHOU Zhonghua, WANG Peng, HU Jianbo, KE Bingqing. Analysis of airworthiness requirements of BDS airborne equipment for aircraft tracking only [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2019, 40(11): 323155-323155.
[6]	LI Zhiping, WANG Mengqi. Airworthiness certification method for aeroengine on stall and surge with inlet distortion [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2015, 36(9): 2947-2957.
[7]	ZHU Hequan, XU Haojun, ZHANG Peng, ZHANG Dengcheng, SUN Xi. Model-driven validation method for software component development assurance level [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2015, 36(3): 907-920.
[8]	LU Zhong, RONG Xiang, ZHOU Jia, CHEN Kang. TLD analysis method of dispatch with multiple faults based on Monte Carlo simulation for FADEC system [J]. ACTA AERONAUTICAET ASTRONAUTICA SINICA, 2015, 36(12): 3970-3979.