计算机科学 ›› 2015, Vol. 42 ›› Issue (7): 222-228.doi: 10.11896/j.issn.1002-137X.2015.07.048

• 软件与数据库技术 • 上一篇    下一篇

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

仵志鹏 黄志球 王珊珊 曹德建   

  1. 南京航空航天大学计算机科学与技术学院 南京210016
  • 出版日期:2018-11-14 发布日期:2018-11-14
  • 基金资助:
    本文受国家自然科学基金(61100034,3),中国博士后科学基金(20110491411),江苏省普通高校研究生科研创新计划资助

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   

  • Online:2018-11-14 Published:2018-11-14

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

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

Abstract: 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.

Key words: Safety verification,Semantic information of fault tree,SysML activity diagram,Promela

[1] 黄志球,徐丙风,阚双龙,等.嵌入式机载软件安全性分析标准、方法及工具研究综述[J].软件学报,2014,5(2):200-218 Huang Zhi-qiu,Xu Bing-feng,Kan Shuang-long,et al.Survey on Embedded Software Safety Analysis Standards,Methods and Tools for Airborne System [J].Journal of Software,2014,25(2):200-218
[2] Vesely W E,et al.Fault tree handbook[R].Washington DC:U.S.Nuclear regulatory commission,1981
[3] OMG.Unified Modeling Language:super structure v2.0[EB/OL].http://www.omg.org/docs/formal/05-07-04.pdf,2005
[4] OMG.Systems Modeling Language.v1.2[EB/OL].http://www.omg.org/spec/SysML/1.2,8
[5] 肖美华,薛锦云.基于 SPIN/Promela 的并发系统验证[J].计算机科学,2004,31(8):201-203 Xiao Mei-hua,Xue Jin-yun.Verification of Concurrent System Using SPIN/Promela[J].Computer Science,2004,31(8):201-203
[6] Walker M,Papadopoulos Y,et al.Qualitative temporal analysis:Towards a full implementation of the Fault Tree Handbook[J].Control Engineering Practice,2009,17(10):1115-1125
[7] Chu T L,Apostolakis G.Methods for probabilistic analysis ofnoncoherent fault trees[J].IEEE Transactions on Reliability,1980,29(5):354-360
[8] Schellhorn G,Thums A,Reif W.Formal fault tree semantics[C]∥Proceedings of The Sixth World Conference on Integrated Design & Process Technology,Pasadena,CA.2002
[9] Jarraya Y,Debbabi M,Bentahar J.On the meaning of SysML activity diagrams[C]∥16th Annual IEEE International Confe-rence and Workshop on Engineering of Computer Based Systems(ECBS 2009).IEEE,2009:95-105
[10] 樊晓光,褚文奎,张凤鸣.软件安全性研究综述[J].计算机科学,2011,38(5):8-13 Fan Xiao-guang,Chu Wen-kui,Zhang Feng-ming.Surveys on Softwate safety[J].Computer Science,2011,38(5):8-13
[11] 薛克.基于 SPIN 的 UML 活动图验证[D].上海:华东师范大学,2008 Xue Ke.Verification of UML ctivity chart using Spin[D].Shanghai:East China normal university,2008
[12] Guelfi N,Mammar A.A formal semantics of timed activity diagrams and its PROMELA translation[C]∥12th Asia-Pacific Software Engineering Conference(APSEC’05).IEEE,2005:8
[13] Ravn A P,Rischel H,et al.Specifying and verifying require-ments of real-time systems[J].IEEE Transactions on Software Engineering,1993,19(1):41-55
[14] Lano K,Kan P,et al.Linking hazard analysis to formal specification and design in B[M]∥Computer Safety,Reliability and Security.Springer Berlin Heidelberg,1998:60-74
[15] Ariss E O,Xu Dian-xiang,et al.Integrating safety analysis with functional modeling[J].IEEE Transactions on Systems,Man and Cybernetics,Part A:Systems and Humans,2011,41(4):610-624
[16] Snchez M A,Felder M.A Systematic Approach to Generate Test Cases based on Faults[C]∥ASSE 2003,Buenos Aires.2003
[17] Hansen K M,Ravn A P,et al.From safety analysis to software requirements[J].IEEE Transactions on Software Engineering,1998,24(7):573-584
[18] Nazier R,Bauer T.Automated Risk-Based Testing by Integrating Safety Analysis Information into System Behavior Models[C]∥2012 IEEE 23rd International Symposium on Software Reliability Engineering Workshops (ISSREW).IEEE,2012:213-218
[19] Reif W,Schellhorn G,et al.Safety analysis of a radio-basedcrossing control system using formal methods[C]∥9th IFAC Symposium Control in Transportation Systems.2000
[20] Dasso A,Funes A,et al.Verification,validation and testing in software engineering[M].IGI Global,2007

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!