秦 楠，馬 亮，黃 銳

（海軍潛艇學(xué)院，山東青島 266199）

（?通信作者電子郵箱qinnanqtxy@126.com）

0 引言

隨著計(jì)算機(jī)軟件技術(shù)的發(fā)展，現(xiàn)代復(fù)雜系統(tǒng)逐漸由機(jī)械、電子密集型向軟件密集型轉(zhuǎn)變，與之相關(guān)的軟件安全性問(wèn)題也日益凸顯。大量涉及軟件的系統(tǒng)事故［1］表明，從系統(tǒng)層面探究安全關(guān)鍵系統(tǒng)的安全性問(wèn)題機(jī)理，結(jié)合系統(tǒng)功能自動(dòng)生成軟件安全性需求，并設(shè)計(jì)合理的軟件安全性驗(yàn)證方法已成為迫切需要解決的問(wèn)題［2-4］。目前，安全性分析普遍采用的故障樹(shù)分析（Fault Tree Analysis，F(xiàn)TA）、故障模式影響及危害性分析（Failure Mode and Effects Analysis，F(xiàn)MEA）等傳統(tǒng)分析方法都是基于事件鏈的事故致因模型［5］。這些方法依然從硬件失效的角度看待軟件問(wèn)題，將軟件安全性問(wèn)題局限于軟件自身的不可靠因素，忽略了軟件需求缺陷、系統(tǒng)交互等潛在的深層次原因，難以適用于軟件密集型系統(tǒng)的安全性分析。

為了克服傳統(tǒng)事件鏈致因模型及安全性分析方法的局限性，Leveson［6］在系統(tǒng)論和控制論基礎(chǔ)上，提出新的安全性分析方法——系統(tǒng)理論過(guò)程分析（System Theoretic Process Analysis，STPA）。國(guó)內(nèi)外針對(duì)該方法做了大量研究：文獻(xiàn)［7］提出不安全控制行為的生成算法，實(shí)現(xiàn)了STPA過(guò)程的部分自動(dòng)化；文獻(xiàn)［8］將STPA方法與模型檢測(cè)技術(shù)相結(jié)合，并成功運(yùn)用于汽車巡航控制系統(tǒng)的軟件安全性分析中。國(guó)內(nèi)學(xué)者也在此方向開(kāi)展探索，文獻(xiàn)［5］將STPA 致因分析與形式化方法結(jié)合，借助安全關(guān)鍵的應(yīng)用開(kāi)發(fā)環(huán)境（Safety Critical Application Development，SCADE）工具對(duì)起落架控制系統(tǒng)軟件進(jìn)行形式化驗(yàn)證，降低了分析過(guò)程中人為因素的影響；文獻(xiàn)［9］運(yùn)用STPA 方法對(duì)平交道口控制系統(tǒng)進(jìn)行安全需求分析，借助XSTAMPP 軟件，得到安全需求的形式化表達(dá)；文獻(xiàn)［10］運(yùn)用STPA 方法對(duì)大飛機(jī)的除冰系統(tǒng)進(jìn)行分析，得到軟件安全性設(shè)計(jì)需求，但是結(jié)果為自然語(yǔ)言?，F(xiàn)有研究表明，使用STPA 方法進(jìn)行軟件安全性分析時(shí)仍然面臨著以下挑戰(zhàn)：1）分析得到的安全性需求為自然語(yǔ)言，影響分析結(jié)果的完整性和客觀性；2）分析過(guò)程依賴人工或其他工具，分析效率低；3）缺乏較為完整的需求分析與驗(yàn)證方法。

本文在STPA 技術(shù)基礎(chǔ)上，提出一種集圖形建模、形式建模和形式驗(yàn)證于一體的軟件安全性分析方法，進(jìn)一步提高分析過(guò)程的自動(dòng)化程度。通過(guò)STPA分析得到軟件安全性需求，并自動(dòng)生成安全需求的形式化表達(dá)式；根據(jù)系統(tǒng)控制行為邏輯，構(gòu)建軟件安全控制行為的狀態(tài)圖模型，并將其自動(dòng)轉(zhuǎn)化為形式化模型；借助模型檢驗(yàn)工具完成軟件安全性驗(yàn)證，結(jié)合某武器發(fā)射控制系統(tǒng)實(shí)例驗(yàn)證方法的可行性。

1 軟件安全性需求分析與驗(yàn)證方法框架

為了保證軟件密集型系統(tǒng)的安全性，必須從系統(tǒng)層面查找軟件安全性薄弱環(huán)節(jié)和問(wèn)題機(jī)理，挖掘深層次的軟件安全性問(wèn)題。在傳統(tǒng)STPA分析方法的基礎(chǔ)上，本文提出了一種軟件安全性需求分析與驗(yàn)證方法，以某武器發(fā)射控制系統(tǒng)軟件為研究對(duì)象進(jìn)行安全性驗(yàn)證。方法總體框架如圖1 所示，主要實(shí)施步驟如下：

1）軟件安全性需求分析。根據(jù)整個(gè)系統(tǒng)功能組成，進(jìn)行系統(tǒng)級(jí)事故與危險(xiǎn)分析，并構(gòu)建系統(tǒng)的分層控制結(jié)構(gòu)模型，通過(guò)過(guò)程模型分析，確定潛在的軟件不安全控制行為，進(jìn)一步提煉出軟件安全性需求。

2）軟件安全性需求的形式化規(guī)約。利用算法將分析得到的軟件安全性需求自動(dòng)轉(zhuǎn)化為用線性時(shí)序邏輯語(yǔ)言描述的形式化表達(dá)式。

3）軟件安全控制行為建模。針對(duì)軟件實(shí)現(xiàn)的系統(tǒng)控制功能，對(duì)軟件的安全性控制過(guò)程進(jìn)行抽象，構(gòu)建軟件安全控制行為邏輯的狀態(tài)圖模型，并將其自動(dòng)轉(zhuǎn)化為形式化語(yǔ)言。

4）軟件安全性驗(yàn)證。借助模型檢查工具，采用形式化方法，完成對(duì)軟件安全性屬性的驗(yàn)證。

圖1 基于STPA的軟件安全性需求分析與驗(yàn)證方法框架Fig.1 Framework of software safety requirement analysis and verification method based on STPA

2 軟件安全性分析建模

通過(guò)過(guò)程分析，得到軟件安全性需求，并明確軟件安全性控制行為邏輯，這是進(jìn)行安全性驗(yàn)證的基礎(chǔ)。形式化方法具有語(yǔ)義嚴(yán)謹(jǐn)、數(shù)學(xué)基礎(chǔ)完備的特點(diǎn)［11］，為提高分析結(jié)果的可靠性，本文采用形式化語(yǔ)言對(duì)分析過(guò)程進(jìn)行定義。

2.1 軟件安全性需求分析建模

在系統(tǒng)理論中，系統(tǒng)被視為層次化的控制結(jié)構(gòu)，每層系統(tǒng)通過(guò)對(duì)下層系統(tǒng)施加約束實(shí)現(xiàn)控制［6］。安全控制結(jié)構(gòu)描述了系統(tǒng)各組件之間的交互關(guān)系，定義如下：

定義1安全控制結(jié)構(gòu)。將安全控制結(jié)構(gòu)表示為五元組（CO，CA，AT，SE，CP）。其中：CO={CO1，CO2，…，COi}，代表一個(gè)或多個(gè)控制受控過(guò)程的軟件控制器，某一控制器COi可以表示為二元組COi=（CA，PM），CA是控制行為的集合，PM 是過(guò)程模型；AT是執(zhí)行控制行為的執(zhí)行器，SE是傳感器，負(fù)責(zé)傳遞受控過(guò)程狀態(tài)的反饋信息；CP是由控制器控制的一組受控過(guò)程。

過(guò)程模型是安全控制結(jié)構(gòu)中受控過(guò)程假定狀態(tài)的模型，用于描述變量及變量之間的關(guān)系，以及受控過(guò)程狀態(tài)更改的邏輯。通過(guò)過(guò)程模型分析，可以識(shí)別出不安全控制行為，進(jìn)而得到安全需求。為實(shí)現(xiàn)分析過(guò)程的自動(dòng)化，規(guī)范分析過(guò)程，本文對(duì)過(guò)程模型分析做如下定義。

定義2過(guò)程模型。過(guò)程模型PM 是用于描述受控過(guò)程CP 假定狀態(tài)的模型，主要包含過(guò)程模型變量（Process Model Variable，PMV）及變量間的關(guān)系，當(dāng)前狀態(tài)以及狀態(tài)轉(zhuǎn)移的邏輯。在控制結(jié)構(gòu)圖中，過(guò)程模型通常作為控制器內(nèi)部狀態(tài)的一部分。過(guò)程模型變量是一組影響控制行為CA 安全性的關(guān)鍵變量P 及其狀態(tài)S，其中P=∪(P1=v1，P2=v2，…，Pn=vn)，P1和Pn是控制器COi的過(guò)程模型變量及其值v1和vn。

定義3狀態(tài)組合表。令CAi為控制器COi向執(zhí)行器ATi發(fā)出的控制行為，令PMV=∪(P1，P2，…，Pn)是一組過(guò)程模型變量，每個(gè)過(guò)程模型變量Pi具有Vi個(gè)變量值。每個(gè)過(guò)程模型的狀態(tài)都會(huì)對(duì)安全性造成影響，對(duì)于每一個(gè)控制行為，需要分析其在n 個(gè)過(guò)程模型不同狀態(tài)組合下是否危險(xiǎn)?；谝韵碌仁娇梢陨蛇^(guò)程模型變量的狀態(tài)組合表TSC：

其中：×是笛卡兒乘積運(yùn)算符，i是過(guò)程模型變量，n是過(guò)程模型變量的總數(shù)，狀態(tài)組合表是過(guò)程模型變量值之間的笛卡兒積。在實(shí)際分析中，將通過(guò)算法自動(dòng)生成過(guò)程模型變量的組合集，并對(duì)生成的結(jié)果成對(duì)覆蓋，以最小化組合集的數(shù)量。

定義4 不安全控制行為。通過(guò)上述步驟分析每一個(gè)不安全行為的組合，剔除無(wú)危險(xiǎn)的組合，進(jìn)一步識(shí)別出不安全控制行為（Unsafe Control Action，UCA），用四元組（CA，CS，TSC，CT）表示，CA是不安全控制行為，CS=∪(P1=v1，P2=v2，…，Pn=vn)是CA 的相關(guān)過(guò)程模型變量的一組關(guān)鍵組合，TSC是控制行為CA 是否不安全的狀態(tài)組合信息，CT 是提供控制行為CA 的狀態(tài)組合類型：任何時(shí)間、過(guò)早或過(guò)晚。其中，“過(guò)早”或“過(guò)晚”的具體時(shí)間需要在自動(dòng)生成的基礎(chǔ)上根據(jù)系統(tǒng)具體情況人工修改。例如，在文中某武器發(fā)射控制系統(tǒng)分析案例里，“過(guò)晚”是指解脫制動(dòng)的動(dòng)作時(shí)間必須控制在1.5 s內(nèi)，否則發(fā)射能量已經(jīng)注入，可能出現(xiàn)武器卡管的嚴(yán)重安全性事故，因此，系統(tǒng)判定為“過(guò)晚”。

2.2 軟件安全性控制行為建模

安全性控制行為模型（Safe Control Behavior Model，SCBM）主要包括對(duì)軟件安全性有影響的控制行為、相應(yīng)的安全需求及影響系統(tǒng)狀態(tài)遷移的過(guò)程模型變量。模型結(jié)構(gòu)可以用三元組（PMV，TS，CA）表示。PMV是一組安全關(guān)鍵過(guò)程模型變量；CA是安全控制行為的集合；TS是從安全需求中提取的狀態(tài)轉(zhuǎn)移條件集合，每個(gè)狀態(tài)轉(zhuǎn)移TSi都用語(yǔ)法TS=EV[SR]/TC表示。EV是導(dǎo)致?tīng)顟B(tài)轉(zhuǎn)移TSi的輸入事件，SR是由不安全控制行為得到的相應(yīng)安全性約束條件，它是一個(gè)限制TSi狀態(tài)轉(zhuǎn)移的布爾條件，TC是當(dāng)布爾表達(dá)式有效時(shí)將執(zhí)行的操作。

Simulink Stateflow 是基于有限狀態(tài)機(jī)理論的圖形化建模工具，具有直觀性強(qiáng)、支持仿真等優(yōu)點(diǎn)，已經(jīng)在工業(yè)界得到廣泛應(yīng)用［12］。本文針對(duì)某武器發(fā)射系統(tǒng)功能特點(diǎn)，提出了系統(tǒng)控制行為邏輯模型的概念，并通過(guò)Stateflow實(shí)現(xiàn)了模型的構(gòu)建。在模型中，通過(guò)entry、during和exit等不同類型的操作，可以更改軟件控制器的狀態(tài)，以及相應(yīng)狀態(tài)下的過(guò)程模型變量值。通過(guò)過(guò)程模型變量值對(duì)當(dāng)前的狀態(tài)轉(zhuǎn)移條件進(jìn)行檢驗(yàn)，并確定系統(tǒng)的后續(xù)遷移狀態(tài)。狀態(tài)轉(zhuǎn)移條件由分析得到的安全性需求確定。圖2 說(shuō)明了如何將控制器的內(nèi)部過(guò)程模型變量及其控制行為映射到安全控制行為模型中，具體規(guī)則如下所示：

1）軟件安全性控制行為模型應(yīng)包括軟件控制器所有狀態(tài)下的過(guò)程模型變量：PMV ?SC∈SCBM，SC代表控制器狀態(tài)的集合。

2）狀態(tài)轉(zhuǎn)移條件由不安全控制行為的相應(yīng)安全約束決定。

3）軟件控制器的所有過(guò)程模型變量都必須在模型中進(jìn)行聲明。

4）在模型中定義名為controlAction 的枚舉類型變量，該變量包含軟件控制器的所有控制行為。軟件控制器進(jìn)入當(dāng)前狀態(tài)時(shí)產(chǎn)生的控制行為由controlAction變量提供。

圖2 過(guò)程模型變量及控制行為到安全性控制行為模型的映射規(guī)則Fig.2 Mapping rules of process model variables and control behaviors into safety control behavior model

3 軟件安全性需求驗(yàn)證

3.1 安全性需求的形式化表達(dá)

傳統(tǒng)STPA 分析結(jié)果為自然語(yǔ)言，在解讀中可能存在歧義，同時(shí)，為了使用模型檢查工具進(jìn)行形式化驗(yàn)證，需要將分析得到的安全性需求用形式化語(yǔ)言表示。線性時(shí)序邏輯（Linear Temporal Logic，LTL）是為實(shí)現(xiàn)計(jì)算機(jī)程序形式化驗(yàn)證而提出的一種規(guī)范表示法［13］，已被廣泛用于表達(dá)安全屬性。

若安全需求SRi對(duì)于所有路徑的執(zhí)行結(jié)果都為T(mén)rue，那么它可以用以下LTL公式表示：

式（2）表示當(dāng)系統(tǒng)安全需求為：當(dāng)CS=∪(P1=v1，P2=v2，…，Pn=vn)時(shí)，該系統(tǒng)必須（或不得）提供控制行為CAi?；谝陨隙x，通過(guò)將過(guò)程模型分析得到的不安全狀態(tài)組合的布爾表達(dá)式轉(zhuǎn)換為L(zhǎng)TL表達(dá)式，可以將STPA分析得到的軟件安全需求自動(dòng)轉(zhuǎn)換為形式化規(guī)范語(yǔ)言，實(shí)現(xiàn)轉(zhuǎn)換的算法見(jiàn)文獻(xiàn)［14］。在該方法的基礎(chǔ)上，本文進(jìn)一步提出軟件安全控制行為模型的概念。針對(duì)狀態(tài)圖模型難以直接被模型檢測(cè)工具驗(yàn)證的問(wèn)題，提出一種將軟件安全控制行為模型自動(dòng)轉(zhuǎn)換為形式化模型的方法，借助成熟的模型檢測(cè)工具對(duì)軟件安全需求進(jìn)行形式化驗(yàn)證，進(jìn)一步降低人工分析的影響。

3.2 安全控制行為模型的形式化描述

欲利用模型檢查工具對(duì)經(jīng)過(guò)形式化處理的安全需求和系統(tǒng)安全控制行為模型進(jìn)行驗(yàn)證，需要將狀態(tài)圖模型轉(zhuǎn)換為符號(hào)模型驗(yàn)證工具（Symbolic Model Verifier，SMV）語(yǔ)言描述的形式化模型?？蓴U(kuò)展標(biāo)記語(yǔ)言（Extensible Markup Language，XML）具有規(guī)范統(tǒng)一、互操作性強(qiáng)、可擴(kuò)展等優(yōu)點(diǎn)，為了方便實(shí)現(xiàn)轉(zhuǎn)換，首先將STPA 數(shù)據(jù)模型和Stateflow 數(shù)據(jù)模型分別導(dǎo)出為XML 格式。通過(guò)解析狀態(tài)圖模型的XML，生成安全控制行為模型的樹(shù)形狀態(tài)圖（Transition Tree Diagram，TTD），圖中的每個(gè)節(jié)點(diǎn)代表一種狀態(tài)。

在2.2 節(jié)分析的基礎(chǔ)上，本文提出了將描述系統(tǒng)控制行為邏輯的狀態(tài)圖模型自動(dòng)轉(zhuǎn)換為形式化模型的方法，基本步驟如下，部分算法如算法1所示。

步驟1 將樹(shù)形狀態(tài)圖的根節(jié)點(diǎn)作為輸入，創(chuàng)建SMV 模型的主模塊。

步驟2 將根節(jié)點(diǎn)局部變量的數(shù)據(jù)類型映射到SMV 數(shù)據(jù)類型中，并為每個(gè)子節(jié)點(diǎn)聲明一個(gè)子模塊。

步驟3 用當(dāng)前狀態(tài)節(jié)點(diǎn)的所有變量來(lái)創(chuàng)建子模塊的參數(shù)列表。

步驟4 對(duì)當(dāng)前節(jié)點(diǎn)的狀態(tài)轉(zhuǎn)移進(jìn)行解析，并創(chuàng)建當(dāng)前狀態(tài)節(jié)點(diǎn)與其他狀態(tài)的轉(zhuǎn)移關(guān)系的真值表。

步驟5 把所有模塊生成的SMV 規(guī)范作為字符串保存到堆棧對(duì)象中，并把STPA 數(shù)據(jù)中的LTL 表達(dá)式添加到主模塊末。

算法1 生成SMV模型。

輸入 安全控制行為模型的樹(shù)型結(jié)構(gòu)圖Ttd，STPA 數(shù)據(jù)模型DataModel，樹(shù)型結(jié)構(gòu)圖節(jié)點(diǎn)a。

輸出：SMV模型SMVi。

4 安全性需求分析與驗(yàn)證方法的應(yīng)用

4.1 系統(tǒng)級(jí)分析

某武器發(fā)射控制系統(tǒng)是包括航行器、發(fā)射裝置、發(fā)控設(shè)備、軟件和人員等組成的能完成規(guī)定發(fā)射任務(wù)的綜合體，是一個(gè)集中指揮、綜合控制的復(fù)雜系統(tǒng)［14］。執(zhí)行發(fā)射任務(wù)之前，航行器被固定在發(fā)射管中，“制止”狀態(tài)傳感器接通。下達(dá)發(fā)射指令后，系統(tǒng)檢查準(zhǔn)備完畢，開(kāi)始傳遞發(fā)射信號(hào)，當(dāng)設(shè)備1 綠色狀態(tài)指示燈亮起，信號(hào)傳向設(shè)備2 且該設(shè)備綠色指示燈亮起后，發(fā)射模塊接收信號(hào)并操縱驅(qū)動(dòng)裝置解脫對(duì)航行器的制動(dòng)，使其在發(fā)射能量作用下出管。某武器發(fā)射控制系統(tǒng)的系統(tǒng)級(jí)事故主要包括：對(duì)人員造成嚴(yán)重傷害或死亡（A-1）、裝備損壞（A-2）、無(wú)法完成發(fā)射任務(wù)（A-3），系統(tǒng)級(jí)危險(xiǎn)及其關(guān)聯(lián)的系統(tǒng)級(jí)事故，如表1所示。

表1 某發(fā)射控制系統(tǒng)的系統(tǒng)級(jí)危險(xiǎn)Tab.1 System-level accidents of a launch control system

根據(jù)系統(tǒng)工作流程及相關(guān)組件，建立如圖3 的系統(tǒng)安全控制結(jié)構(gòu)模型，通過(guò)識(shí)別系統(tǒng)控制和交互進(jìn)一步分析潛在的不安全控制行為。

4.2 軟件安全性需求分析

在發(fā)射過(guò)程中，人員操作和發(fā)射控制系統(tǒng)軟件高度交互，控制行為頻繁。本文以系統(tǒng)對(duì)航行器“解脫制動(dòng)”這一典型控制行為例，開(kāi)展軟件安全性需求分析。

圖3 某武器發(fā)射控制系統(tǒng)安全控制結(jié)構(gòu)Fig.3 Safety control structure of a weapon launch control system

STPA 方法將不安全控制行為分為4 類：1）未提供控制導(dǎo)致危險(xiǎn)；2）提供控制導(dǎo)致危險(xiǎn)；3）過(guò)早/過(guò)晚提供控制或者控制順序錯(cuò)誤導(dǎo)致危險(xiǎn)；4）控制行為持續(xù)時(shí)間過(guò)長(zhǎng)或者過(guò)早停止導(dǎo)致危險(xiǎn)。針對(duì)“解脫航行器制動(dòng)”這一控制行為中的四類不安全控制行為逐一進(jìn)行分析評(píng)估，如表2所示。

表2 解脫航行器制動(dòng)的不安全控制行為T(mén)ab.2 Unsafe control behaviors of releasing the aircraft brake

在已有研究［14］基礎(chǔ)上，結(jié)合某武器發(fā)射控制系統(tǒng)實(shí)際，進(jìn)一步完善設(shè)備指示燈狀態(tài)變量，并添加傳感器接收航行器狀態(tài)信號(hào)情況的過(guò)程模型變量，建立如圖4 所示的帶有過(guò)程模型的控制結(jié)構(gòu)。

圖4 帶有過(guò)程模型的控制結(jié)構(gòu)Fig.4 Control structure with process model

解脫制動(dòng)控制行為擁有4個(gè)過(guò)程模型變量：

1）設(shè)備1 指示燈，擁有4 個(gè)狀態(tài)，分別為黃燈、綠燈、紅燈和熄滅狀態(tài)；

2）設(shè)備2 指示燈，擁有4 個(gè)狀態(tài)，分別為黃燈、綠燈、紅燈和熄滅狀態(tài)；

3）制動(dòng)裝置，擁有3 個(gè)狀態(tài)，分別為完全提起、完全落下和中間狀態(tài)（卡滯）。

4）傳感器接收航行器狀態(tài)信號(hào)情況，擁有兩種狀態(tài)，分別是正常和故障。

每個(gè)過(guò)程模型的狀態(tài)都會(huì)對(duì)安全性造成影響，對(duì)于每一個(gè)控制行為，需要分析其在4 個(gè)過(guò)程模型不同狀態(tài)組合下是否危險(xiǎn)。過(guò)程模型變量的狀態(tài)組合總數(shù)理論上為4×4×3×2=96 個(gè)，通過(guò)算法對(duì)生成的結(jié)果成對(duì)覆蓋（Pairwise），以最小化組合數(shù)量；同時(shí)剔除無(wú)危險(xiǎn)的組合，最終得到30 種危險(xiǎn)組合，由此得到30 條用自然語(yǔ)言描述的安全需求。因篇幅限制，生成的部分狀態(tài)組合表如表3所示。

表3 解脫航行器制動(dòng)控制行為的部分狀態(tài)組合示例Tab.3 Some examples of state combinations of releasing the aircraft brake

4.3 軟件安全性驗(yàn)證

通過(guò)分析得到了某武器發(fā)射控制系統(tǒng)的安全需求，但是其結(jié)果為自然語(yǔ)言。為了避免在解讀中存在歧義，影響分析效果，并且為了在下一步工作中使用模型檢查器進(jìn)行形式化驗(yàn)證，用上文中提出的算法將其轉(zhuǎn)換為L(zhǎng)TL表達(dá)式，部分安全需求及相應(yīng)的LTL表達(dá)式如表4所示。

表4 安全需求及相應(yīng)的LTL表達(dá)式示例Tab.4 Examples of safety requirements and the corresponding LTL expressions

其中，SR1.27 表達(dá)式意為在一號(hào)設(shè)備指示燈為綠色、二號(hào)設(shè)備指示燈為紅色，制動(dòng)裝置呈制止?fàn)顟B(tài)且狀態(tài)傳感器工作正常的情況下，不允許提供解脫制動(dòng)動(dòng)作，這與系統(tǒng)安全要求一致。

借助Simulink Stateflow 工具來(lái)描述安全控制結(jié)構(gòu)圖中過(guò)程模型變量之間的關(guān)系以及軟件控制行為對(duì)安全性的影響，如圖5所示。

圖5 軟件安全控制行為的Stateflow模型Fig.5 Stateflow model of software safety control behaviors

將系統(tǒng)安全控制行為模型轉(zhuǎn)換為SMV 語(yǔ)言，并運(yùn)行模型檢查工具NuSMV 對(duì)生成的SMV 文件進(jìn)行驗(yàn)證。NuSMV 是基于二進(jìn)制決策圖的符號(hào)模型驗(yàn)證工具，支持LTL模型檢查，目前已廣泛應(yīng)用于有窮狀態(tài)遷移系統(tǒng)分析［15］。NuSMV 版本為2.6.0，驗(yàn)證過(guò)程耗時(shí)0.6 s。經(jīng)驗(yàn)證，所有的LTL 公式都得到滿足，沒(méi)有產(chǎn)生反例，這是因?yàn)闃?gòu)建的安全控制行為模型是根據(jù)分析得出的軟件安全性需求構(gòu)建的，部分驗(yàn)證結(jié)果如圖6所示。

圖6 NuSMV驗(yàn)證結(jié)果Fig.6 NuSMV verification results

5 結(jié)語(yǔ)

本文研究STPA方法在軟件安全性分析中的應(yīng)用，并結(jié)合某武器發(fā)射控制系統(tǒng)進(jìn)行驗(yàn)證。結(jié)果表明：1）通過(guò)對(duì)軟件安全性需求分析過(guò)程進(jìn)行形式化定義，并將安全性需求自動(dòng)轉(zhuǎn)化為形式化規(guī)范表達(dá)式，可以彌補(bǔ)傳統(tǒng)STPA方法分析結(jié)果為自然語(yǔ)言的缺陷，得到較為完備的軟件安全性需求。2）使用狀態(tài)圖模型對(duì)系統(tǒng)安全控制行為進(jìn)行描述，并將其自動(dòng)轉(zhuǎn)化為形式化模型，能夠?qū)崿F(xiàn)STPA方法的形式化擴(kuò)展。3）運(yùn)用模型檢測(cè)工具對(duì)安全控制行為模型進(jìn)行驗(yàn)證，可以進(jìn)一步實(shí)現(xiàn)分析過(guò)程的自動(dòng)化，提高方法的分析效率。在未來(lái)工作中，將嘗試開(kāi)展針對(duì)安全性的軟件測(cè)試方案的研究，進(jìn)一步提高安全性需求分析與驗(yàn)證的針對(duì)性和可靠性。