一种结合线性时序逻辑和故障树的软件安全验证方法  

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

作　　者：王飞[1] 沈国华[1] 黄志球[1] 马琳[1] 刘畅[2] 李海峰[2] 廖莉莉[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016 [2]中国航空综合技术研究所,北京100028

出　　处：《计算机科学》2015年第12期71-75,共5页Computer Science

基　　金：国家自然科学基金(61272083);国家高技术研究发展计划(863)(2009AA010307);国家国防科技工业局技术基础科研项目(Z052013B009;JSJC2013205C507)资助

摘　　要：嵌入式软件在安全关键领域的广泛应用使得保障软件的安全性成为学界的研究热点。故障树技术是工业界常用的传统的安全分析方法之一。然而,传统的故障树无法精确描述安全关键系统中具有时序特征的系统故障。针对此问题,给出了一种结合线性时序逻辑和故障树的安全验证方法。该方法运用线性时序逻辑对故障树进行形式化规约,从中抽取出软件安全属性并用时序逻辑公式进行描述,用以支持对安全关键软件的模型检验。最后,以某机载控制系统软件数据处理故障模块的模型检验为例,来说明该方法的有效性和可行性。Embedded software is playing an important role in safety critical field. How to ensure the safety of safetycritical 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.

关 键 词：故障树分析 模型检验 线性时序逻辑 安全关键系统 安全属性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]