计算机科学 ›› 2016, Vol. 43 ›› Issue (11): 193-199.doi: 10.11896/j.issn.1002-137X.2016.11.038
胡军,石娇洁,程桢,陈松,王明明
HU Jun, SHI Jiao-jie, CHENG Zhen, CHEN Song and WANG Ming-ming
摘要： 近年来,基于模型的系统安全性分析与验证方法是安全关键系统工程领域中的一个重要研究方向。提出了一种基于四变量模型的系统安全性建模与分析验证方法,该方法利用AltaRica建模语言对系统进行建模。通过对四变量模型及AltaRica进行语义研究构建二者之间的映射规则,以民用飞机中机轮刹车系统(Wheel Brake System,WBS)为例来说明整个验证过程,即首先利用四变量模型从系统的需求层次上对WBS进行需求分析并根据映射关系构建AltaRica模型,接着利用故障树分析方法对WBS进行安全性研究,最后基于AltaRica配套工具ARC对系统的安全性属性进行验证。验证结果表明了该方法在系统安全工程领域中的实用性。
| [1] Bouali A,Dion B.Formal Verification for Model-Based Development[J].Sae Transactions,2005,114(7):171-181 [2] Feiler P H.Model-based validation of safety-critical embedded systems[C]∥Proceedings of the Aerospace Conference.2010 IEEE,2010:1-10 [3] Shokry H,Hinchey M.Model-Based Verification of Embedded Software[J].Computer,2009,42(4):53-59 [4] Battueux M,Prosvirnova T,Rauzy A,et al.The AltaRica 3.0 project for model-based safety assessment[C]∥2013 11th IEEE International Conference on Proceedings of the Industrial Informatics(INDIN).2013:127-132 [5] Humbert S,Seguin C,Castel C,et al.Deriving Safety SoftwareRequirements from an AltaRica System Model[M]∥Computer Safety,Reliability,and Security.Springer Berlin Heidelberg,2008:320-331 [6] Li S,Su D.A Practicable MBSA Modeling Process Using Altarica[M]∥Model-Based Safety and Assessment.Springer International Publishing,2014:1-13 [7] Patcas L M,Lawford M,Maibaum T.From System Require-ments to Software Requirements in the Four-Variable Model[J/OL].http://core.al.uk/display/23645454 [8] Patcas L M,Lawford M,Maibaum T.Implementability of requirements in the four-variable model[J].Science of Computer Programming,2015,111(P2):339-362 [9] Miller S P,Tribble A C.Extending the four-variable model to bridge the system-software gap [J].Digital Avionics Systems dascconference,2001:4E5/1-4E5/11 [10] Farkas H,Noszticzius Z.Analytical investigation of a four-variable model of the BZ reaction[J].Reaction Kinetics & Catalysis Letters,1987,33(1):93-98 [11] Heitmeyer C L,Jeffords R D,Labaw B G.Automated Consistency Checking of Requirements Specifications[J].Automated Consistency Checking of Requirements Specifications,1996,5(3):231-261 [12] Point G,Rauzy A.AltaRica:Constraint automata as a description language[J/OL].http://altarica.labri.fr/pub/publications/PR996.pdf [13] Bieber P,Bougnol C,Castel C,et al.Safety Assessment with Altarica[J].Journal of the American College of Cardiology, 2004,53(11):982-991 [14] Joshi A,Miller S P,Whalen M,et al.A proposal for model-based safety analysis[C]∥Proceedings of the Digital Avionics Systems Conference,2005(DASC 2005).2005 [15] Cassez F,Pagetti C,Roux O.A Timed Extension for ALTARICA[J].Fundamenta Informaticae,2004,62(3/4):291-332 [16] Bozzano M,Cimatti A,Lisagor O,et al.Symbolic Model Checking and Safety Assessment of Altarica models[J/OL].http://journal.ub.tu-berlin.de/eceasst/article/view/697 [17] Bieber P,Castel C,Seguin C.Combination of Fault Tree Analysis and Model Checking for Safety Assessment of Complex System[M]∥Dependable Computing EDCC-4.Springer Berlin Heidelberg,2002:19-31 [18] Lee W S,Grosh D L,Tillman F A,et al.Fault Tree Analysis,Methods,and Applications ? A Review[J].IEEE Transactions on Reliability,1985,34(3):194-203 [19] Boulanger J L.Safety Analysis of the Embedded Systems with the AltaRica Approach[M].Industrial Use of Formal Methods:Formal Verification.John Wiley & Sons,Inc.,2013:83-121 |
| No related articles found! |
|
||
首页