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

摘要：

随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一.使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和SysML活动图两种模型语义描述的基础上,提出了一种基于故障扩展SysML活动图的安全性验证框架,包括:首先利用故障树最小割集提取故障信息并给出故障树逻辑门的转换规则;然后给出故障扩展SysML活动图的构建步骤;最后使用Promela对故障扩展SysML活动图进行建模,并使用模型检测工具SPIN对其进行分析验证.通过一个燃气灶控制系统验证了此方法的有效性.

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

所属期刊栏目：42

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2016-05-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：222-228