顧 益，黃志球

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

基于SPIN的系統(tǒng)級失效模式與影響分析方法研究

顧 益，黃志球

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

為保證關(guān)鍵軟件系統(tǒng)的安全性和可靠性，對軟件失效模式與影響分析方法在實際應(yīng)用中存在的問題進行了分析研究，結(jié)合模型檢驗技術(shù)提出了一種基于SPIN的系統(tǒng)級失效模式與影響分析方法。該方法運用SPIN模型檢驗工具的驗證和模擬功能，有效提高了失效模式分析的準(zhǔn)確性和充分性。此外還結(jié)合某型航空發(fā)動機控制系統(tǒng)介紹了一個應(yīng)用實例，證明了該方法在工程實踐中的可行性。

模型檢驗;SFMEA;SPIN;PROMELA;失效模式

隨著計算機軟硬件系統(tǒng)的日益復(fù)雜，保證軟件系統(tǒng)的安全性和可靠性已成為日益緊迫的問題。在軟件設(shè)計的早期(如需求分析或概要設(shè)計階段)，盡可能多地找到軟件系統(tǒng)的潛在失效模式能極大地降低分析成本，從根本上保證軟件系統(tǒng)的安全性和可靠性。

研究發(fā)現(xiàn)，傳統(tǒng)的安全性分析方法——軟件失效模式與影響分析(Software Failure Modes and Effect Analysis，SFMEA)［1］——在實際應(yīng)用中存在著許多問題。首先，傳統(tǒng)的SFMEA過分依賴分析人員的技能和經(jīng)驗，使得分析效率較低并且分析結(jié)果不夠精確;其次，傳統(tǒng)的SFMEA過程中的失效原因分析依靠分析人員人工完成，無法保證原因分析的正確性和完備性;最后，傳統(tǒng)的SFMEA過程中的失效影響分析同樣依靠分析人員人工完成，無法保證分析結(jié)果的充分性，而且工作量巨大。

SPIN［2］是一款由貝爾實驗室研發(fā)的模型檢驗工具，它使用特定的解釋語言PROMELA對軟件系統(tǒng)進行建模，并在此基礎(chǔ)上對模型的各種安全屬性進行驗證;此外，SPIN還支持對PROMELA模型的模擬運行，以觀察軟件設(shè)計模型的行為。SPIN的這些功能恰好能夠彌補傳統(tǒng)SFMEA方法由于人工分析導(dǎo)致的缺陷，從而提高分析的準(zhǔn)確性和充分性。

因此，本文提出了一種基于SPIN的系統(tǒng)級SFMEA方法，利用SPIN模型檢驗工具的驗證和模擬功能，在傳統(tǒng)SFMEA過程的失效模式提取、失效原因分析、失效影響分析和改進措施的提出等多個步驟中幫助分析工作更加有效地進行。

1 基于SPIN的系統(tǒng)級SFMEA方法

本文針對傳統(tǒng)SFMEA方法精確性低、客觀性差、工作量大等問題，提出了基于SPIN的系統(tǒng)級SFMEA方法。該方法應(yīng)用在軟件開發(fā)的需求分析或概要設(shè)計階段，目的是對軟件體系結(jié)構(gòu)和高級設(shè)計進行安全性評估和分析，在軟件實現(xiàn)之前為改進軟件設(shè)計提供依據(jù)，從而提高軟件系統(tǒng)的安全性和可靠性。

基于SPIN的系統(tǒng)級SFMEA方法除了傳統(tǒng)方法中所需的安全性分析人員以外，還需要模型分析人員的加入。安全性分析人員負(fù)責(zé)提取失效模式、分析失效原因、分析失效影響等工作;模型分析人員則負(fù)責(zé)系統(tǒng)建模、失效模式驗證等工作。兩類人員必須協(xié)同配合，才能成功完成整個安全性分析工作。基于SPIN的系統(tǒng)級SFMEA方法整體流程如圖1所示。

步驟一，熟悉系統(tǒng)需求。

基于SPIN的系統(tǒng)級SFMEA過程的第一步是熟悉系統(tǒng)需求，確定所要分析的目標(biāo)，并設(shè)法對其進行描述。分析人員可以通過閱讀軟件系統(tǒng)需求規(guī)格說明文檔、軟件概要設(shè)計文檔等來了解待分析的軟件對象，然后將軟件系統(tǒng)分解為子系統(tǒng)和子功能，重點確定系統(tǒng)中比較重要、容易發(fā)生風(fēng)險的部分來進行分析。

圖1 基于SPIN的系統(tǒng)級SFMEA流程圖

步驟二，建立系統(tǒng)的PROMELA模型。

軟件需求建模方法是軟件工程中長期研究討論的問題，本文提出的安全性分析方法需要借助SPIN模型檢驗工具進行驗證分析，因此采用PROMELA建模語言對需求進行建模。PROMELA語言本身就非常適合用于對并發(fā)控制系統(tǒng)進行建模，因此使用PROMELA建立的模型可以很好地描述軟件系統(tǒng)需求，為模型分析人員的驗證和分析工作提供基礎(chǔ)。

軟件系統(tǒng)的PROMELA建模當(dāng)前仍然主要依靠人工手動完成，對于不同的軟件系統(tǒng)，具體的建模方法也不盡相同。但是，對于一般的軟件需求，模型分析人員可以從以下4個方面展開建模工作:建立系統(tǒng)各主要進程、建立環(huán)境進程、建立模塊間調(diào)用關(guān)系、抽象未實現(xiàn)的功能模塊。

步驟三，提取功能模塊的失效模式。

安全性分析人員在確定分析目標(biāo)并且構(gòu)建系統(tǒng)層次及依賴關(guān)系模型之后，就可以開始著手提取軟件系統(tǒng)的失效模式，確定目標(biāo)模塊的各種失效，以形成軟件模塊的失效模式列表。

提取軟件失效模式的方式有很多，安全性分析人員一般可以從以下3個方面進行失效模式的提取工作:從通用失效模式集中提取、從特定軟件失效模式庫中提取、針對特定軟件模塊分析提取。

步驟四，通過SPIN驗證系統(tǒng)的失效模式。

模型分析人員不能夠直接針對失效模式進行驗證，因為模型檢驗工具只能識別形式化的驗證屬性，因此當(dāng)模型分析人員得到了安全性分析人員提供的軟件模塊失效模式列表以后，首先必須著手將這些軟件失效逐一轉(zhuǎn)化為SPIN能夠識別的與系統(tǒng)PROMELA模型相容的驗證屬性，如斷言(assertion)、LTL(Linear Temporal Logic)公式［3］等。然后利用SPIN的模型檢驗功能，自動地對各失效模式進行驗證，判斷其是否有可能在系統(tǒng)模型中發(fā)生。更重要的是，如果證明可能發(fā)生失效，SPIN會自動生成一個反例文件，以記錄原因。

步驟五，通過SPIN反例分析失效原因。

SPIN模型檢驗工具在驗證一個安全屬性時，如果驗證過程出現(xiàn)問題，會生成一個反例文件。該反例文件中會記錄一個從系統(tǒng)初始狀態(tài)到出現(xiàn)安全屬性驗證失敗狀態(tài)的路徑，模型分析人員能夠追蹤該路徑，分析出該安全屬性在系統(tǒng)模型中被違反的原因，將其映射到實際系統(tǒng)需求中，就能得到某一模式發(fā)生失效的原因。

然而，當(dāng)模型分析人員找到了導(dǎo)致某個軟件失效的原因之后，仍不能結(jié)束失效原因的分析工作，而應(yīng)該設(shè)法在屏蔽了該失效原因的基礎(chǔ)上繼續(xù)分析驗證系統(tǒng)的PROMELA模型，觀察除了該失效原因以外是否仍然存在其他原因會導(dǎo)致同一個軟件失效，這是保證失效原因分析充分性的必要工作。

步驟六，通過SPIN模擬分析失效影響。

對于每個提取出的軟件失效模式，在查找出了失效原因的基礎(chǔ)上，應(yīng)當(dāng)進一步分析其失效影響。

基于SPIN的SFMEA分析過程中，對失效影響的分析仍然借助于SPIN工具。SPIN除了可以進行模型檢驗以外，還能夠?qū)ROMELA模型進行模擬運行。因此，可以利用SPIN的模擬運行能力，對存在失效模式的PROMELA模型進行模擬運行，其運行結(jié)果會體現(xiàn)模型在這種情況下的表現(xiàn)。將這些表現(xiàn)映射到實際的軟件系統(tǒng)之中，就成為了該失效模式的失效影響。

步驟七，提出改進措施并完成系統(tǒng)級SFMEA工作表。

為了有效地控制軟件失效，分析人員應(yīng)當(dāng)根據(jù)每個軟件失效模式發(fā)生的原因、產(chǎn)生的影響以及嚴(yán)酷度等級，綜合地提出有針對性的改進措施。然后將改進措施同樣建模到系統(tǒng)的PROMELA模型之中，再次進行驗證，以判斷改進措施的有效性。

最后，分析人員還需要填寫系統(tǒng)級SFMEA工作表，以完整地記錄分析的過程和取得的成果。

2 實例分析

某型航空發(fā)動機數(shù)字控制系統(tǒng)負(fù)責(zé)對某型航空發(fā)動機的燃油供油量、風(fēng)扇導(dǎo)葉角度、矢量噴管位移等進行控制。該型航空發(fā)動機數(shù)字控制軟件主要包括系統(tǒng)初始化、信號采集、信號處理、故障診斷與處理、控制邏輯處理、控制算法處理、信號輸出、通訊等功能。本文以某型航空發(fā)動機數(shù)字控制系統(tǒng)為例，通過基于SPIN的系統(tǒng)級SFMEA方法對其進行安全性分析，說明該方法在工程實踐中的可行性。

首先，分析人員通過閱讀需求說明文檔，了解了該型發(fā)動機控制系統(tǒng)(以下簡稱發(fā)控系統(tǒng))的設(shè)計需求，然后針對發(fā)控系統(tǒng)的各個模塊進行PROMELA建模，并合并化簡為一個統(tǒng)一的PROMELA模型。接著對各個模塊及其子模塊展開分析，提取出每個模塊中的失效模式，將這些失效模式轉(zhuǎn)化為系統(tǒng)PROMELA模型中的驗證屬性，并進行驗證。根據(jù)對SPIN產(chǎn)生的反例進行追蹤分析，尋找導(dǎo)致失效的原因，再通過SPIN的模擬來分析失效影響。最后綜合上述分析，對每條失效模式提出相應(yīng)的改進措施，并整理完成系統(tǒng)級SFMEA工作表［4］。

本文僅在此對發(fā)控系統(tǒng)中控制邏輯處理模塊做一個詳細(xì)的舉例分析。

首先，分析人員認(rèn)真理解控制邏輯處理模塊的需求規(guī)約，如其中“假開車控制”過程的需求如下所示:

進入條件:油門桿角度位于慢車域，“假開車信號”和“起動按鈕信號”有效，“起落架放下信號”有效，且“起落架收起信號”無效。

控制過程:

(1)0s開始，輸出“起動機控制信號”，持續(xù)60s后進入停車控制;

(2)0s開始，輸出“起動電磁閥信號”，持續(xù)5s;

(3)整個過程中按“起動供油規(guī)律”輸出主燃油起動供油流量，且“主燃燒室點火信號”無效。

此時，分析人員便能將發(fā)控系統(tǒng)的控制邏輯處理模塊用PROMELA語言進行建模。其中“假開車控制”功能的PROMELA模型如圖2所示。

圖2 假開車控制功能的PROMELA模型

然后，針對該模塊內(nèi)的各個軟件部件展開失效模式分析，列出失效模式列表，見表1。

表1 初步分析所得失效模式列表

接著，將表中的失效模式轉(zhuǎn)化為系統(tǒng)模型中的驗證屬性，代入系統(tǒng)PROMELA模型進行驗證。如第5條“冷運轉(zhuǎn)控制異常被假開車控制打斷”可以用LTL公式“＜＞((g_status==s_cool_run)U(g_status!=s_init)U(g_status==s_dummy_start))＆＆ ＜＞(g_status==s_cool_run)”來表示，其中g(shù)_status是當(dāng)前系統(tǒng)的控制狀態(tài)，s_cool_run、s_init、s_dummy_start分別表示冷運轉(zhuǎn)狀態(tài)、系統(tǒng)初始狀態(tài)和假開車狀態(tài)，這個LTL公式的直接意義是“存在一種情況，使得g_status先為s_cool_run，然后不經(jīng)過g_status為s_init的情況再直接滿足g_status為s_dummy_start的情況”。通過這個LTL公式，SPIN可以驗證其是否可能在系統(tǒng)運行中發(fā)生，反映到實際的軟件系統(tǒng)中也就是冷運轉(zhuǎn)控制是否可能被假開車控制異常打斷。

將這一系列的驗證屬性逐一用SPIN進行驗證，發(fā)現(xiàn)第1條“從起動狀態(tài)進入未知狀態(tài)”這種失效模式不可能發(fā)生，因此可以將其從表格中刪除，而第5條失效模式“冷運轉(zhuǎn)控制異常被假開車控制打斷”卻可能發(fā)生。

接下來針對那些可能發(fā)生的失效模式進行失效原因的分析。譬如第5條“冷運轉(zhuǎn)控制異常被假開車控制打斷”，分析人員根據(jù)SPIN產(chǎn)生的反例文件進行追蹤分析，發(fā)現(xiàn)導(dǎo)致該失效的原因是“冷運轉(zhuǎn)過程中，油門桿被推到了慢車域，并且按下了假開車按鈕，此時系統(tǒng)雖然沒有完成冷運轉(zhuǎn)控制功能，卻一下子進入了假開車控制了”，這是發(fā)動機控制系統(tǒng)需求所不允許的情況。通過SPIN的模擬運行，分析人員發(fā)現(xiàn)該失效模式可能導(dǎo)致整個系統(tǒng)的狀態(tài)遷移異常，使得“冷運轉(zhuǎn)控制”功能始終無法完成。最后，通過對該失效模式失效原因和失效影響的分析，得出第5條失效模式的改進措施為“在假開車控制的進入條件中增加額外限制，還要求在初始條件下才能進入假開車控制”?？偨Y(jié)的部分系統(tǒng)級SFMEA工作表見表2。

表2 發(fā)動機控制系統(tǒng)SFMEA工作表

3 結(jié)束語

基于SPIN的SFMEA方法能夠彌補傳統(tǒng)方法對分析人員過分依賴、精確性低、自動化程度差等問題，然而需要安全性分析人員與模型分析人員協(xié)同合作才能達到最好的效果，因此可以基于本文方法，開發(fā)一個原型系統(tǒng)以規(guī)范整個方法的實施，保證最好的分析效果。

［1］Goddard P L.Software FMEA techniques［C］//Reliability and Maintainability Symposium.［S.l.］:IEEE，2000:138 －144.

［2］Ben－Ari M.Principles of the Spin model checker［M］.［S.l.］:Springer，2008:45 －50.

［3］Vardi M.Branching vs linear time:Final showdown［J］.Tools and Algorithms for the Construction and Analysis of Systems，2001(1):1－22.

［4］鄭軍，胡軍，柯昌博，等.綜合模塊化航電軟件系統(tǒng)測試方法研究綜述［J］.計算機應(yīng)用與軟件，2012，29(5):163－168.

The System Level SFMEA Methodology Based on SPIN

GU Yi，HUANG Zhiqiu
(Nanjing University of Aeronautics and Astronautics，Jiangsu Nanjing，210016，China)

In order to increase the complexity of software systems，it is important to ensure the correctness and reliability of critical software.The traditional software failure modes and effect analysis methodology is lack of accuracy and completeness because of the restrict of the artificial work.Therefore，it presents SPIN based system level SFMEA methodology，which can provide more accuracy and more completeness analysis for the system.It also describes a case study of one aero engine using this mothedology to prove the feasibility of the mothedology.

Model Checking;SFMEA;SPIN;PROMELA;Failure Mode

TP311

A

2095－509X(2013)05－0055－04

10.3969/j.issn.2095 －509X.2013.05.014

2013－01－14

顧益(1987—)，男，江蘇太倉人，南京航空航天大學(xué)碩士研究生，主要研究方向為模型檢驗、軟件安全性分析、軟件形式化方法等。