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

司 佳，朱羿全，馬 琳

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

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

司 佳，朱羿全，馬 琳

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

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

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

0 引 言

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

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

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

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

1 相關(guān)工作

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

2 時序描述邏輯

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

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

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

2.1 TDL擴展的語法和語義

(1)TDL擴展的語法。

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

(2)TDL擴展的語義。

假設(shè)時間流ζ=，其中T表示時間點的非空集合，<表示T中時間點之間嚴格的線性時序二元關(guān)系。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]已證明，描述邏輯的推理問題均可以規(guī)約為可滿足性問題，可滿足性的定義如下：

(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的形式化故障樹構(gòu)建

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

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

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

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

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

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

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

圖1 傳統(tǒng)故障樹與形式化故障樹對比

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

4.1 安全屬性的提取

通過對傳統(tǒng)故障樹的擴展和形式化規(guī)約構(gòu)建出能夠描述時序關(guān)系的形式化故障樹。在此基礎(chǔ)上，研究形式化故障樹安全屬性的提取過程，給出一個基于“上行法”的故障樹安全屬性提取算法，為軟件系統(tǒng)模型的形式化驗證提供證據(jù)?！吧闲蟹ā笔莻鹘y(tǒng)故障樹分析方法中一種常規(guī)分析法，其基本思想是從故障樹的基本事件開始，由下到上進行規(guī)約?；凇吧闲蟹ā碧崛⌒问交收蠘浒踩珜傩缘牧鞒倘缦拢?/p>

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

步驟二：判斷當(dāng)前TDL公式是否是最簡形式，若不是，則執(zhí)行步驟四；

步驟三：判斷當(dāng)前事件是否為頂事件，若是，則執(zhí)行步驟五，否則執(zhí)行步驟一；

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

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

4.2 安全屬性的形式化驗證

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

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

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

5 實例分析

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

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

圖3 環(huán)境輸入模塊故障樹

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

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

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

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

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

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

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

輸入一：Promela語言描述的環(huán)境輸入模塊；

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

輸出結(jié)果：環(huán)境輸入模塊是否滿足這3條安全屬性。

圖5 SPIN驗證結(jié)果

由圖中結(jié)果可以說明，由于環(huán)境輸入模塊的計數(shù)器無法及時清零，導(dǎo)致程序多次執(zhí)行了空語句，浪費了寶貴的計算資源。

6 結(jié)束語

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

[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].計算機與數(shù)字工程,2013,41(2):257-260.

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

[4] 楊海波.基于時序描述邏輯的UML狀態(tài)圖語義研究[D].蘭州:蘭州理工大學(xué),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] 劉 磊.軟件時序故障樹建模與分析技術(shù)研究[D].長沙：國防科學(xué)技術(shù)大學(xué),2011.

[8] 馬 琳.基于故障樹的航電軟件系統(tǒng)安全性驗證方法研究[D].南京：南京航空航天大學(xué),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服務(wù)本體語言過程模型語義[J].計算機應(yīng)用,2013,33(1):266-269.

[12] 榮先球.基于描述邏輯的UML行為圖的形式化研究[D].蘭州:蘭州理工大學(xué),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">網(wǎng)絡(luò)出版時間

時間：2017-08-01

國家自然科學(xué)基金資助項目(61272083,61100034,61170043);中央高?；究蒲袠I(yè)務(wù)費專項資金(NS2014099)；江蘇省自然科學(xué)基金青年基金項目(BK20130812)

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

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