一种基于故障扩展SysML活动图的安全性验证框架研究  

Research on Framework of Safety Verification Based on Fault-extended SysML Activity Diagram

作　　者：仵志鹏 黄志球[1] 王珊珊[1] 曹德建 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016

出　　处：《计算机科学》2015年第7期222-228,共7页Computer Science

基　　金：国家自然科学基金(61100034;61170043);中国博士后科学基金(20110491411);江苏省普通高校研究生科研创新计划资助项目;中央高校基本科研业务费专项资金(CXZZ11_0218)资助

摘　　要：随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一。使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和SysML活动图两种模型语义描述的基础上,提出了一种基于故障扩展SysML活动图的安全性验证框架,包括:首先利用故障树最小割集提取故障信息并给出故障树逻辑门的转换规则;然后给出故障扩展SysML活动图的构建步骤;最后使用Promela对故障扩展SysML活动图进行建模,并使用模型检测工具SPIN对其进行分析验证。通过一个燃气灶控制系统验证了此方法的有效性。Embedded system has been widely used in safety-critical areas such as energy,transportation,etc.The safety analysis and verification for embedded software have always been one of the hot topics in both academia and industry.In order to unify function model and safety requirements analysis model of the system,we introduced extended SysML activity diagrams with semantic information of fault tree.On the basis of retaining the semantic descriptions of both the fault tree and the SysML activity diagram,we presented a kind of safety verification framework based on fault-extended SysML activity diagrams.Firstly,we used minimal cut sets to extract fault information and presented transformation rules of fault tree logic gate.Then,we presented build steps of fault-extended SysML activity diagrams.Finally,we used Promela to model fault-extended SysML activity diagrams and used model checking tool SPIN to analyze and verify it.We verified the effectiveness of the method by using it in a gas stove control system.

关 键 词：安全性验证 故障树语义 SysML活动图 PROMELA 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]