| 一种基于故障扩展SysML活动图的安全性验证框架研究 |
| |
| 引用本文： | 仵志鹏,黄志球,王珊珊,曹德建.一种基于故障扩展SysML活动图的安全性验证框架研究[J].计算机科学,2015,42(7):222-228. |
| |
| 作者姓名： | 仵志鹏 黄志球 王珊珊 曹德建 |
| |
| 作者单位： | 南京航空航天大学计算机科学与技术学院 南京210016 |
| |
| 基金项目： | 本文受国家自然科学基金(61100034,3),中国博士后科学基金(20110491411),江苏省普通高校研究生科研创新计划资助 |
| |
| 摘 要： | 随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一。使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和SysML活动图两种模型语义描述的基础上,提出了一种基于故障扩展SysML活动图的安全性验证框架,包括:首先利用故障树最小割集提取故障信息并给出故障树逻辑门的转换规则；然后给出故障扩展SysML活动图的构建步骤；最后使用Promela对故障扩展SysML活动图进行建模,并使用模型检测工具SPIN对其进行分析验证。通过一个燃气灶控制系统验证了此方法的有效性。
|
| 关 键 词： | 安全性验证 故障树语义 SysML活动图 Promela |
Research on Framework of Safety Verification Based on Fault-extended SysML Activity Diagram |
| |
| WU Zhi-peng HUANG Zhi-qiu WANG Shan-shan CAO De-jian.Research on Framework of Safety Verification Based on Fault-extended SysML Activity Diagram[J].Computer Science,2015,42(7):222-228. |
| |
| Authors: | WU Zhi-peng HUANG Zhi-qiu WANG Shan-shan CAO De-jian |
| |
| Affiliation: | College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China |
| |
| Abstract: | |
| |
| Keywords: | Safety verification Semantic information of fault tree SysML activity diagram Promela |
|
|
点击此处可从《计算机科学》下载全文 |
