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