面向模型檢查的NuSMV統(tǒng)一建模方法

陳 露, 焦 健, 魏錢鋅

(北京航空航天大學(xué)可靠性與系統(tǒng)工程學(xué)院,北京 100191)

0 引 言

隨著規(guī)模和功能不斷增大,復(fù)雜大型裝備系統(tǒng)逐漸趨向于高度集成化,包含了各類嵌入式組件和軟硬件耦合的功能結(jié)構(gòu),給技術(shù)人員識別危險、分析事故過程帶來了更大困難和挑戰(zhàn)[1]。當(dāng)面臨復(fù)雜裝備系統(tǒng)時,傳統(tǒng)的安全分析技術(shù),如:故障模式影響分析(failure mode and effects analysis,FMEA)、故障樹分析(fault tree analysis,FTA)和危險與可操作性分析(Hazard and operability analysis,HAZOP)等[2-3],較多地依賴分析人員的經(jīng)驗(yàn),容易疏漏系統(tǒng)故障狀態(tài)或者誤判系統(tǒng)故障影響,從而降低了安全分析結(jié)果的準(zhǔn)確性和完整性。近年來,基于模型的安全性分析方法(model based safety analysis, MBSA)，采用了形式化模型和自動化分析過程,使安全性分析工作更加客觀和高效,已被廣泛應(yīng)用于航空航天等工業(yè)領(lǐng)域[4-7]。

開展MBSA的首要前提是構(gòu)建正確且完備的形式化模型。本文在MBSA現(xiàn)有框架下,基于新型符號模型檢查器(new symbolic model verifier,NuSMV)平臺研究提出面向模型檢查的統(tǒng)一建模方法,用于構(gòu)建包含系統(tǒng)正常模塊和故障模塊的耦合模型,支持安全性分析評估,提高安全性工作效率。

1 MBSA現(xiàn)狀與不足

MBSA是以研究和實(shí)現(xiàn)復(fù)雜系統(tǒng)建模并基于系統(tǒng)模型實(shí)現(xiàn)自動或半自動化的安全分析或驗(yàn)證為目的的一類理論及方法的統(tǒng)稱,能夠提高安全性分析效率,增強(qiáng)分析能力并減少人力和經(jīng)濟(jì)投入[7]。目前較為常用的MBSA理論與方法中包括:以故障邏輯建模技術(shù)(failure logic modelling, FLM)[8]為基礎(chǔ)的層次化危險起因與傳播研究(hierarchically performed Hazard origin and propagation studies,HiP-HOPS)[9],故障傳播與轉(zhuǎn)換符號(failure propagation and transformation notation,FPTN)[10]等故障邏輯分析技術(shù);系統(tǒng)符號化模型描述工具M(jìn)atlab/Simulink,安全關(guān)鍵應(yīng)用開發(fā)環(huán)境(safety-critical application development environment,SCADE)[11]等;系統(tǒng)建模語言(system modeling language,SysML),體系結(jié)構(gòu)分析與設(shè)計語言(architecture analysis & design language,AADL)[12],AltaRica[13-14]等,及用于實(shí)現(xiàn)自動安全驗(yàn)證的模型檢測工具NuSMV[15-16],安全分析與模型檢測相結(jié)合的工具[17]等。

MBSA流程大致包括3個階段[7,11,15]:首先是構(gòu)建能夠反映故障狀態(tài)及交互關(guān)系的系統(tǒng)模型;然后進(jìn)行模型轉(zhuǎn)換,便于模型檢查;最后利用模型檢查工具分析轉(zhuǎn)換后的模型,識別反例、驗(yàn)證安全性要求,完成安全性分析評估。其中建立形式化模型是MBSA的基礎(chǔ)和核心。現(xiàn)有的建模方法主要分為兩大思路:一種是先建立名義系統(tǒng)模型(nominal system model，NSM),描述系統(tǒng)在正常狀態(tài)下的行為;然后定義系統(tǒng)可能存在的故障模式,建立系統(tǒng)的故障模型;再通過模型擴(kuò)展將兩種模型結(jié)合[18]。另一種方法則采用故障邏輯的思路[16],直接面向系統(tǒng)中的故障建模,簡化甚至忽略系統(tǒng)的正常行為。前者構(gòu)建的模型更加全面真實(shí),但建模過程復(fù)雜,難度高;后者建模過程簡單,但模型提供的信息相對較少,在一定程度上會影響分析結(jié)論的全面性。

然而,復(fù)雜大型裝備系統(tǒng)故障模式的多樣性和復(fù)雜性給建模過程帶來了很大的阻礙。現(xiàn)有的大多數(shù)建模方法主要是對系統(tǒng)的功能結(jié)構(gòu)和運(yùn)行狀態(tài)進(jìn)行建模,對于系統(tǒng)的故障模式及其傳播過程的描述較為薄弱。此外,由于建模語言、工具平臺及模型檢查工具的種類繁雜,導(dǎo)致在模型的構(gòu)建、轉(zhuǎn)換和驗(yàn)證方面產(chǎn)生了許多問題[17,19],在一定程度上影響了MBSA方法的進(jìn)一步研究和應(yīng)用。

另一方面,MBSA通常采用模型檢查的方式開展分析,而模型檢查器一般需要專用的輸入語言來描述系統(tǒng)模型[20-21],例如目前已得到廣泛應(yīng)用的開源模型檢查工具NuSMV[19,22],因此通常需要進(jìn)行模型轉(zhuǎn)換。模型轉(zhuǎn)換過程中難免會產(chǎn)生信息損失,導(dǎo)致模型和真實(shí)系統(tǒng)之間產(chǎn)生偏差;并且模型中元素映射的難易程度不同,不同建模語言和驗(yàn)證工具的可用性和適用性也各有差異,即使不考慮信息損失,模型轉(zhuǎn)換的工作量及難度也較大,影響了工作效率。

鑒于此,本文直接面向模型檢查,研究提出了基于NuSMV平臺、包含系統(tǒng)正常和故障行為的統(tǒng)一建模方法,給出了建模總體框架和具體步驟。利用該方法構(gòu)建的模型可以直接用于模型檢查,避免了模型轉(zhuǎn)換可能帶來的信息損失,可以進(jìn)一步規(guī)范MBSA框架下的建模過程,提高安全性分析的準(zhǔn)確性;并且由于不再需要模型轉(zhuǎn)換,在客觀上也提高了工作效率。

2 基于NuSMV的統(tǒng)一建模方法

如圖1所示,基于NuSMV的統(tǒng)一建模方法可以概括為3個方面內(nèi)容,包括建模準(zhǔn)備、模型建立和模型檢查。

圖1 基于NuSMV的統(tǒng)一建模框架Fig.1 Unified modeling framework based on NuSMV

2.1 建模準(zhǔn)備

在分析一個復(fù)雜大型裝備系統(tǒng)時,首先要明確系統(tǒng)的定義,包括系統(tǒng)需求規(guī)范、故障模式及系統(tǒng)安全性要求等。

(1) 定義系統(tǒng)需求

在系統(tǒng)需求規(guī)范的基礎(chǔ)上,可以采用功能框圖來輔助明確系統(tǒng)的層級結(jié)構(gòu)、功能邏輯關(guān)系、性能參數(shù)及系統(tǒng)的輸入輸出等內(nèi)容,并對其進(jìn)行適當(dāng)?shù)暮喕统橄蟆０凑展δ苓壿嬯P(guān)系將系統(tǒng)劃分為各個不同的子系統(tǒng),表示為不同的NuSMV模塊,并確定每個子模塊的輸入和輸出。

(2) 定義故障模式

通過歷史數(shù)據(jù)手冊、可靠性試驗(yàn)及早期的系統(tǒng)安全性分析結(jié)果等獲取系統(tǒng)的故障數(shù)據(jù);進(jìn)而根據(jù)子系統(tǒng)內(nèi)各個部件發(fā)生功能喪失或者降級的方式和類型來確定各個子系統(tǒng)的故障模式。

(3) 定義安全性要求

根據(jù)系統(tǒng)的目標(biāo)和最終的輸出來確定子系統(tǒng)部件的功能喪失或者降級對系統(tǒng)狀態(tài)的影響。確定安全要求應(yīng)同時考慮系統(tǒng)的安全功能要求和安全完整性要求,可以參考系統(tǒng)設(shè)計要求和用戶需求。

2.2 模型建立

進(jìn)行模型檢查之前需要以有限狀態(tài)機(jī)(finite state machine, FSM)的形式對所給系統(tǒng)進(jìn)行建模,并采用模型檢驗(yàn)工具的輸入語言來描述系統(tǒng)的功能、層級和結(jié)構(gòu),要求所建立的模型在功能上要符合系統(tǒng)規(guī)范,在描述語言上要遵循模型檢查工具的語言規(guī)范。NuSMV的輸入語言可以通過模塊化分層的方式來描述整個復(fù)雜大系統(tǒng)的結(jié)構(gòu),也就是說不同的部件及其功能在NuSMV程序中可以通過獨(dú)立的模塊來表達(dá),以便于在保持系統(tǒng)原來的層級結(jié)構(gòu)的基礎(chǔ)上定義和區(qū)分不同的子系統(tǒng)。系統(tǒng)的行為通過每個組件功能模塊內(nèi)的變量來表示,而不同模塊之間的邏輯關(guān)系和接口是通過各個模塊的運(yùn)行狀態(tài)及相關(guān)參數(shù)的形式來表示的。

模型的基本結(jié)構(gòu)如圖2所示。在構(gòu)建系統(tǒng)模型的過程中,首先要為整個系統(tǒng)建立一個主模塊,在主模塊中逐一列出系統(tǒng)中所有子模塊。其次要為系統(tǒng)中的每一個子系統(tǒng)分別建立3個互相關(guān)聯(lián)的子模塊,分別是正常模塊、故障模塊和耦合模塊。每個模塊包含2個基本部分,分別是變量和賦值。變量部分定義所有變量及其取值范圍,賦值部分給每個變量賦初值并描述變量的狀態(tài)轉(zhuǎn)移情況。最后,采用時態(tài)邏輯公式對待驗(yàn)證系統(tǒng)的安全屬性進(jìn)行規(guī)約,該約束即是系統(tǒng)的目標(biāo)和最終輸出。

圖2 模型的基本結(jié)構(gòu)Fig.2 Basic structure of the model

(1) 形式化建模

形式化建模,即采用NuSMV語言元素來描述系統(tǒng)的層級結(jié)構(gòu)、功能邏輯關(guān)系和故障模式,為每個子系統(tǒng)建立正常模塊和故障模塊。

建立正常模塊時,先通過VAR代碼聲明內(nèi)部變量的狀態(tài)。可以通過多種方式進(jìn)行表達(dá),如布爾型、整數(shù)型和枚舉型。可同時聲明內(nèi)部變量的狀態(tài)和輸出參數(shù),例如: status:{work, fail}, export_parameter:0..10;然后通過ASSIGN代碼聲明初始狀態(tài)和轉(zhuǎn)移關(guān)系。初始狀態(tài)用init代碼表示,下一狀態(tài)用next代碼表示。子系統(tǒng)的下一狀態(tài)往往取決于某些特定的系統(tǒng)條件,可以通過一組條件語句代碼case&esac來表達(dá)變量(狀態(tài))關(guān)系。

建立故障模塊時,由于大多數(shù)的關(guān)聯(lián)內(nèi)容已經(jīng)在正常模塊中進(jìn)行了聲明,因此采用DEFINE代碼直接定義子系統(tǒng)的各類故障模式,如卡死、反轉(zhuǎn)、阻塞、斷路和短路等,并要聲明每種故障模式造成的相應(yīng)局部后果。

(2) 模型擴(kuò)展

耦合模塊綜合了正常模塊和故障模塊,通過NuSMV代碼定義子系統(tǒng)內(nèi)各個變量(狀態(tài))之間的關(guān)系,為前2個模塊之間建立聯(lián)系。耦合模塊的核心作用在于判定子系統(tǒng)的最終狀態(tài)和輸出變量是否遵循正常模塊或故障模塊的規(guī)范,并將該子系統(tǒng)的內(nèi)部變量值輸出到系統(tǒng)內(nèi)作為其他子系統(tǒng)的輸入。耦合模塊不需要再將具體的變量重復(fù)表出,可以直接用相應(yīng)的正常模塊或故障模塊的狀態(tài)和輸出來表出。表1歸納總結(jié)了系統(tǒng)模型與NuSMV語言之間的元素映射關(guān)系。

表1 系統(tǒng)模型和NuSMV語言之間的元素映射關(guān)系

(3) 安全屬性規(guī)約

一個完整的NuSMV模型還應(yīng)包括整個系統(tǒng)的最終目標(biāo),或是要實(shí)現(xiàn)某種特定的功能需求,或是要保證系統(tǒng)處于安全狀態(tài)。符號模型檢查器(symbolic model verifier,SMV)語言用時態(tài)邏輯公式來描述待驗(yàn)證系統(tǒng)的功能需求和安全屬性。常用的時態(tài)邏輯包括計算樹邏輯(computation tree logic, CTL)和線性時態(tài)邏輯(linear temporal logic, LTL)。

本文以CTL為代表來討論一些具體的規(guī)約細(xì)節(jié)。計算樹是將指定的Kripke關(guān)系結(jié)構(gòu)的初始狀態(tài)作為根,將Kripke結(jié)構(gòu)展開所形成的一個具有無限結(jié)構(gòu)的樹,它由路徑量詞和時態(tài)運(yùn)算符組成。路徑量詞包括E(存在一條路徑)和A(對于所有路徑而言);時態(tài)運(yùn)算符包括G (全部)、F(最終)、X(下一個)和U(直到)。

經(jīng)過組合之后,產(chǎn)生8種最主要的運(yùn)算符,分別是EX、AX、EG、AG、EF、AF和EU、AU。計算樹邏輯定義的規(guī)范都是以布爾代數(shù)的形式表出。3種最常用的組合運(yùn)算符的語義如下:

①EXp為真,表示存在一條路徑使得當(dāng)狀態(tài)s轉(zhuǎn)移到狀態(tài)s′時,p在狀態(tài)s′時是成立的,該組合運(yùn)算符通常用于表述系統(tǒng)的存在特性;

②AGp為真,表示對于所有路徑而言,系統(tǒng)狀態(tài)從s轉(zhuǎn)移到s1,從s1轉(zhuǎn)移到s2……p在每個狀態(tài)si下始終為真,該組合運(yùn)算符常用于表述系統(tǒng)的不變特性;

③AFp為真,表示對于所有路徑而言,系統(tǒng)狀態(tài)從s轉(zhuǎn)移到s1,從s1轉(zhuǎn)移到s2…從sn-1轉(zhuǎn)移到sn,p在狀態(tài)sn下是成立的,該組合運(yùn)算符常用于表述從初始狀態(tài)出發(fā)總能進(jìn)入到使得p為真的狀態(tài)。

2.3 模型檢查

最后,通過模型檢查,NuSMV將會自動地驗(yàn)證所構(gòu)建的系統(tǒng)模型是否滿足規(guī)定的CTL規(guī)范。如果不滿足則會給出反例執(zhí)行序列來示意其中的故障傳播路徑。通過提取反例序列中變化的狀態(tài)量,可以確定導(dǎo)致不期望事件發(fā)生的故障事件組合,即為故障樹的一個割集。

此外,NuSMV還能夠自動生成系統(tǒng)的可達(dá)狀態(tài)集,包括系統(tǒng)可以達(dá)到的所有正常、降級或故障狀態(tài)及基本事件的狀態(tài)。根據(jù)更加詳細(xì)的系統(tǒng)安全屬性和要求對可達(dá)狀態(tài)集進(jìn)行統(tǒng)計篩選和條件剔除,得到可用狀態(tài)集。基于此便可獲得導(dǎo)致不期望事件發(fā)生的所有故障組合,通過分析各故障事件之間的邏輯關(guān)系,得到最小故障組合(即為最小割集),進(jìn)而可以很容易地構(gòu)建出完整的故障樹。在此基礎(chǔ)上,便可進(jìn)行一系列后續(xù)的定性和定量安全性分析。

3 案例應(yīng)用

3.1 案例分析

前主槳舵機(jī)是飛行控制系統(tǒng)的執(zhí)行機(jī)構(gòu),接受來自電傳控制計算機(jī)的指令,進(jìn)行相應(yīng)的動作,拉動傾斜器前傾或后傾,以實(shí)現(xiàn)對飛機(jī)的俯仰控制。前主槳舵機(jī)系統(tǒng)的功能框圖如圖3所示。

圖3 前主槳舵機(jī)系統(tǒng)的功能框圖Fig.3 Function block diagram of the actuator system

舵機(jī)采用旋轉(zhuǎn)式直接驅(qū)動閥作為伺服放大部件。正常工作時,旋轉(zhuǎn)直接驅(qū)動閥控制作動筒運(yùn)動,使用壓力傳感器以實(shí)現(xiàn)過載告警。舵機(jī)主要由以下幾部分組成:液壓控制級1(hydraulic control system,HY-CS1)、液壓控制級2(hydraulic control system,HY-CS2)、電氣部件(electrical parts,EP)、飛控計算機(jī)(flight control computer,FLCC)、傳感器-閥(sensor-valve， S-Valve)、旋轉(zhuǎn)直接驅(qū)動閥(rotary direct drive valve,RDDV)、傳感器-筒(sensor-cylinder，S-Cylinder)和作動筒組件(actuator assembly,ACT)。

在編寫NuSMV模型代碼的過程中,假定FLCC及兩個傳感器不發(fā)生故障。由于FLCC的高穩(wěn)定性和傳感器的可替換性,所以該假設(shè)不會影響結(jié)果的正確性。通過對系統(tǒng)內(nèi)各組件之間的功能交互關(guān)系進(jìn)行初步分析,得到主要功能組件的輸入、輸出和故障模式,如表2所示。

表2 前主槳舵機(jī)系統(tǒng)的主要功能組件清單

根據(jù)系統(tǒng)內(nèi)的功能交互關(guān)系將前主槳舵機(jī)系統(tǒng)按照主要功能部件劃分為8個模塊,以RDDV為例,其相互關(guān)聯(lián)的子模塊代碼分別如下:

? 正常模塊代碼

MODULE RDDV_normal_type

(EP_status, HY-CS1_export_ hydraulicoil,

HY-CS2_export_ hydraulicoil, S-Valve_export_signal)

VAR

status:{work,fail};

export_hydraulicoil:{0,1};

ASSIGN

init(status):=work;

next(status):=case

EP_status=work &

(HY-CS1_export_hydraulicoil=1|

HY-CS2_export_hydraulicoil=1)

& S-Valve_export_signal=1:{work,fail};

TRUE:fail;

esac;

next(export_hydraulicoil):=case

status=work:1;

status=fail:0;

esac;

? 故障模塊代碼

MODULE RDDV_stuck_closed_type

(EP_status,HY-CS1_export_ hydraulicoil,

HY-CS2_export_ hydraulicoil,S-Valve_export_signal)

DEFINE

status:=fail;

export_hydraulicoil:=0;

為了實(shí)現(xiàn)對飛機(jī)的俯仰控制,將系統(tǒng)的最終目標(biāo)概括為ACT輸出伸縮運(yùn)動,因此,相應(yīng)的系統(tǒng)需求用時態(tài)邏輯公式表示為

構(gòu)建完前主槳舵機(jī)系統(tǒng)模型之后,采用NuSMV進(jìn)行自動的模型檢查,輸入指令“NuSMV > check_ctlspec”之后,得到的安全性分析結(jié)果如下,“specification AG ACT.status!=fail is false”表明ACT的狀態(tài)不可能一直保持正常,即存在故障傳播路徑。

NuSMV > read_model

-i C:UsersChenluDesktopsteering_gear.smv

NuSMV > go

NuSMV > check_ctlspec

--specification AG ACT.status!=fail is false

因此,NuSMV給出了一個反例以展示其中的一種故障傳播路徑,即通過仿真序列來演示系統(tǒng)是如何一步一步發(fā)生故障的。從反例State 1中可知:當(dāng)HY-CS1和HY-CS2及電氣故障發(fā)生時,將導(dǎo)致RDDV故障,最終導(dǎo)致ACT狀態(tài)異常,ACT.ACT_normal. status=fail。

--as demonstrated by the following execution sequence

Trace Description: CTL Counterexample

Trace Type: Counterexample

-------State 1------

HY-CS1.Failure_Mode=clog_closed

HY-CS1.HY-CS1_normal.status=work

HY-CS1.HY-CS1_normal.export_hydraulicoil=1

HY-CS2.Failure_Mode=clog_closed

HY-CS2.HY-CS2_normal.status=work

HY-CS2.HY-CS2_normal.export_hydraulicoil=1

EP. Failure_Mode=stuck_closed

EP.EP_normal.status=fail

FLCC.status=work

FLCC.export_signal_valve=1

FLCC.export_signal_cylinder=1

S-Valve.status=work

S-Valve.export_signal_valve=1

RDDV. Failure_Mode=stuck_closed

RDDV.RDDV_normal.status=fail

RDDV.RDDV_normal.export_hydraulicoil=1

S-Cylinder.status=work

S-Cylinder.export_signal_cylinder=1

ACT.Failure_Mode=stuck_closed

ACT.ACT_normal.status=fail

在NuSMV中對模型進(jìn)行檢查,可生成前主槳舵機(jī)系統(tǒng)的可達(dá)狀態(tài)集合,共16 384個(214),包含系統(tǒng)可以達(dá)到的所有正常、降級或故障狀態(tài)及各個基本事件的狀態(tài)或參量。

根據(jù)系統(tǒng)邏輯和實(shí)際情況對可達(dá)狀態(tài)集進(jìn)行篩選,將不會導(dǎo)致故障的事件進(jìn)行剔除,得到可用狀態(tài)集,對其進(jìn)行如下處理和統(tǒng)計:將“輸出液壓油”0至n的狀態(tài)數(shù)組簡化并界定為“故障”和“正常”兩類;對冗余事件“液壓控制級故障”進(jìn)行標(biāo)記與合并,只統(tǒng)計冗余事件均發(fā)生故障并導(dǎo)致頂事件發(fā)生時的可達(dá)狀態(tài);用單點(diǎn)故障對同層次其余事件進(jìn)行吸收簡化。據(jù)此,確定出前主槳舵機(jī)系統(tǒng)故障(即ACT不能輸出伸縮運(yùn)動)的4個最小割集為

{EP.stuck_closed}

{RDDV.stuck_closed}

{ACT. stuck_closed}

{HY-CS1.clog_closed,HY-CS2.clog_closed}.

最后,確定邏輯門的連接。冗余事件HY-CS1和HY-CS2同時故障才會導(dǎo)致頂事件發(fā)生,故{HY-CS1.clog_closed}和{HY-CS2. clog_closed}之間采用“與門”連接;單點(diǎn)故障事件EP、RDDV及ACT任一發(fā)生故障,均會直接導(dǎo)致頂事件發(fā)生,故{EP.stuck_closed}、{RDDV.stuck_closed}、{ACT. stuck_closed}之間采用“或門”連接。最終得到故障樹如圖4所示。

圖4 前主槳舵機(jī)系統(tǒng)的故障樹Fig.4 Fault tree of the actuator system

3.2 結(jié)果討論

第3.1節(jié)案例應(yīng)用表明本文所提出的建模方法的可行性,另一方面也反映出該方法具有以下優(yōu)點(diǎn):

(1) 直接針對系統(tǒng)的功能結(jié)構(gòu),綜合考慮正常和故障狀態(tài)構(gòu)建統(tǒng)一的形式化模型,在保證模型準(zhǔn)確性的前提下很大程度地降低了建模的工作量,不僅簡單實(shí)用,而且避免了模型之間的混淆。

(2) 該方法面向模型檢查,構(gòu)建的模型符合檢查規(guī)范,從而省略模型轉(zhuǎn)換過程,最大限度地減少了模型轉(zhuǎn)換可能造成的信息損失,使得所構(gòu)建的模型更加接近真實(shí)系統(tǒng),進(jìn)一步降低了建模工作量,提高分析結(jié)果的準(zhǔn)確性。

(3) 從系統(tǒng)的故障模式及故障傳播角度進(jìn)行建模,更利于模型檢查過程識別出關(guān)鍵事件和事故序列,有助于安全性分析工作的開展。

(4) 選用已得到普遍應(yīng)用的開源符號模型檢查工具NuSMV作為建模載體,能夠?qū)崿F(xiàn)自動化的模型檢查過程,通過遍歷系統(tǒng)狀態(tài)空間來驗(yàn)證系統(tǒng)的設(shè)計是否滿足規(guī)定的安全性要求。

4 結(jié) 論

針對現(xiàn)有MBSA框架中的建模及轉(zhuǎn)換過程效率低、易造成信息損失的問題,本文面向模型檢查,提出了基于NuSMV構(gòu)建統(tǒng)一系統(tǒng)模型的建模方法,包含建模準(zhǔn)備、統(tǒng)一系統(tǒng)模型的建立、模型檢查3個階段。

面向模型檢查的NuSMV統(tǒng)一建模方法從研究形式化符號語言元素與系統(tǒng)功能、結(jié)構(gòu)和部件故障模式之間的分配與映射關(guān)系入手,提出了將正常模塊和故障模塊進(jìn)行耦合、構(gòu)建形式化系統(tǒng)模型的統(tǒng)一建模方法,可直接利用模型檢查工具對模型進(jìn)行分析處理,驗(yàn)證系統(tǒng)模型是否滿足規(guī)定的安全屬性和要求,得到故障傳播路徑以及故障樹等安全性分析結(jié)果。該方法避免了模型轉(zhuǎn)換可能帶來的信息損失,具有快速、高效、準(zhǔn)確等優(yōu)點(diǎn)。

本文主要對面向模型檢查的NuSMV統(tǒng)一建模方法進(jìn)行了研究,下一步的研究重點(diǎn)將集中于基于模型檢查的定性和定量的安全性分析,以及對于分析結(jié)果的細(xì)化和精煉。

參考文獻(xiàn)：

[1] SHARVIA S, PAPADOPOULOS Y. Integrating model checking with HiP-HOPS in model-based safety analysis[J]. Reliability Engineering & System Safety, 2015, 135: 64-80.

[2] 趙遠(yuǎn), 焦健, 趙廷弟. 基于危險要素的危險分析技術(shù)[J]. 北京航空航天大學(xué)學(xué)報, 2014，59(11): 1623-1628.

ZHAO Y, JIAO J, ZHAO T D. Hazard analysis technique based on hazard factors[J]. Journal of Beijing University of Aeronautics and Astronautics, 2014，59(11): 1623-1628.

[3] ERICSON C A. 危險分析技術(shù)[M].趙廷弟,焦健,譯.北京: 國防工業(yè)出版社, 2012.

ERICSON C A. Hazard analysis techniques for system safety[M].ZHAO T D, JIAO J, trans.Beijing: National Defend Industry Press, 2012.

[4] FAN J, JIAO J, WU W, et al. A model-checking oriented modeling method for safety critical system[C]∥Proc.of the International Conference on Reliability Systems Engineering,2015:1-6.

[5] CHEN L, JIAO J, FAN J, et al. A fault propagation modeling and analysis method based on model checking[C]∥Proc.of the Annual Reliability and Maintainability Symposium, 2016: 1-7.

[6] WEI Q X, JIAO J, FAN J, et al. An optimized method for generating fault tree from a counter-example[C]∥Proc.of the Annual Reliability and Maintainability Symposium, 2016: 1-7.

[7] 陳磊, 焦健, 趙廷弟. 基于模型的復(fù)雜系統(tǒng)安全分析綜述[J]. 系統(tǒng)工程與電子技術(shù), 2017, 39(6): 1287-1291.

CHEN L, JIAO J, ZHAO T D. Review for model-based safety analysis of complex safety-critical system[J]. Systems Engineering and Electronics, 2017, 39(6): 1287-1291.

[8] LISAGOR O, MCDERMID J A, PUMFREY D J. Towards a practicable process for automated safety analysis[C]∥Proc.of the 16th International Ship and Offshore Structures Conference, 2006: 596-607.

[9] PAPADOPOULOS Y, MCDERMID J A. Hierarchically performed hazard origin and propagation studies[C]∥Proc.of the International Conference on Computer Safety, Reliability and Security, 1999: 139-152.

[10] FENELON P, MCDERMID J A, NICHOLSON M, et al. Towards integrated safety analysis and design[J]. ACM Computing Reviews, 1994, 2(1): 21-32.

[11] JOSHI A, HEIMDAHL M P E. Model-based safety analysis of Simulink models using SCADE design verifier[C]∥Proc.of the International Conference on Computer Safety, Reliability and Security, 2005:122-135.

[12] 楊志斌, 皮磊, 胡凱, 等. 復(fù)雜嵌入式實(shí)時系統(tǒng)體系結(jié)構(gòu)設(shè)計與分析語言:AADL[J]. 軟件學(xué)報, 2010，21(5): 899-915.

YANG Z B, PI L, HU K, et al. AADL: an architecture design and analysis language for complex embedded real-time systems[J]. Journal of Software, 2010，21(5): 899-915.

[13] GRIFFAULT A, RAUZY A. The altaRica formalism for describing concurrent systems[J]. Fundamenta Informaticae, 1999, 40(2-3): 109-124.

[14] POINT G, RAUZY A. Altarica: constraint automata as a description language[J]. Journal Européen des Systèmes Automatisés, 1999, 33(8-9): 1033-1052.

[15] 馬徑梁. 基于形式化模型檢驗(yàn)的飛機(jī)系統(tǒng)演繹式安全分析方法研究[D]. 南京: 南京航空航天大學(xué), 2012.

MA J L. Research on deductive security analysis method of aircraft system based on formal model checking[D]. Nanjing: Nanjing University of Aeronautics & Astronautics, 2012.

[16] LISAGOR O, KELLY T, NIU R. Model-based safety assessment: review of the discipline and its challenges[C]∥Proc.of the 9th IEEE International Conference on Reliability, Maintainability and Safety, 2011: 625-632.

[17] BOZZANO M, VILLAFIORITA A. Improving system reliability via model checking: The FSAP/NuSMV-SA safety analysis platform[C]∥Proc.of the 22nd International Conference on Computer Safety, Reliability and Security, 2003: 49-62.

[18] JOSHI A, MILLER S P, WHALEN M, et al. A proposal for model-based safety analysis[C]∥Proc.of the 24th IEEE Digital Avionics Systems Conference, 2005: 13.

[19] ADELINE R, DARFEUIL P, HUMBERT S, et al. Toward a methodology for the AltaRica modelling of multi-physical systems[C]∥Proc.of the Annual European Conference on Safety and Reliability, 2010.

[20] CAVADA R, CIMATTI R, JOCHIM C A. NuSMV 2.5 User Manual[OL/EB]. [2017-05-06].http:∥nusmv. fbk.eu/NuSMV/userman/v25/ nusmv.pdf.

[21] MCMILLAN K L. Getting started with SMV[J]. Cadence Berkeley Laboratories, 2001, 27(4): 3-25.

[22] 劉超, 吳海橋. 基于NuSMV的系統(tǒng)安全性分析平臺開發(fā)和應(yīng)用[J]. 飛機(jī)設(shè)計, 2013, 33(2): 68-71.

LIU C, WU H Q. Development and application of system safety analysis platform based on NuSMV[J]. Aircraft Design, 2013, 33(2): 68-71.