支持SPIN驗證的詳細級SFMEA方法研究

劉　暢　李海峰　沈國華　顧　益　劉銀陵

1(中國航空綜合技術研究所　北京 100028)2(南京航空航天大學　江蘇 南京 200016)

?

支持SPIN驗證的詳細級SFMEA方法研究

劉暢1李海峰1沈國華2顧益2劉銀陵2

1(中國航空綜合技術研究所北京 100028)2(南京航空航天大學江蘇 南京 200016)

摘要隨著軟件系統的規模和復雜度不斷增大，以軟件為核心的安全關鍵系統的可靠性和安全性越來越難以保證。軟件失效模式與影響分析SFMEA(Software Failure Modes and Effect Analysis)是軍工業中常用的一種安全分析方法，其依賴人工分析、缺乏形式化語義、無法支持驗證。針對SFMEA方法的不足，提出一種結合SPIN的詳細級SFMEA方法，對軟件失效模式進行形式化建模與分析，并結合模型檢驗工具SPIN進行自動化地模型檢驗和模擬仿真，從而提高軟件系統的安全性和可靠性。該方法驗證了“緩沖區數組下標越界”的這一失效模式，從而說明該方法的有效性。

關鍵詞軟件FMEA失效模式SPIN安全關鍵系統

0引言

當前嵌入式軟件已經普遍運用于航空航天、交通運輸、核電能源等安全關鍵領域。為了提供更為靈活和可靠的服務，嵌入式軟件的規模和復雜性不斷增加。用于安全關鍵領域的嵌入式軟件一旦失效將有可能造成人員傷亡、財產損失等災難性后果，因此，將這類嵌入式軟件稱為安全關鍵軟件[1]。軟件失效模式與影響分析[2]SFMEA方法提出于1979年，是工業界常用的軟件安全性分析方法之一。SFMEA的基本思想是識別軟件中的潛在失效模式；分析這些失效模式產生的原因并評估其對系統的影響；最后提出有效的改進措施以提高軟件系統的安全性和可靠性。然而，傳統的SFMEA方法仍然存在著一些問題和缺陷：傳統方法采用自然語言描述失效信息，缺乏精確語義定義，容易產生二義性，制約了失效知識的存儲和共享；另外，由于主要依靠人工分析，傳統方法分析效率低、工作量大，結果易受分析人員主觀經驗影響，無法保證準確性。

針對上述問題，國內外學者們展開了一系列研究工作。文獻[3]提出了一種基于灰色區間關聯的SFMEA方法,通過計算各失效模式對象同理想評估對象的區間關聯度,對水下機器人智能決策系統軟件失效模式風險進行了定量評估。文獻[4]在可信背景下，從軟硬件FMEA對比和在軟件分析和軟件開發中的作用等方面詳細分析了軟件失效模式和影響分析技術。文獻[5]對基于UML建模軟件的SFMEA方法進行研究,建立了用例圖和活動圖與SFMEA分析要素之間的關系,并提出了一套分析方法。文獻[6]提出了一種基于SFMEA的嵌入式軟件質量控制方法，用以管理和分析實時嵌入式軟件的多種失效模式。

基于上述研究，本文分析了傳統的SFMEA方法，針對該方法的不足，結合模型檢驗工具SPIN，提出結合SPIN的SFMEA方法；關注了詳細級的SFMEA安全性分析方法流程，用形式化的方法實現安全性模型驗證；最后結合某型航空發動機數字控制系統的安全性實例分析，說明了該方法的實用性。

1結合SPIN的詳細級SFMEA方法

1.1模型檢驗工具SPIN

SPIN是一個在有限狀態系統中對于特定的安全屬性進行正確性驗證的工具。它擅長使用類似C語言語法的PROMELA建模語言對并發系統進行建模和分析。軟件的失效模式可以轉換為SPIN能識別的與PROMELA模型相容的驗證屬性。這些屬性可以采用在模型中放置斷言或使用LTL公式進行描述。SPIN工具提供了一個模型檢驗器和一個模擬器。模型檢驗器能通過自動檢驗程序的行為來判斷一個PROMELA模型是否滿足指定的驗證屬性；模擬器則可以通過模擬運行PROMELA模型代碼，從而觀察模型的可見行為[7]。如果某個安全屬性沒有被滿足，那么模型檢驗器將返回一個供驗證人員追蹤查錯的錯誤軌跡，即反例。模型檢驗在SFMEA中的意義：(1) 利用SPIN支持斷言或LTL公式描述傳統SFMEA方法采用自然語言描述失效信息，提高了語義定義的精確性，支持失效知識的存儲和共享。(2) 利用SPIN中的PROMELA模型自動檢驗安全屬性，解決了傳統SFMEA方法中由于人工分析導致的分析效率低、工作量大，結果易受分析人員主觀經驗影響的缺陷。因此，本文采用結合SPIN的詳細級SFMEA方法對軟件失效模式進行形式化建模與分析，從而提高分析的準確性和充分性。

1.2結合SPIN的詳細級SFEMA方法流程

由于詳細級SFMEA的對象是已經編碼實現的模塊或由偽代碼描述的模塊，因此詳細級SFMEA的實施繁瑣且工作量大，對系統中的每個模塊都進行詳細級SFMEA既是不必要的也是不現實的。因此分析人員應當挑選系統中安全關鍵、邏輯復雜、與其它模塊關系緊密的軟件模塊進行分析。圖1給出了基于SPIN的詳細級SFMEA的具體實施過程。

圖1　結合SPIN的詳細級軟件FMEA過程

1.2.1建立目標模塊的PROMELA模型

步驟一選定分析模塊

在詳細級SFMEA過程中，應當首先確定待分析的軟件模塊，有針對性地對相關軟件模塊進行詳細級SFMEA分析以限制模塊的可能危害。通過閱讀軟件系統需求規格說明文檔，軟件概要設計文檔，分析人員將軟件系統分解為子系統和子功能并從中重點確定系統中比較重要、容易發生風險的部分來進行分析。

步驟二C語言程序的PROMELA建模

在詳細級SFMEA過程中,對目標模塊的建模對象多為軟件實現代碼或程序偽代碼,它們和PROMELA語言之間往往存在著許多一一對應的關系，這為轉化為PROMELA模型提供了便利。因此，針對某種特定的程序設計語言，能夠設計一套從程序設計語言到PROMELA模型的轉換方法。根據這套轉換方法，模型分析人員就能夠方便快捷地對程序模塊進行PROMELA建模，以支持后面的分析驗證工作。從C語言到PROMELA的建模包括：基本類型建模、結構體類型建模、枚舉型建模、變量作用域建模、控制語句建模、函數建模建模。

PROMELA出于效率等方面的考慮，不支持指針類型的建模[8]。然而C語言代碼中廣泛使用指針，因此有時必須對指針設法建模。這里論述指針類型建模的不必要性。然而事實上，像PROMELA這樣的模型檢驗器輸入語言要支持指針從理論上就是不可行的。因為模型檢驗需要保證模型狀態的有限性，而指針卻支持模型狀態的動態擴充，因此不可能在PROMELA模型中對指針進行很好地建模。盡管在SPIN4.0版本以后我們可以利用SPIN允許內嵌C語言代碼的功能，使用c_decl、c_code、c_expr等原語緩解對指針進行處理的問題。但是對指針進行轉化的問題從根本上還是需要模型分析人員根據實際情況對源代碼進行人工的轉換來解決。譬如當需要對某結構指針(p)進行建模時，可以用該結構類型的變量(_pt_p)進行建模，然后當需要通過該指針取得結構內容((*p)->x)時，直接通過變量獲取(_pt_p.x)，通過這樣的一系列等價轉換來避開對指針的建模。然而必須指出的是，并非所有的指針類型相關的程序都可以等價轉換為不用指針的版本，因此對某些指針相關的建模驗證可能無法進行。

下面將對C語言的核心模塊——基本類型建模、控制語句建模、函數建模進行簡要介紹。

1) 基本類型建模

C語言中的基本數據類型PROMELA語言中很多都有對應的類型，但是浮點數類型在PROMELA中是不支持的，原因很簡單，因為浮點數的狀態過多，而且不能精確表示，因此不適合作為模型檢驗程序的數據類型。表1給出了一種C語言和PROMELA語言的基本類型對應表。從表中可以發現，最后兩種難以處理的類型一般都被簡化處理為int類型，這樣的做法在很多時候是適當地，但是畢竟改變了原來變量的語義，因此有些時候可能不適用，必須由模型分析人員根據實際情況特殊處理。

表1　C語言和PROMELA語言的基本類型映射表

2) 控制語句

C語言的主要控制語句有if、switch、while、for等，它們分別提供分支判斷和循環等功能。PROMELA語言同樣提供了對應的語法以支持分支和循環的控制能力。建模人員可以使用PROMELA中的if…fi語法對C語言中的if、switch等進行轉換，使用do…od語法對while、for等進行建模，如圖2所示。

圖2　C語言控制語句到PROMELA模型的轉換

3) 函數建模

PROMELA中沒有函數的概念，然而C語言程序中卻充滿了函數調用，因此必須有一種方式將函數建模到PROMELA模型之中。好在PROMELA中有替代函數的語法特征，我們一般可以采用inline過程或者進程調用的方式來建模C語言中的函數調用。例如，對于圖3(a)中的C語言代碼片段，我們可以采用圖3(b)中的inline過程對其進行轉換，也可以像圖3(c)中那樣使用進程來進行轉換。

圖3　C語言函數到PROMELA的轉換

1.2.2通過SPIN驗證模塊的失效模式

步驟三確定軟件模塊的失效模式

變量失效模式表示的是某個變量的值發生錯誤、超出范圍等。變量失效模式可能是由于算法錯誤所導致，也可能是由于外部的異常輸入所導致。表2給出了一些典型的變量失效模式。

表2　典型的變量失效模式

步驟四驗證模塊失效模式

詳細級軟件FMEA過程中的失效模式驗證方法與系統級軟件FMEA相同，而且此時由于PROMELA模型與實際代碼或詳細設計的聯系更為緊密，因此驗證的過程也更為容易。模型分析人員能夠很方便地將安全性分析人員所給的各種變量失效和算法失效等轉化為PROMELA模型中的待驗證屬性，通過SPIN的自動驗證功能判斷某潛在失效模式是否確實可能發生等。

1.2.3結合SPIN分析失效原因和影響

步驟五分析失效原因和影響

SPIN模型檢驗工具在驗證一個安全屬性時，如果驗證過程出現問題，會生成一個反例文件。該反例文件中會記錄一個從系統初始狀態到出現安全屬性驗證失敗狀態的路徑，模型分析人員能夠追蹤該路徑，分析出該安全屬性在系統模型中被違反的原因。將其映射到實際系統需求中，就能得到某一模式發生失效的原因。將其映射到實際系統需求中，就能得到某一模式發生失效的原因。為保證保證失效原因分析充分性，仍需在屏蔽了該失效原因的基礎上繼續分析驗證系統的PROMELA模型，觀察除了該失效原因以外是否仍然存在其他原因會導致同一個軟件失效。

對于每個提取出的軟件失效模式，在查找出了失效原因的基礎上，應當進一步分析其失效影響。

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

步驟六提出改進措施并形成詳細級軟件FMEA工作表

根據上述詳細級軟件FMEA分析過程，分析人員已經找到了目標軟件模塊中的各種潛在失效模式及其對本模塊、其他模塊乃至整個系統的影響。根據結合SPIN的失效原因分析，分析人員已經定位了產生失效的根源，此時應該與設計開發人員一同提出改進措施并修改設計或實現。為了分析工作的完整性，為今后的工作提供依據，最后還應該分別完成詳細級變量FMEA工作表等。

由于此時的改進措施已經非常詳細，此時的改進措施由安全性分析人員來提出已經意義不大，因此詳細級軟件FMEA過程中的改進措施應該主要由軟件開發人員來提出，輔以安全性分析人員的把關。

最后，在結束了與詳細級軟件FMEA的綜合分析后，形成詳細級軟件FMEA工作表。

2發動機數字控制系統實例分析

某型發動機控制系統的數據接收子模塊由兩個部分組成：一個接收數據緩沖區和一個數據接收函數。接收數據緩沖區其實主要就是一個數組，它負責將各通道和上位機發來的數據緩存起來，等待數據接收函數的讀取。數據接收函數則負責從緩沖區中一幀一幀地讀取和解析校驗數據，并把已讀取的數據幀從緩沖區中移除。

模型分析人員根據軟件程序代碼，結合本文介紹的從C語言代碼到PROMELA模型的轉換方法，將這兩個部分分別建模。為了能夠對這些程序模塊進行驗證，模型分析人員還建立了一個環境進程，負責產生各種輸入數據幀。其中數據接收函數的PROMELA模型偽代碼如下：

proctype ReceiveData()

{

g_dRegRead = 0;

if

:: g_dRegLength < DATA_FRAME_LENGTH -> skip;

:: else ->

do

:: if

:: g_dRegister[g_dRegRead] == head_data ->

copy data to g_sRS422Receive[];

if

:: g_sRS422Receive checks right ->

variates = g_sRS422Receive[1…n];

:: else ->

g_dRegRead = g_dRegRead + DATA_FRAME_LENGTH;

fi;

g_dRegRead = g_dRegRead + DATA_FRAME_LENGTH;

if

:: g_dRegLength - g_dRegRead >= DATA_FRAME_LENGTH -> skip;

:: else ->

copy g_dRegister[g_dRegRead…g_dRegRead+n] to g_dRegister[0…n];

g_dRegLength=g_dRegLength-g_dRegRead;

break;

fi;

:: else ->

g_dRegRead++;

if

:: g_dRegLength - g_dRegRead >= DATA_FRAME_LENGTH -> skip;

:: else ->

copy g_dRegister[g_dRegRead…g_dRegRead+n] to g_dRegister[0…n];

g_dRegLength=g_dRegLength-g_dRegRead;

break;

fi;

在結合SPIN的發動機控制系統詳細級FMEA過程中，我們需要對失效模式進行逐一驗證。

本例針對失效模式—緩沖區數組下標越界引用進行驗證。該失效模式不需要模型分析人員將其轉化為PROMELA模型中的驗證元素，因為SPIN會自動檢測所有的數組越界引用問題。通過SPIN的模型檢驗，模型分析人員會發現該失效模式確實可能在該軟件模塊中發生，即這段代碼確實可能產生緩沖區數組越界引用的失效，如下所示：

>spin -a controller.pml

>gcc -DSAFETY -DCOLLAPSE -o controller.exe pan.c

>controller.exe -m100000

pan:1: assertion violated - invalid array index (at depth 18378)

pan: wrote controller.pml.trail

通過SPIN分析失效原因和影響

結合SPIN的詳細級SFMEA過程中，由于PROMELA模型與實際的C語言代碼更為接近，因此模型分析人員能夠更加方便高效地追蹤反例，分析出失效原因。這個過程類似于固定執行路徑的程序單步調式過程，分析人員可以在每一步中觀察系統當前的所有變量的狀態，從而分析出導致軟件存在某個失效模式的原因。

如本例中的“緩沖區數組下標越界”這一失效模式，通過分析人員對反例的追蹤分析，發現導致失效模式的原因是在數據幀校驗失敗的分支中多了一句數組下標向后移動的語句。

詳細級分析過程中的失效影響分析可以借助SPIN的模擬運行方式加以輔助，以提高分析的效率和準確性。如本例中的失效影響，通過對PROMELA模型的模擬運行，模型分析人員可以發現該編碼問題在本模塊中除了會導致數據越界的問題以外，更多的是會導致數據幀丟失的問題，如下所示：

>spin -u2000 receive.pml

產生數據：1, 1, 11, 3, 5, 7, 21, 2/*不能通過校驗的數據幀*/

產生數據：1, 1, 12, 15, 3, 4, 11, 3/*正確的數據幀*/

產生數據：1, 1, 3, 12, 14, 1, 5, 13/*正確的數據幀*/

…

校驗不通過！

接收數據：1, 1, 3, 12, 14, 1, 5, 13/*丟失了第二條數據幀*/

…

spin: indexing g_dRegister[36] - size is 100

在結合SPIN的發動機控制系統詳細級SFMEA過程的最后，安全性分析人員與軟件開發人員一同對各個失效模式提出改進措施，進而修改程序代碼，提高軟件系統的質量[9]。并總結工作，完成各種詳細級SFMEA工作表。部分詳細級變量FMEA工作表如表3所示。

表3　發控系統部分詳細級變量FMEA工作表

從該實例分析可以看出，結合SPIN的詳細級SFMEA方法，利用SPIN工具的模型檢驗和模擬運行功能，輔助進行失效原因和失效影響分析工作，使分析方法在準確性、充分性和自動化程度等方面都比傳統方法有很大提高。

3結語

本文研究分析了傳統的SFMEA方法，針對該方法的不足，

結合模型檢驗工具SPIN，提出了結合SPIN的詳細級SFMEA方法；重點關注詳細級的SFMEA安全性分析方法流程，用形式化的方法實現安全性模型驗證；最后結合實例分析，詳細介紹了本文所提出的方法在實際工程項目中的使用過程，說明了該方法的實用性。

本文的主要工作總結如下：

(1) 在傳統SFMEA方法的基礎上，結合模型檢驗技術，提出了一種結合SPIN的SFMEA方法。該方法實現了自動化的驗證了軟件失效模式，解決了傳統SFMEA依賴人工，缺乏形式化語義以及無法支持驗證的問題。

(2) 本文詳細介紹了結合SPIN的SFMEA流程，以及分析目標的形式化建模方法。給出了使用本文方法進行安全性分析的具體過程，并闡述了模型檢驗與軟件失效模式與影響分析方法相結合的解決方案。

(3) 本文通過結合SPIN的SFMEA方法對某型航空發動機數字控制系統進行了安全性分析實例研究。通過實際工程項目詳細介紹了使用本文方法進行實踐分析的步驟和細節，說明了本文提出的安全性分析方法的實用性。

參考文獻

[1] NASA-STD-8710.13B.Software Safety Standard [S].USA:National Aviation and Space Association,2004.

[2] Reifer J.Software Failure Modes and Effect Analysis[J].IEEE Transaction on Reliability,1979,28(3):247-249.

[3] 史長亭,張汝波.改進SFMEA的AUV風險評估方法[J].哈爾濱工程大學學報,2011,32(3):345-349.

[4] 劉俊麗.可信軟件失效模式和影響分析技術研究[J].電子商務,2014(12):47-48.

[5] Shi H,Wang X.FMEA-Based Control Mechanism for Embedded Control Software[C]//Information Technology,Computer Engineering and Management Sciences(ICM),2011 International Conference on,IEEE.2011:110-112

[6] 王雁濤,王毅,楊鈿.軟件需求分析階段基于UML的SFMEA方法研究[J].艦船電子工程,2013,33(8):119-122.

[7] Ben-Ari M.Principles of the Spin model checker[M].Springer,2008.

[8] 鄭軍,黃志球,徐丙鳳.機載軟件適航認證標準新進展及展望[J].計算機工程與設計,2012,33(1):204-208.

[9] Schr?ter C,Schwoon S.The model-checking kit[R].Applications and Theory of Petri Nets,2003:463-472.

ON DETAILED-LEVEL SFMEA METHOD SUPPORTING SPIN VERIFICATION

Liu Chang1Li Haifeng1Shen Guohua2Gu Yi2Liu Yinling2

1(ChineseAviationCompositeTechnologyResearchInstitute,Beijing100028,China)2(NanjingUniversityofAeronauticsandAstronautics,Nanjing200016,Jiangsu,China)

AbstractWith the increment in scale and complexity of software systems, the reliability and safety of the safety-critical system which taks software as the core are becoming increasingly difficult to guarantee. Software failure mode and effect analysis (SFMEA) is a common safety analysis method in military industries. However, it depends on manual analysis, lacks the formal semantics and does not support verification. In light of the deficiencies of SFMEA, we propose a detailed-level SFMEA method which combines SPIN to carry out formalised modelling and analysis on software failure mode. Moreover, in combination with model verification tool SPIN it makes automatic model verification and simulation so as to improve the security and reliability of software system. The method validates the failure mode of “out of bound of array subscripts in buffer zone”, therefore explains the effectiveness of the method.

KeywordsSoftware FMEAFailure modeSimple Promela Interpreter (SPIN)Safety-critical system

收稿日期：2014-12-08。國家自然科學基金項目(61272083)。劉暢，高工，主研領域：軟件安全性工程，軟件工程，需求驗證。李海峰，高工。沈國華，副教授。顧益，碩士。劉銀陵，碩士。

中圖分類號TP311

文獻標識碼A

DOI:10.3969/j.issn.1000-386x.2016.05.070