计算机科学 ›› 2015, Vol. 42 ›› Issue (7): 222-228.doi: 10.11896/j.issn.1002-137X.2015.07.048
仵志鹏 黄志球 王珊珊 曹德建
WU Zhi-peng HUANG Zhi-qiu WANG Shan-shan CAO De-jian
摘要: 随着嵌入式系统在能源、交通等安全关键领域的广泛应用,针对嵌入式软件的安全性分析与验证方法一直是学术界和工业界的研究热点之一。使用扩展了故障树语义信息的SysML活动图来统一系统的功能模型与安全需求分析模型,并在保留故障树和SysML活动图两种模型语义描述的基础上,提出了一种基于故障扩展SysML活动图的安全性验证框架,包括:首先利用故障树最小割集提取故障信息并给出故障树逻辑门的转换规则;然后给出故障扩展SysML活动图的构建步骤;最后使用Promela对故障扩展SysML活动图进行建模,并使用模型检测工具SPIN对其进行分析验证。通过一个燃气灶控制系统验证了此方法的有效性。
[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] Snchez 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! |
|