基于時序描述邏輯的故障樹分析方法研究

司 佳，朱羿全，馬 琳

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 210016)

基于時序描述邏輯的故障樹分析方法研究

司 佳，朱羿全，馬 琳

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 210016)

故障樹分析法是工業界常用的安全分析方法之一。然而由于其非形式化方法的局限性，難以對軟件故障進行形式化驗證，更難以描述嵌入式實時系統中事件之間的時序邏輯關系。因此，提出了一種基于時序描述邏輯的故障樹分析方法,以解決故障樹難以對時序關系進行描述以及難以形式化驗證的問題。首先，通過時序描述邏輯對故障樹進行時序特征的擴充與規約；其次抽取出用描述邏輯表示的軟件安全屬性；最后對軟件系統進行安全屬性建模并通過模型檢測工具SPIN形式化驗證軟件系統是否滿足這些屬性。以某一機載控制系統環境輸入模塊為案例，對該案例進行故障樹分析和建模并給出該案例的待驗證安全屬性以及實驗分析結果。結果表明，提出的方法是有效的和可行的。

故障樹分析；時序描述邏輯；安全屬性；形式化驗證

0 引 言

目前故障樹分析法(Fault Tree Analysis,FTA)是學術界和工業界應用最為廣泛的安全性分析方法之一[1]。它首先分析了造成故障結果的所有原因，并給出了失效結果與失效原因之間的因果關系鏈，進而協助檢測系統的設計錯誤、安全缺陷以及薄弱環節[2]。

由于傳統的故障樹分析法一般采用非形式化方法進行描述，缺乏精確語義，因此難以對軟件故障進行形式化驗證。另一方面，由于其非形式化方法的局限性，使傳統的故障樹缺乏對具有時序特征的安全關鍵系統精確的描述方法[3]。

時序描述邏輯(Temporal Description Logic,TDL)是描述邏輯的時序擴展，既具有描述邏輯很強的表達和可判斷推理能力，又包含大量時序算子，可以對動態領域的知識進行描述[4]。

文中提出一種基于時序描述邏輯的故障樹分析方法，旨在將時序描述邏輯與傳統故障樹分析方法相結合。首先利用時序描述邏輯對故障樹進行時序擴充，而后從中抽取出描述軟件安全屬性的時序邏輯公式，最終實現軟件系統安全性的形式化驗證。

1 相關工作

如何將傳統的故障樹分析技術與形式化分析驗證方法相互結合，已成為國內外學者研究的熱點之一。文獻[5]采用PLTLP對故障樹的語義進行形式化，然而PLTLP的表達能力有限，無法描述復雜的時序性質；文獻[6]通過Z語言對故障樹進行了形式化規約，但由于Z語言的局限性，其缺乏對故障樹中安全屬性提取和正確性驗證的方法；文獻[7]為了能夠表達更多的故障，已經對軟件系統進行規約，其對現有的時序故障樹進行了TCTL擴充；文獻[8]提出一種用線性時序邏輯規約的時序故障樹LTFT，從中提取出描述系統時序故障的安全屬性，用于軟件安全性驗證。

2 時序描述邏輯

描述邏輯(Description Logic,DL)是一種基于對象的知識表示形式化方法[9]。它建立在概念(concept)和角色(role)之上。概念是一類事物的抽象，通常用A,B,C,D…表示；而角色則用來刻畫事物之間的各種聯系和關系，通常用P,Q,R,S…P表示?；A描述邏輯知識詳見文獻[9]。

時序描述邏輯主要是在基礎的描述邏輯上擴展了4個時序邏輯算子[10-11]：○、□、◇和∪，詳細說明如表1所示。

表1 時序描述邏輯擴展的時序算子

2.1 TDL擴展的語法和語義

(1)TDL擴展的語法。

其中，C和D表示為描述邏輯中的概念；R1和R2表示角色；φ和ψ表示公式；、、◇為一目算子；∪為二目算子，用來表示左式一直為真，直到右式為真。

(2)TDL擴展的語義。

假設時間流ζ=，其中T表示時間點的非空集合，<表示T中時間點之間嚴格的線性時序二元關系。TDL擴展部分的語義可描述如下[12]：

(◇C)I={|?t1.t≤t1∧∈CI}

(□C)I={|?t1.t≤t1∧∈CI}

(C∪D)I={|?t1.t≤t1∧∈DI∧?t2.t∈CI}

2.2 TDL擴展后的可滿足性

由于文獻[13]已證明，描述邏輯的推理問題均可以規約為可滿足性問題，可滿足性的定義如下：

(1)(M,i)|=C=D?CI(i)=DI(i)

(2)(M,i)|=a:C?aI(i)∈CI(i)

(3)(M,i)|=aRb?aI(i)RbI(i)

(4)(M,i)|=φ∪ψ??j>i,(M,i)|=ψ&&?k.(i≤k

(5)(M,i)|=φ?(M,i+1)|=φ

(6)(M,i)|=◇φ??j>i,(M,j)|=φ

(7)(M,i)|=□φ??j>i,(M,j)|=φ

(8)(M,i)|=φ→ψ?(M,i)|=φ→(M,i)|=ψ

3 基于TDL的形式化故障樹構建

文中工作的核心是構建帶有形式化信息的故障樹，并從中抽取支持形式化驗證的軟件安全屬性。因此，首先利用時序描述邏輯對傳統故障樹進行擴充，生成支持安全屬性規約的能夠形式化表示的時序描述邏輯故障樹。

時序描述邏輯故障樹保留了傳統故障樹中的全部邏輯門和事件[14]，在此基礎上引入與TDL時序算子相對應的○、□、◇和∪時序邏輯門：

(1)“○”門分別有一個輸出事件以及一個輸入事件。當“○”門的輸入故障事件在系統運行的下一個時刻為永真，“○”門的輸出故障事件發生。

(2)“□”門分別有一個輸出事件和一個輸入事件。若“□”的輸入故障事件在整個系統運行時間內為永真，則“□”門的輸出故障事件發生。

(3)“◇”門分別有一個輸出事件和一個輸入事件。若“◇”門下的輸入故障事件在系統運行時間內的某一時刻為真，則“◇”門的輸出故障事件發生。

(4)對于條件“A∪B”而言，此“∪”門有兩個輸入事件A和B以及一個輸出事件C，只有滿足條件“A∪B(即事件A為真，直到事件B為真)”時，輸出事件C才發生。

引入以上時序邏輯門后，基于TDL的故障樹構建原則仍遵循傳統故障樹的基本原則[14]。在傳統的故障樹構建過程中，不允許邏輯門之間直接相連。而由于引進了時序邏輯門，為了正確地構建故障樹，文中允許時序邏輯門與普通邏輯門以及時序邏輯門之間的直接相連。舉例說明如圖1所示。

圖1 傳統故障樹與形式化故障樹對比

4 軟件安全屬性的提取及驗證

4.1 安全屬性的提取

通過對傳統故障樹的擴展和形式化規約構建出能夠描述時序關系的形式化故障樹。在此基礎上，研究形式化故障樹安全屬性的提取過程，給出一個基于“上行法”的故障樹安全屬性提取算法，為軟件系統模型的形式化驗證提供證據?！吧闲蟹ā笔莻鹘y故障樹分析方法中一種常規分析法，其基本思想是從故障樹的基本事件開始，由下到上進行規約。基于“上行法”提取形式化故障樹安全屬性的流程如下：

步驟一：自底向上遍歷TDL擴充的故障樹，根據下層的TDL公式以及事件之間的邏輯門關系，給出新的TDL公式來描述上一層邏輯門的輸出或輸出事件；

步驟二：判斷當前TDL公式是否是最簡形式，若不是，則執行步驟四；

步驟三：判斷當前事件是否為頂事件，若是，則執行步驟五，否則執行步驟一；

步驟四：對TDL公式進行約簡,并執行步驟三；

步驟五：得到描述頂事件的描述邏輯公式，即為系統需要被驗證的安全屬性。

4.2 安全屬性的形式化驗證

形式化驗證方法的主要思路是使用數學的公式、定理和系統來驗證一個系統的正確性[15]。目前常用的形式化驗證方法主要包括模型檢測和定理證明。文中采用模型檢測方法，運用Promela語言對軟件系統形式化建模，驗證所提取的安全屬性。

方法的具體實施流程如圖2所示。首先，用時序描述邏輯對傳統故障樹進行擴充和形式化規約，形成能夠形式化描述系統時序故障的形式化故障樹。根據3.1節安全屬性提取算法，從形式化故障樹中提取出描述系統安全屬性的TDL公式；其次，根據TDL公式，利用Promela進行系統建模，得到待驗證的系統模型；最后，將待驗證的安全屬性和系統模型導入SPIN中進行驗證，并根據SPIN提供的驗證結果對系統進行安全性分析。

圖2 安全屬性形式化驗證流程

5 實例分析

為了說明文中方法的有效性，更清晰地演示方法的運用過程，給出某一機載控制系統環境輸入模塊代碼的安全性驗證與分析案例。

環境輸入模塊主要負責采集不斷變化的外界環境參數，其失效模式的初始化故障樹描述如圖3所示。

圖3 環境輸入模塊故障樹

根據文中方法對該故障樹進行形式化擴充，如圖4所示。

圖4 基于TDL擴展后的形式化故障樹

再利用3.1節提出的calTDL算法對擴展后的形式化故障樹進行安全屬性提取，得出3條通過TDL表達式描述的待驗證的安全屬性：

(1)割集為{Sub-Tree1}，表示該模塊接受函數始終無法響應，其對應的TDL表達式為：□(g_SciaRX_Ready==1)；

(2)割集為{EnviBase2}，表示為緩沖區溢出，其對應TDL表達式為：◇(g_dRegLength>MAX_REG)；

(3)割集為{Sub-Tree2}，表示計數器始終無法及時清零，其對應的TDL表達式為：□(SCIRXCounter==0)。

再利用模型檢測工具SPIN對環境輸入模塊進行形式化驗證。SPIN是基于Promela語言的主流模型檢測工具之一[16]。

輸入一：Promela語言描述的環境輸入模塊；

輸入二：待驗證的3條安全屬性；

輸出結果：環境輸入模塊是否滿足這3條安全屬性。

圖5 SPIN驗證結果

由圖中結果可以說明，由于環境輸入模塊的計數器無法及時清零，導致程序多次執行了空語句，浪費了寶貴的計算資源。

6 結束語

針對傳統故障樹分析法缺乏形式化語義、無法解決時序問題的缺陷，提出一種基于時序描述邏輯的故障樹分析方法。將時序描述邏輯與故障樹相結合，并給出了具體的形式化故障樹擴展方法；在此基礎上，給出了一種提取故障樹安全屬性的算法，并將安全屬性用于系統的模型檢測。下一步工作的重點是研究如何對故障樹本身的正確性進行驗證。

[1] Lee W S,Grosh D,Tillman F A,et al. Fault tree analysis,methods,and application:a review[J].IEEE Transactions on Reliability,1985,34(3):194-203.

[2] 馬 琳,黃志球,徐丙鳳,等.支持模型檢測的故障樹生成方法研究[J].計算機與數字工程,2013,41(2):257-260.

[3] 黃志球,徐丙鳳,闞雙龍,等.嵌入式機載軟件安全性分析標準、方法及工具研究綜述[J].軟件學報,2014,25(2):200-218.

[4] 楊海波.基于時序描述邏輯的UML狀態圖語義研究[D].蘭州:蘭州理工大學,2010.

[5] Palshikar G K.Temporal fault trees[J].Information and Software Technology,2002,44(3):137-150.

[6] Coppit D,Sullivan K J,Dugan J B.Formal semantics of models for computational engineering:a case study on dynamic fault trees[C]//Proceedings of 11th international symposium on software reliability engineering.[s.l.]:IEEE,2000:270-282.

[7] 劉 磊.軟件時序故障樹建模與分析技術研究[D].長沙：國防科學技術大學,2011.

[8] 馬 琳.基于故障樹的航電軟件系統安全性驗證方法研究[D].南京：南京航空航天大學,2012.

[9] Badder F,Nutt W.The description logic hand book:theory,implementation and application[M].Cambridge:Cambridge University Press,2002.

[10] Lutz C,Wolter F,Zakharyaschev M.Temporal description logic:a survey[C]//Proceedings of the 15th international symposium on temporal representation and reasoning.Washington,DC:IEEE,2008:3-14.

[11] 李 明,劉士儀,年福忠.基于時序描述邏輯的Web服務本體語言過程模型語義[J].計算機應用,2013,33(1):266-269.

[12] 榮先球.基于描述邏輯的UML行為圖的形式化研究[D].蘭州:蘭州理工大學,2012.

[13] Baader F,Bauer A,Lippmann M.Runtime verification using a temporal description logic[C]//Proceedings of 7th international conference on frontiers of combining systems.Berlin:Springer-Verlag,2009:149-164.

[14] Vesely W E,Goldberg F F,Roberts N H,et al.Fault tree handbook[M].United States:U.S. Nuclear Regulatory Commission,1981.

[15] Schamann J M.Automated theorem proving in software engineering[M].Berlin:Springer-Verlag,2001.

[16] Huth M,Ryan M.Logic in computer science:modeling and reasoning about systems[M].Cambridge,UK:Cambridge University Press,2004.

ResearchonFaultTreeAnalysisBasedonTemporalDescriptionLogic

SI Jia，ZHU Yi-quan，MA Lin

(School of Computer Science and Technology，Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

Fault Tree Analysis (FTA) is one of safety analysis methods which is commonly used in industry.However,as the limitation of its non-formal method,it is difficult to be formal verification of software fault and even to describe the temporal logic relation between events in embedded real-time system.Therefore,in order to solve the problem,a formal fault tree analysis based on Temporal Description Logic (TDL) is proposed.Firstly,the fault tree is extended and constrained in temporal sequence characteristic by TDL.Secondly,safety attributes of software are extracted in the representation of TDL.At last,the safety attributes modeling is carried out in software system which is verified whether to meet these attributes or not by SPIN,a model checking tool.A case of environment input module of airborne control system is given where the analysis and modeling of fault tree is conducted,and its security attributes to be checked and experimental results are achieved.It is showed that the proposed method is effective and feasible.

fault tree analysis;temporal description logic;safety attributes;formal verification

TP311

A

1673-629X(2017)12-0089-04

10.3969/j.issn.1673-629X.2017.12.020

2016-11-30

2017-04-05 < class="emphasis_bold">網絡出版時間

時間：2017-08-01

國家自然科學基金資助項目(61272083,61100034,61170043);中央高校基本科研業務費專項資金(NS2014099)；江蘇省自然科學基金青年基金項目(BK20130812)

司 佳(1992-),男,碩士研究生，研究方向為需求工程、安全工程。

http://kns.cnki.net/kcms/detail/61.1450.TP.20170801.1554.054.html