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

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

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

中圖分類號：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)害呈上升趨勢[1]，因此，需要對軟件進(jìn)行安全性分析[2]，以便識別出安全關(guān)鍵系統(tǒng)的軟件中的危險行為，進(jìn)而可以將危險行為轉(zhuǎn)化為安全性需求[3-4]，對軟件進(jìn)行安全性驗(yàn)證，以確保識別出的危險行為不會發(fā)生。傳統(tǒng)安全性分析技術(shù)是將硬件安全分析方法擴(kuò)展到軟件領(lǐng)域，例如軟件故障樹分析（Software Fault Tree Analysis，SFTA）、軟件失效模式和影響分析（Software Failure Mode and Effects Analysis，SFMEA），是基于傳統(tǒng)鏈?zhǔn)?樹式事故因果模型的安全性分析方法，并且是為過去簡單、松耦合的系統(tǒng)而開發(fā)的，主要集中在故障事件上，而目前與軟件相關(guān)的系統(tǒng)危害是由軟件缺陷、軟件需求錯誤和組成系統(tǒng)的不同組件之間不受控制的交互作用造成的，確保系統(tǒng)的安全運(yùn)行需要充分了解與軟件密切相關(guān)的潛在危險，以便在設(shè)計(jì)中消除它們。

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

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

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

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

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

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

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

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

2?軟件危險行為識別

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

2.1?定義系統(tǒng)級事故與危險

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

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

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

2.3?識別危險行為

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

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

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

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

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

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

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

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

3?致因分析

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

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

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

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

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

3.2?形式化致因分析

構(gòu)建了軟件過程模型后，需要對軟件過程模型進(jìn)行分析。為了減少人工對軟件過程模型的分析過程，本文對軟件過程模型進(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)生對系統(tǒng)的控制信號的軟件控制器集合，SC=（sc1，sc2，…，scn）。

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

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

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

定義2?定義四元組UCA=∑（CA，ST）∧CT→H表示軟件控制路徑∑（CA，ST）以CT的控制類型發(fā)生時是否會對系統(tǒng)產(chǎ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，對帶有過程模型變量的起落架軟件過程模型進(jìn)行形式化分析。其中，定義中的SC表示LGCS的軟件控制器;CA表示軟件控制器中的控制行為，軟件控制器的輸出信息作為軟件的控制行為作用于起落架的內(nèi)部組件，對于LGCS而言，軟件控制器對起落架的控制行為為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)部組件與軟件控制信號的健康信息state={normaly，anormaly};CT表示起落架的四種控制行為類型CT={P，NP，ES，EAT}。

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

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

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

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

為了驗(yàn)證通過STPA方法獲取的軟件安全性需求能夠正確約束軟件的危險行為，本文根據(jù)已有的起落架軟件功能需求設(shè)計(jì)了起落架軟件，采用的是法國愛斯特爾技術(shù)有限公司的安全關(guān)鍵的應(yīng)用開發(fā)環(huán)境（Safty Critical Application Development， SCADE）[14]，一款通過了多個安全關(guān)鍵行業(yè)軟件工程標(biāo)準(zhǔn)認(rèn)證的工具。該工具廣泛應(yīng)用于安全關(guān)鍵領(lǐng)域的軟件建模。SCADE模型結(jié)合了Lustre和Esterel兩種形式化同步語言，以嚴(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ù)，對來自前、左、右起落架的組件狀態(tài)信息進(jìn)行同步，保證對三點(diǎn)式起落架同步控制。同步后的狀態(tài)信息輸入給邏輯控制模塊，邏輯控制模塊根據(jù)狀態(tài)信息執(zhí)行邏輯控制，輸出對起落架組件的控制信號，起落架控制邏輯分為收起落架控制邏輯和放起落架控制邏輯。軟件控制器需要實(shí)時監(jiān)控起落架的狀態(tài)與控制信號之間的約束關(guān)系是否被滿足，并將監(jiān)控的狀態(tài)信息傳遞給飛行座艙，以便飛行員執(zhí)行相應(yīng)操作，整個過程涉及到多方系統(tǒng)的交互，都將影響軟件控制器的執(zhí)行過程，因此需要識別出其中的危險交互場景，保證系統(tǒng)的安全。

4.1.2?安全需求建模

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

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

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

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

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

5結(jié)語

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

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

[1]?黃志球，徐丙鳳，闞雙龍，等. 嵌入式機(jī)載軟件安全性分析標(biāo)準(zhǔn)、方法及工具研究綜述[J]. 軟件學(xué)報， 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]?朱丹江，姚淑珍，譚火彬. 基于場景控制特征的安全性需求分析方法[J]. 北京航空航天大學(xué)學(xué)報， 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.）