计算机科学 ›› 2015, Vol. 42 ›› Issue (12): 71-75.
王飞,沈国华,黄志球,马 琳,刘 畅,李海峰,廖莉莉
WANG Fei, SHEN Guo-hua, HUANG Zhi-qiu, MA Lin, LIU Chang, LI Hai-feng and LIAO Li-li
摘要： 嵌入式软件在安全关键领域的广泛应用使得保障软件的安全性成为学界的研究热点。故障树技术是工业界常用的传统的安全分析方法之一。然而,传统的故障树无法精确描述安全关键系统中具有时序特征的系统故障。针对此问题,给出了一种结合线性时序逻辑和故障树的安全验证方法。该方法运用线性时序逻辑对故障树进行形式化规约,从中抽取出软件安全属性并用时序逻辑公式进行描述,用以支持对安全关键软件的模型检验。最后,以某机载控制系统软件数据处理故障模块的模型检验为例,来说明该方法的有效性和可行性。
| [1] Peled D A.Software reliability methods[M].Springer Science & Business Media,2013 [2] Lee W S,Grosh D,Tillman F A,et al.Fault Tree Analysis,Methods,and Applications-A Review[J].IEEE Transactions on Reliability,1985,34(3):194-203 [3] 苏晓勤.FTA故障树分析算法改进研究与实现[D].天津:河北工业大学,2005 Su X Q.Research on Improving and Realizing Arithmatic of Fault Tree Analysis [D].Tianjin:Hebei University of Technolo-gy,2005 [4] 龚海里.故障树计算机辅助分析优化算法研究与应用[D].大连:大连理工大学,2004 Gong H X.Research and Application of Computer Aided Analysis Optimization Algorithm in Fault Tree [D].Dalian:Dalian University of Technology,2004 [5] 陈建军.关于故障树分析中联合重要度的研究[D].大连:大连交通大学,2009 Chen J J.Research of Joint Failure Importance in Fault Tree Analysis [D].Dalian:Dalian Jiaotong University,2009 [6] Palshikar G K.Temporal fault trees[J].Information and Software Technology,2002,44(3):137-150 [7] Cˇepin M,Mavko B.A dynamic fault tree[J].Reliability Engineering & System Safety,2002,75(1):83-91 [8] Gluchowski P.Duration Calculus for Analysis of Fault Treeswith Time Dependencies[C]∥2nd International Conference on Dependability of Computer Systems.2007:107-114 [9] 刘磊.软件时序故障树建模与分析技术研究[D].长沙:国防科学技术大学,2011 Liu L.Research on Modeling and Analysis Techniques for Software Temporal Fault Tree[D].Changsha:National University of Defense Technology,2011 [10] Schfer A.Combining real-time model-checking and fault treeanalysis[M]∥FME 2003:Formal Methods.2003:522-541 [11] Koh K Y,Seong P H.SMV model-based safety analysis of software requirements[J].Reliability Engineering & System Safety,2009,94(2):320-331 [12] Cha S,Yoo J.A safety-focused verification using software fault trees[J].Future Generation Computer Systems,2012,28(8):1272-1282 [13] Pnueli A.The temporal logic of programs[C]∥18th AnnualSymposium on IEEE.1977:46-57 [14] 马琳,黄志球,徐丙凤,等.支持模型检测的故障树生成方法研究[J].计算机与数字工程,2013,0(2):257-260 Ma L,Huang Z Q,Xu B F,et al.A Fault Tree Analysis Method Supporting Model Checking[J].Computer&Digital Enginee-ring,2013,0(2):257-260 [15] Platz O,Olsen J V.FAUNET:a program package for evaluation of fault trees and networks[J].Research Establishment Risk Report,1976,8(41):97-103 [16] 吕威,黄志球,陈哲,等.ESpin:基于SPIN的Eclipse模型检测环境[J].计算机工程与应用,2013,9(7):45-51 Lv W,Huang Z Q,Chen Z,et al.ESpin:SPIN-based Eclipse model checking environment.Computer Engineering and Applications[J].Computer Engineering and Applications,2013,9(7):45-51 |
| No related articles found! |
|
||
首页