Computer Science ›› 2015, Vol. 42 ›› Issue (12): 71-75.

Previous Articles     Next Articles

Method Combining Linear Temporal Logic and Fault Tree for Software Safety Verification

WANG Fei, SHEN Guo-hua, HUANG Zhi-qiu, MA Lin, LIU Chang, LI Hai-feng and LIAO Li-li   

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

Abstract: Embedded software is playing an important role in safety critical field.How to ensure the safety of safety-critical software has recently become a research focus.The fault tree technique is a safety analysis method which is commonly used in traditional industry.However,FTA (Fault Tree Analysis) itself lacks formal temporal semantics.To solve the problem,this paper proposed a method to verify the safety of embedded software combining linear temporal logic and FTA.Applying linear temporal logic to formal specification of the fault tree,it extracts the software safety properties from the formal fault tree and describes them with the temporal logic.Expert can use the extracted safety properties to do model checking of the safety-critical software,to analyze and verify its reliability and safety.The paper applied the model checking to a module of a safety-critical airborne software to demonstrate the method in detail.

Key words: Fault tree analysis,Model checking,Linear temporal logic,Safety-critical system,Safety property

[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] Schfer 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!
Full text



No Suggested Reading articles found!