摘要
近年来,随着航空、交通、医疗等安全关键系统的规模越来越大,涉及到的复杂度也越来越高,基于模型的系统安全性分析与验证成为安全关键系统工程领域的一个重要研究方向,因而如何对以SysML为典型的系统模型进行安全性分析与验证是一个非常重要的问题。文中以基于模型的安全性分析(MBSA)为框架,设计了一个面向SysML模型的系统安全性分析与验证方法,实现了从模型构建到安全性分析与属性验证的完整过程。首先,从需求层面和设计层面对SysML系统架构设计模型和最新系统安全性建模语言AltaRica3.0进行了介绍,构建了从SysML的核心模型元素到AltaRica3.0模型的语义等价的转换规则,给出了转换规则的形式化描述并分析证明转换规则的正确性;然后,基于模型驱动的方法设计了一个原型工具平台来完成模型的自动转换和安全性分析过程,该原型工具集成了转换、编译生成故障树、故障树分析、单步仿真及故障路径动态演示等功能,实现了系统设计和安全性分析的同步性,并在此基础上给出了AltaRica3.0至Promela模型的转换关键点,结合穷尽式模型验证工具SPIN对模型的属性进行安全性验证;最后,根据4761标准中对机轮刹车系统的体系结构设计描述和安全性的需求建立SysML模型,依据原型工具平台和属性验证工具实现模型的自动转换和安全性分析验证,进而来说明此转换方法的有效性。
In recent years,with the increasing scale and complexity of safety-critical systems such as aviation,transportation and medical treatment,model-based system safety analysis and verification has become an important research direction in the field of safety-critical system engineering.How to analyze and verify the safety of SysML as a typical system model is a very important issue.Based on the framework of model-based safety analysis,this paper designed a safety analysis and verification method for the SysML models,which realizes the complete process from model construction to safety analysis and attribute verification.Firstly,this paper introduced SysML system architecture design model and the latest system safety modeling language AltaRica3.0 from requirement level and design level,constructed the semantic equivalence transformation rules from the core model elements of SysML to AltaRica 3.0,gave the formal description of transformation rules,analyzed and proved the transformation rules.Then,this paper designed a prototype tool platform based on the model-driven method to complete the process of automatic transformation and safety analysis of the model.The prototype tool combines the functions of transformation,compilation and generation of fault tree,fault tree analysis,stepwise simulation and dynamic demonstration of fault path.The synchronization of system design and safety analy-sis was realized.On the basis of this,the key points of transformation from AltaRica 3.0 to Promela model were given,and the attributes of the model were verified by the exhaustive model verification tool SPIN.Finally,the SysML model was established according to the architecture design description and safety requirements of the wheel brake system in 4761 standard,and the automatic conversion,safety analysis and verification of the model were realized based on the prototype tool platform and attribute verification tool,which further illustrates the effectiveness of the conversion method.
作者
李宛倩
胡军
陈松
张维珺
LI Wan-qian;HU Jun;CHEN Song;ZHANG Wei-jun(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)
出处
《计算机科学》
CSCD
北大核心
2019年第11期100-108,共9页
Computer Science
基金
国家重点基础研究发展计划-973计划(2014CB744903)
国家航空科学基金(20165515001)
南京航空航天大学研究生创新基地开放基金(kfjj20171611)
中央高校基本科研业务费专项资金资助
