王鵬 吳康 閻芳 汪克念 張嘯晨

摘 要：現(xiàn)代安全關(guān)鍵系統(tǒng)的功能實(shí)現(xiàn)越來越依賴于軟件，這導(dǎo)致軟件的安全性對(duì)系統(tǒng)安全至關(guān)重要，而軟件的復(fù)雜性使得采用傳統(tǒng)安全性分析方法很難捕獲組件交互過程帶來的危險(xiǎn)。為保證安全關(guān)鍵系統(tǒng)的安全性，提出一種基于系統(tǒng)理論過程分析（STPA）的軟件安全性驗(yàn)證方法。在安全控制結(jié)構(gòu)基礎(chǔ)上，通過構(gòu)建帶有軟件過程模型變量的過程模型，細(xì)化分析危險(xiǎn)行為發(fā)生的系統(tǒng)上下文信息，并以此生成軟件安全性需求。然后通過設(shè)計(jì)起落架控制系統(tǒng)軟件，采用模型檢驗(yàn)技術(shù)對(duì)軟件進(jìn)行安全性驗(yàn)證。結(jié)果表明，所提方法能夠在系統(tǒng)級(jí)層面有效識(shí)別出軟件中潛在的危險(xiǎn)控制路徑，并可以減少對(duì)人工分析的依賴。

關(guān)鍵詞：系統(tǒng)理論過程分析方法;軟件安全;形式化;模型檢驗(yàn);起落架控制軟件

中圖分類號(hào)：TP311.5;V247

文獻(xiàn)標(biāo)志碼：A

Security verification method of safety critical software

based on system theoretic process analysis

WANG Peng1，2，3*， WU Kang1，3， YAN Fang1，2， WANG Kenian1，2， ZHANG Xiaochen1，2

1.Key Laboratory of Airworthiness Certification Technology for Civil Aviation Aircraft， Tianjin 300300， China;

2.College of Airworthiness， Civil Aviation University of China， Tianjin 300300， China;

3.College of Electronic Information and Automation， Civil Aviation University of China， Tianjin 300300， China

Abstract：

Functional implementation of modern safety critical systems is increasingly dependent on software. As a result， software security is very important to system security， and the complexity of software makes it difficult to capture the dangers of component interactions by traditional security analysis methods. In order to ensure the security of safety critical systems， a software security verification method based on System Theoretic Process Analysis （STPA） was proposed. On the basis of the security control structure， by constructing the process model with software process model variables， the system context information of dangerous behavior occurrence was specified and analyzed， and the software security requirements were generated. Then， through the landing gear control system software design， the software security verification was carried out by the model checking technology. The results show that the proposed method can effectively identify the potential dangerous control paths in the software at the system level and reduce the dependence on manual analysis.

Key words：

System Theoretic Process Analysis （STPA） method; software safety; formalization; model checking; landing gear control software

0?引言

現(xiàn)代安全關(guān)鍵電子系統(tǒng)由電子機(jī)械密集型向軟件密集型轉(zhuǎn)變，軟件在實(shí)現(xiàn)安全關(guān)鍵功能、控制和消除危害方面發(fā)揮著越來越重要的作用。近年來，安全關(guān)鍵領(lǐng)域因軟件故障造成的人員傷亡、財(cái)產(chǎn)損失等重大災(zāi)害呈上升趨勢(shì)[1]，因此，需要對(duì)軟件進(jìn)行安全性分析[2]，以便識(shí)別出安全關(guān)鍵系統(tǒng)的軟件中的危險(xiǎn)行為，進(jìn)而可以將危險(xiǎn)行為轉(zhuǎn)化為安全性需求[3-4]，對(duì)軟件進(jìn)行安全性驗(yàn)證，以確保識(shí)別出的危險(xiǎn)行為不會(huì)發(fā)生。傳統(tǒng)安全性分析技術(shù)是將硬件安全分析方法擴(kuò)展到軟件領(lǐng)域，例如軟件故障樹分析（Software Fault Tree Analysis，SFTA）、軟件失效模式和影響分析（Software Failure Mode and Effects Analysis，SFMEA），是基于傳統(tǒng)鏈?zhǔn)?樹式事故因果模型的安全性分析方法，并且是為過去簡(jiǎn)單、松耦合的系統(tǒng)而開發(fā)的，主要集中在故障事件上，而目前與軟件相關(guān)的系統(tǒng)危害是由軟件缺陷、軟件需求錯(cuò)誤和組成系統(tǒng)的不同組件之間不受控制的交互作用造成的，確保系統(tǒng)的安全運(yùn)行需要充分了解與軟件密切相關(guān)的潛在危險(xiǎn)，以便在設(shè)計(jì)中消除它們。

針對(duì)傳統(tǒng)安全性分析方法的不足，Leverson等[5]提出了基于系統(tǒng)理論事故模型和過程（Systems Theoretic Accident Model and Processes， STAMP）的安全性分析方法——系統(tǒng)理論過程分析（System Theoretic Process Analysis， STPA）[6-7]，它將事故的潛在原因擴(kuò)展為動(dòng)態(tài)控制問題，而不是簡(jiǎn)單的部件失效問題。在此基礎(chǔ)上，Thomas[8]提出了一種基于控制結(jié)構(gòu)圖中各控制器的過程模型變量組合的STPA擴(kuò)展方法，用于識(shí)別系統(tǒng)中存在的危險(xiǎn)行為。Abdulkhaleq等[9]研究了使用STPA在系統(tǒng)級(jí)分析軟件安全性的可行性，并成功應(yīng)用于汽車巡航控制系統(tǒng)的軟件安全性分析中。

但是STPA的分析過程依賴分析人員的經(jīng)驗(yàn)，容易對(duì)結(jié)果的完整性和客觀性造成影響。形式化方法[10]采用嚴(yán)謹(jǐn)?shù)恼Z(yǔ)義，描述STPA分析過程，并且可以運(yùn)用數(shù)學(xué)方法對(duì)軟件的安全性進(jìn)行驗(yàn)證。

因此，本文在保證充分識(shí)別軟件中的危險(xiǎn)行為基礎(chǔ)上，考慮減少對(duì)人工的依賴，提出一種基于STPA的安全關(guān)鍵系統(tǒng)的軟件安全性驗(yàn)證方法。該方法以安全控制結(jié)構(gòu)為基礎(chǔ)，分析得到危險(xiǎn)行為，通過構(gòu)建軟件過程模型，確定危險(xiǎn)行為的過程模型變量組合，根據(jù)形式化定義的分析過程，生成危險(xiǎn)行為發(fā)生的系統(tǒng)上下文信息及安全性需求，結(jié)合模型檢驗(yàn)技術(shù)[11]，完成對(duì)軟件的安全性驗(yàn)證。本文以起落架控制系統(tǒng)為案例，根據(jù)功能需求設(shè)計(jì)了起落架控制系統(tǒng)軟件[12]，采用STPA方法提取出軟件安全性需求，借助模型檢驗(yàn)工具對(duì)軟件進(jìn)行安全性驗(yàn)證，驗(yàn)證結(jié)果表明了該方法的可行性，并降低人工分析所可能引入錯(cuò)誤的概率。

1?軟件安全性驗(yàn)證方法總體架構(gòu)

為了保證安全關(guān)鍵系統(tǒng)的安全，對(duì)軟件進(jìn)行安全性分析時(shí)，不能只從軟件本身出發(fā)，必須從系統(tǒng)角度對(duì)軟件進(jìn)行分析，考慮軟件使用過程中軟件與其他組件之間的交互作用，分析軟件可能的工作時(shí)序、使用條件、邏輯缺陷對(duì)系統(tǒng)造成的不利影響，基于此，本文提出了一種基于STPA的軟件安全性驗(yàn)證方法。以前三點(diǎn)式收放起落架控制系統(tǒng)（Langding Gear Control System，LGCS）軟件為對(duì)象進(jìn)行安全性驗(yàn)證。驗(yàn)證框架如圖1所示。驗(yàn)證過程主要分為3個(gè)步驟：

步驟1?軟件危險(xiǎn)行為識(shí)別。從系統(tǒng)規(guī)范出發(fā)，確定LGCS軟件失效可能導(dǎo)致的系統(tǒng)級(jí)事故與危險(xiǎn)，構(gòu)建軟件安全控制結(jié)構(gòu)，識(shí)別軟件中的危險(xiǎn)行為。

步驟2?致因分析。基于已確定的潛在危險(xiǎn)行為，結(jié)合構(gòu)建的軟件過程模型進(jìn)行進(jìn)一步細(xì)化分析，確定每個(gè)潛在危險(xiǎn)行為是如何發(fā)生的，并轉(zhuǎn)化為相應(yīng)的軟件安全性需求。

步驟3?軟件安全性驗(yàn)證。軟件必須根據(jù)已確定的安全需求進(jìn)行驗(yàn)證，以確保潛在的危險(xiǎn)行為不會(huì)發(fā)生，采用形式化的建模方法對(duì)軟件的功能需求和安全需求分別進(jìn)行建模，借助模型檢驗(yàn)工具，完成對(duì)軟件的安全性驗(yàn)證。

2?軟件危險(xiǎn)行為識(shí)別

確保系統(tǒng)的安全運(yùn)行需要充分識(shí)別出軟件中的潛在危險(xiǎn)行為，以便在軟件設(shè)計(jì)中消除它們。

2.1?定義系統(tǒng)級(jí)事故與危險(xiǎn)

在STPA方法中，需要對(duì)所有控制行為所可能引發(fā)的系統(tǒng)級(jí)事故進(jìn)行定義，并分析得到導(dǎo)致事故發(fā)生的相關(guān)系統(tǒng)危險(xiǎn)。軟件中的不恰當(dāng)控制行為是導(dǎo)致系統(tǒng)事故發(fā)生的重要原因，對(duì)軟件的安全性分析需要首先定義與軟件中的控制行為相關(guān)的系統(tǒng)級(jí)事故。由于起落架引起的事故主要集中在飛機(jī)的起飛和降落過程中，因此，本文定義安全性分析場(chǎng)景為飛機(jī)的起飛和降落過程。在此場(chǎng)景下，與LGCS的軟件控制器相關(guān)的系統(tǒng)級(jí)事故為：飛機(jī)不能正常降落（A1）、飛機(jī)不能正常起飛（A2）。根據(jù)系統(tǒng)級(jí)事故分析得到的危險(xiǎn)包括：起落架未鎖定（H1）、起落架異常收起（H2）、起落架未放下（H3）。系統(tǒng)級(jí)事故及危險(xiǎn)映射關(guān)系如表1所示。

2.2?構(gòu)建安全控制結(jié)構(gòu)

在確定系統(tǒng)級(jí)事故與危險(xiǎn)后，需要分析軟件中可能存在的導(dǎo)致軟件在某種致因場(chǎng)景下對(duì)系統(tǒng)進(jìn)行了危險(xiǎn)控制的危險(xiǎn)行為，致使系統(tǒng)級(jí)事故的發(fā)生。STPA方法中通過構(gòu)建安全控制結(jié)構(gòu)，分析各組件之間的交互關(guān)系，進(jìn)而得到危險(xiǎn)控制行為。本文對(duì)起落架系統(tǒng)工作原理和軟件的功能進(jìn)行分析，構(gòu)建了圖2所示的安全控制結(jié)構(gòu)圖，包含了LGCS軟件控制器、起落架動(dòng)作機(jī)構(gòu)、液壓系統(tǒng)、飛行座艙系統(tǒng)。軟件控制器作為人與物理設(shè)備之間的交互樞紐，通過接收飛行員指令和飛行狀態(tài)信息，產(chǎn)生對(duì)系統(tǒng)的控制信號(hào)，分布在系統(tǒng)關(guān)鍵部位的傳感器會(huì)反饋系統(tǒng)狀態(tài)信息給軟件控制器，軟件控制器處理后傳遞給飛行座艙，告知飛行員當(dāng)前起落架系統(tǒng)狀態(tài)， 形成了一個(gè)包含控制路徑和反饋路徑的閉環(huán)安全控制結(jié)構(gòu)。

2.3?識(shí)別危險(xiǎn)行為

根據(jù)安全控制結(jié)構(gòu)能夠識(shí)別出軟件中可能存在的危險(xiǎn)行為，而軟件中潛在的危險(xiǎn)行為有可能只有在某些場(chǎng)景下才會(huì)導(dǎo)致系統(tǒng)危險(xiǎn)，根據(jù)軟件安全性要求，均應(yīng)被視為潛在危險(xiǎn)行為，故作出如下假設(shè)：

假設(shè)1?飛行員的操作過程無危險(xiǎn)性錯(cuò)誤，且正確處理了系統(tǒng)提示信息，只要軟件提供錯(cuò)誤信息就會(huì)導(dǎo)致系統(tǒng)級(jí)事故發(fā)生。

假設(shè)2?由于是對(duì)軟件的安全性分析，假設(shè)其他機(jī)械輔助控制方式失效，且來自其他系統(tǒng)和傳感器組件的信息均正常，軟件一旦出現(xiàn)危險(xiǎn)行為將會(huì)導(dǎo)致系統(tǒng)級(jí)事故發(fā)生。

根據(jù)STAMP理論，將安全性問題當(dāng)作系統(tǒng)控制問題，系統(tǒng)危險(xiǎn)發(fā)生是由于對(duì)系統(tǒng)的不恰當(dāng)控制造成的。軟件通過產(chǎn)生不恰當(dāng)?shù)目刂菩盘?hào)導(dǎo)致系統(tǒng)危險(xiǎn)。Abdulkhaleq等[13]將STPA方法中的危險(xiǎn)行為類型衍生為四種：沒有提供控制信號(hào)、提供控制信號(hào)、控制信號(hào)錯(cuò)誤執(zhí)行時(shí)間、控制信號(hào)錯(cuò)誤作用時(shí)間。本文以放下起落架控制信號(hào)作為控制行為為例進(jìn)行說明，給出識(shí)別出的軟件中存在的危險(xiǎn)行為，所得結(jié)果如下所示。

沒有提供導(dǎo)致危險(xiǎn)（UCA1）?LGCS控制器沒有提供放下起落架控制信號(hào)（H3）。

提供導(dǎo)致危險(xiǎn)（UCA2）?LGCS控制器提供放下起落架控制信號(hào)，導(dǎo)致起落架解鎖（H1、H2）。

錯(cuò)誤執(zhí)行時(shí)間導(dǎo)致危險(xiǎn)（UCA3）?LGCS控制器在起落架艙門打開之前提供放下起落架控制信號(hào)（H3）。

錯(cuò)誤作用時(shí)間導(dǎo)致危險(xiǎn)（UCA4）?LGCS控制器一直提供放下起落架控制信號(hào)，導(dǎo)致起落架無法被鎖定（H1、H2）。

3?致因分析

上述已經(jīng)識(shí)別出了軟件控制器可能發(fā)生的危險(xiǎn)行為，通過構(gòu)建軟件過程模型可以進(jìn)一步分析軟件危險(xiǎn)行為在軟件控制器中是如何發(fā)生的，得到包含LGCS的軟件過程模型變量的軟件危險(xiǎn)控制路徑，轉(zhuǎn)化為相應(yīng)的軟件安全性需求。在STPA中，該過程通常依賴人工分析完成，容易受到人為因素的影響。因此，本文結(jié)合形式化方法，對(duì)軟件過程模型的分析過程進(jìn)行了定義，規(guī)范了分析過程，分析結(jié)果將根據(jù)定義生成。

3.1?構(gòu)建軟件過程模型

識(shí)別軟件過程中產(chǎn)生的影響控制行為安全性的變量，并將它們包含在控制結(jié)構(gòu)圖的軟件控制器中，以記錄每個(gè)危險(xiǎn)行為是如何發(fā)生的，構(gòu)建了如圖3所示的包含軟件過程模型變量的軟件過程模型。

過程模型包含三種類型的變量（信息）：軟件控制器接收系統(tǒng)外部控制器信息、軟件控制器接收系統(tǒng)內(nèi)部組件信息、軟件控制器的輸出信息。

這些過程模型變量可以用來細(xì)化分析每一個(gè)可能發(fā)生的危險(xiǎn)控制行為的上下文信息及其控制路徑，并轉(zhuǎn)化為相應(yīng)的安全約束。

3.2?形式化致因分析

構(gòu)建了軟件過程模型后，需要對(duì)軟件過程模型進(jìn)行分析。為了減少人工對(duì)軟件過程模型的分析過程，本文對(duì)軟件過程模型進(jìn)行了形式化定義，通過定義四元組形式化描述軟件控制器在系統(tǒng)上下文信息下產(chǎn)生了某種類型的控制行為所導(dǎo)致的結(jié)果。四元組定義如下：

定義1?定義四元組（SC、CA、CT、ST）表示軟件控制器（SC） 在系統(tǒng)狀態(tài)下（ST）產(chǎn)生某種控制類型（CT） 的控制行為（CA）。其中：

SC表示能夠產(chǎn)生對(duì)系統(tǒng)的控制信號(hào)的軟件控制器集合，SC=（sc1，sc2，…，scn）。

CT代表控制行為類型集合，且CT={P，NP，ES，EAT}。其中P表示提供控制信號(hào);NP表示沒有提供控制信號(hào);ES表示控制信號(hào)錯(cuò)誤的時(shí)序;EAT表示控制信號(hào)錯(cuò)誤的作用時(shí)間。

CA表示軟件控制器產(chǎn)生的對(duì)被控對(duì)象的控制行為集合，且CA={ca1，ca2，…，can}。

ST表示控制行為發(fā)生時(shí)系統(tǒng)上下文信息集合，ST={st1，st2，…，stn}。

定義2?定義四元組UCA=∑（CA，ST）∧CT→H表示軟件控制路徑∑（CA，ST）以CT的控制類型發(fā)生時(shí)是否會(huì)對(duì)系統(tǒng)產(chǎn)生危險(xiǎn)，其中∑（CA，ST）和CT滿足∑（CA，ST）×CT=∑ i，j（CA，ST）i·CTj，i為（CA，ST）可能的取值數(shù)，UCA∈U，U=∑ i，j（CA，ST）i·CTj→H，H∈Hazards，Hazards={Yes，No}。

結(jié)合上述形式化定義1和定義2，對(duì)帶有過程模型變量的起落架軟件過程模型進(jìn)行形式化分析。其中，定義中的SC表示LGCS的軟件控制器;CA表示軟件控制器中的控制行為，軟件控制器的輸出信息作為軟件的控制行為作用于起落架的內(nèi)部組件，對(duì)于LGCS而言，軟件控制器對(duì)起落架的控制行為為extend_EV和retract_EV。影響這些控制行為安全的系統(tǒng)上下文信息ST包含收放手柄的狀態(tài)信息handle={up，down}、飛機(jī)當(dāng)前的飛行狀態(tài)信息flight={take_off，landing}以及監(jiān)控系統(tǒng)內(nèi)部組件與軟件控制信號(hào)的健康信息state={normaly，anormaly};CT表示起落架的四種控制行為類型CT={P，NP，ES，EAT}。

為充分分析危險(xiǎn)行為發(fā)生的上下文信息，為每個(gè)危險(xiǎn)控制行為確定過程模型變量及其可能的組合。每個(gè)組合都將在四個(gè)控制行為類型中進(jìn)行評(píng)估，以確定控制行為在系統(tǒng)上下文信息中是否是危險(xiǎn)。在系統(tǒng)上下文信息中，如果某種控制類型的控制行為發(fā)生導(dǎo)致系統(tǒng)危險(xiǎn)，那么控制行為將被認(rèn)為是危險(xiǎn)的，然后分析導(dǎo)致每個(gè)危險(xiǎn)行為的潛在危險(xiǎn)場(chǎng)景及控制路徑。本文是對(duì)軟件設(shè)計(jì)模型進(jìn)行安全性驗(yàn)證需要通過安全需求檢測(cè)出模型中的危險(xiǎn)的狀態(tài)變遷，因此本文通過線性時(shí)序邏輯（Linear Temporal Logic， LTL）公式描述危險(xiǎn)控制路徑和相應(yīng)的安全性需求，對(duì)軟件設(shè)計(jì)模型的時(shí)態(tài)邏輯進(jìn)行驗(yàn)證。本文以收放手柄處于拉下位置，軟件控制器產(chǎn)生extend_EV信號(hào)為例進(jìn)行說明，通過文中給出的定義1可以確定LGCS的軟件控制器中與之對(duì)應(yīng)的關(guān)鍵變量，

表3中顯示了控制器產(chǎn)生entend_EV信號(hào)，在系統(tǒng)上下文信息ST所包含的關(guān)鍵過程模型變量可能的取值組合下，針對(duì)不同控制類型CT是否會(huì)對(duì)系統(tǒng)產(chǎn)生危險(xiǎn)，由于以handle=down為例進(jìn)行說明，表中確定了4種不安全的場(chǎng)景，并組合得到16個(gè)可能的結(jié)果。參照定義2，可通過LTL公式描述表3中所給出的軟件控制路徑及其對(duì)系統(tǒng)所產(chǎn)生的結(jié)果，首先可確定定義2中的i取值為4，采用LTL中的邏輯符號(hào)“∧”描述CA、ST、CT下的過程模型變量之間的關(guān)系;采用“→”符號(hào)表明控制行為到控制結(jié)果的遷移關(guān)系;采用“□”時(shí)間符號(hào)表示控制信號(hào)一直被提供。

表4為CT=P，UCA1的危險(xiǎn)路徑及其對(duì)應(yīng)的軟件安全性需求。安全性需求包含了軟件中關(guān)鍵的過程模型變量組合，能夠?qū)浖械奈ｋU(xiǎn)行為進(jìn)行約束。

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

為了驗(yàn)證通過STPA方法獲取的軟件安全性需求能夠正確約束軟件的危險(xiǎn)行為，本文根據(jù)已有的起落架軟件功能需求設(shè)計(jì)了起落架軟件，采用的是法國(guó)愛斯特爾技術(shù)有限公司的安全關(guān)鍵的應(yīng)用開發(fā)環(huán)境（Safty Critical Application Development， SCADE）[14]，一款通過了多個(gè)安全關(guān)鍵行業(yè)軟件工程標(biāo)準(zhǔn)認(rèn)證的工具。該工具廣泛應(yīng)用于安全關(guān)鍵領(lǐng)域的軟件建模。SCADE模型結(jié)合了Lustre和Esterel兩種形式化同步語(yǔ)言，以嚴(yán)格的數(shù)學(xué)理論保證設(shè)計(jì)的完整性和無二義性，集成的KCG代碼生成器能夠保證模型和代碼的一致性，已被廣泛應(yīng)用于反應(yīng)式系統(tǒng)的開發(fā)。

4.1?SCADE建模

4.1.1?起落架控制系統(tǒng)軟件建模

根據(jù)LGCS軟件的功能需求設(shè)計(jì)了如圖4所示的軟件控制器。LGCS軟件控制器接收傳感器的數(shù)據(jù)，對(duì)來自前、左、右起落架的組件狀態(tài)信息進(jìn)行同步，保證對(duì)三點(diǎn)式起落架同步控制。同步后的狀態(tài)信息輸入給邏輯控制模塊，邏輯控制模塊根據(jù)狀態(tài)信息執(zhí)行邏輯控制，輸出對(duì)起落架組件的控制信號(hào)，起落架控制邏輯分為收起落架控制邏輯和放起落架控制邏輯。軟件控制器需要實(shí)時(shí)監(jiān)控起落架的狀態(tài)與控制信號(hào)之間的約束關(guān)系是否被滿足，并將監(jiān)控的狀態(tài)信息傳遞給飛行座艙，以便飛行員執(zhí)行相應(yīng)操作，整個(gè)過程涉及到多方系統(tǒng)的交互，都將影響軟件控制器的執(zhí)行過程，因此需要識(shí)別出其中的危險(xiǎn)交互場(chǎng)景，保證系統(tǒng)的安全。

4.1.2?安全需求建模

對(duì)于已經(jīng)構(gòu)建完成并通過功能測(cè)試的起落架軟件設(shè)計(jì)模型，需要在安全關(guān)鍵的應(yīng)用開發(fā)環(huán)境（Safty Critical Application Development， SCADE）中建立觀察器模型，對(duì)其進(jìn)行安全性驗(yàn)證。觀察器模型根據(jù)已有的安全需求建立，由于SCADE中的邏輯建模符號(hào)與LTL公式語(yǔ)義相同，可直觀地進(jìn)行轉(zhuǎn)換，提高了STPA方法與SCADE建模工具之間的結(jié)合效率，以便實(shí)現(xiàn)對(duì)軟件設(shè)計(jì)模型的安全性驗(yàn)證。本文對(duì)表4中的軟件安全需求進(jìn)行建模，將安全需求轉(zhuǎn)為了SCADE中對(duì)起落架控制軟件的觀察器模型，如圖5所示。

4.2?形式化驗(yàn)證

SCADE的形式化驗(yàn)證中，用戶不需要編寫傳統(tǒng)驗(yàn)證流程中大量的測(cè)試用例和測(cè)試規(guī)程，只需要根據(jù)已有的安全性需求設(shè)計(jì)出安全屬性，通過SCADE對(duì)安全屬性建模，在SCADE中建立形式化驗(yàn)證工程，自動(dòng)化實(shí)現(xiàn)對(duì)設(shè)計(jì)模型的形式化驗(yàn)證，驗(yàn)證框架如圖6所示，分為軟件設(shè)計(jì)模型和觀察器模型。將軟件設(shè)計(jì)模型中的關(guān)鍵變量作為觀察器模型的輸入，對(duì)軟件進(jìn)行約束。同時(shí)，考慮到軟件控制信號(hào)發(fā)出后，硬件返回狀態(tài)信息將會(huì)隨著變化，因?yàn)槭菍?duì)軟件的安全性驗(yàn)證，所以假設(shè)系統(tǒng)硬件均正常，在觀察器模型中需要限定形式化驗(yàn)證過程中的輸入，以便軟件能夠被正常執(zhí)行。

驗(yàn)證環(huán)境為一臺(tái)搭載Intel Xeon E51620 v4的處理器、3.5GHz主頻、8GB內(nèi)存的電腦，在該環(huán)境下運(yùn)行SCADE形式化驗(yàn)證引擎。

驗(yàn)證結(jié)果表明，軟件設(shè)計(jì)中存在不符合安全需求的危險(xiǎn)行為，并檢測(cè)出了潛在的危險(xiǎn)行為UCA1，其中圖7（a）為SSR1.4的驗(yàn)證結(jié)果，說明軟件中存在導(dǎo)致UCA1發(fā)生的危險(xiǎn)路徑RUCA1.4，并且SCADE工具為SSR1.4生成一個(gè)反例，如圖7（b）所示。將反例導(dǎo)入到仿真工程中，通過單步調(diào)試搜索軟件設(shè)計(jì)中的危險(xiǎn)路徑。在此之前本文已經(jīng)分析得到了可能導(dǎo)致UCA1發(fā)生的危險(xiǎn)路徑RUCA1.4，實(shí)現(xiàn)對(duì)危險(xiǎn)行為的原因進(jìn)行定位，可以減少人為分析的工作量。定位后只需分析已給出的導(dǎo)致違反SSR1.4的路徑，反例的仿真結(jié)果如圖7（c）所示，反例總共給出了15個(gè)周期的交互場(chǎng)景，在第13個(gè)周期時(shí)，Res4輸出為false，說明此時(shí)軟件中存在違反SSR1.4的危險(xiǎn)行為，此時(shí)關(guān)鍵變量取值為{extend_EV=open，handle=down，state=anormaly， flight=take_off}，對(duì)比RUCA1.4可知extend_EV信號(hào)出現(xiàn)錯(cuò)誤，有可能導(dǎo)致當(dāng)飛機(jī)處于起飛狀態(tài)并且飛機(jī)未離開地面時(shí)，起落架異常解鎖，導(dǎo)致事故發(fā)生。該系統(tǒng)級(jí)事故發(fā)生是由于提供extend_EV信號(hào)導(dǎo)致的，而該信號(hào)是在一個(gè)交互場(chǎng)景中被異常提供，在進(jìn)行模擬仿真時(shí)很難被發(fā)現(xiàn)，通過本文提供的系統(tǒng)安全性分析方法獲取的安全性需求，結(jié)合模型檢驗(yàn)技術(shù)識(shí)別出了潛在的致因場(chǎng)景導(dǎo)致軟件危險(xiǎn)行為的發(fā)生。根據(jù)發(fā)現(xiàn)的危險(xiǎn)原因修改設(shè)計(jì)后，危險(xiǎn)行為被消除，最終驗(yàn)證通過。

5結(jié)語(yǔ)

本文結(jié)合民機(jī)起落架控制系統(tǒng)的設(shè)計(jì)過程，對(duì)系統(tǒng)安全性分析方法STPA在軟件安全性分析中的應(yīng)用進(jìn)行了研究。通過構(gòu)建軟件過程模型，生成包含軟件過程模型變量的軟件危險(xiǎn)控制路徑和安全性需求，結(jié)合模型檢驗(yàn)工具實(shí)現(xiàn)自動(dòng)的安全性驗(yàn)證。結(jié)果表明：1）STPA安全性分析方法，可以在系統(tǒng)級(jí)識(shí)別出軟件的危險(xiǎn)行為，并推導(dǎo)出相應(yīng)的軟件安全性需求。2）對(duì)軟件過程模型的分析過程進(jìn)行形式化定義，能夠生成包含軟件過程模型變量的軟件危險(xiǎn)控制路徑和相應(yīng)安全性需求。3）結(jié)合模型檢驗(yàn)技術(shù)，能夠自動(dòng)完成對(duì)軟件的安全性驗(yàn)證; 同時(shí)，降低了安全性驗(yàn)證過程中人為因素的影響，提高了分析結(jié)果的可靠性。但依然存在部分人工分析過程，需要進(jìn)一步提高該方法的形式化過程，并開發(fā)相關(guān)工具自動(dòng)化完成分析工作，以及開發(fā)LTL邏輯運(yùn)算符與SCADE模型符號(hào)之間的轉(zhuǎn)換工具，以實(shí)現(xiàn)對(duì)安全關(guān)鍵系統(tǒng)軟件更高自動(dòng)化的安全性驗(yàn)證。

參考文獻(xiàn) （References）

[1]?黃志球，徐丙鳳，闞雙龍，等. 嵌入式機(jī)載軟件安全性分析標(biāo)準(zhǔn)、方法及工具研究綜述[J]. 軟件學(xué)報(bào)， 2014， 25（2）：200-218. （HUANG Z Q， XU B F， KAN S L， et al. Survey on embedded software safety analysis standards， methods and tools for airborne system [J]. Journal of Software， 2014， 25（2）：200-218.）

[2]?DODD I， HABLI I. Safety certification of airborne software： an empirical study[J]. Reliability Engineering and System Safety， 2012， 98（1）：7-23.

[3]?朱丹江，姚淑珍，譚火彬. 基于場(chǎng)景控制特征的安全性需求分析方法[J]. 北京航空航天大學(xué)學(xué)報(bào)， 2016， 42（11）：2358-2370. （ZHU D J， YAO S Z， TAN H B. Safety requirements analysis method based on control characteristics of scenarios[J]. Journal of Beijing University of Aeronautics and Astronautics， 2016， 42（11）：2358-2370.）