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

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

?

支持SPIN驗證的詳細(xì)級SFMEA方法研究

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

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

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

關(guān)鍵詞軟件FMEA失效模式SPIN安全關(guān)鍵系統(tǒng)

0引言

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

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

基于上述研究，本文分析了傳統(tǒng)的SFMEA方法，針對該方法的不足，結(jié)合模型檢驗工具SPIN，提出結(jié)合SPIN的SFMEA方法；關(guān)注了詳細(xì)級的SFMEA安全性分析方法流程，用形式化的方法實現(xiàn)安全性模型驗證；最后結(jié)合某型航空發(fā)動機(jī)數(shù)字控制系統(tǒng)的安全性實例分析，說明了該方法的實用性。

1結(jié)合SPIN的詳細(xì)級SFMEA方法

1.1模型檢驗工具SPIN

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

1.2結(jié)合SPIN的詳細(xì)級SFEMA方法流程

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

圖1　結(jié)合SPIN的詳細(xì)級軟件FMEA過程

1.2.1建立目標(biāo)模塊的PROMELA模型

步驟一選定分析模塊

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

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

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

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

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

1) 基本類型建模

C語言中的基本數(shù)據(jù)類型PROMELA語言中很多都有對應(yīng)的類型，但是浮點數(shù)類型在PROMELA中是不支持的，原因很簡單，因為浮點數(shù)的狀態(tài)過多，而且不能精確表示，因此不適合作為模型檢驗程序的數(shù)據(jù)類型。表1給出了一種C語言和PROMELA語言的基本類型對應(yīng)表。從表中可以發(fā)現(xiàn)，最后兩種難以處理的類型一般都被簡化處理為int類型，這樣的做法在很多時候是適當(dāng)?shù)兀钱吘垢淖兞嗽瓉碜兞康恼Z義，因此有些時候可能不適用，必須由模型分析人員根據(jù)實際情況特殊處理。

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

2) 控制語句

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

圖2　C語言控制語句到PROMELA模型的轉(zhuǎn)換

3) 函數(shù)建模

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

圖3　C語言函數(shù)到PROMELA的轉(zhuǎn)換

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

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

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

表2　典型的變量失效模式

步驟四驗證模塊失效模式

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

1.2.3結(jié)合SPIN分析失效原因和影響

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

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

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

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

步驟六提出改進(jìn)措施并形成詳細(xì)級軟件FMEA工作表

根據(jù)上述詳細(xì)級軟件FMEA分析過程，分析人員已經(jīng)找到了目標(biāo)軟件模塊中的各種潛在失效模式及其對本模塊、其他模塊乃至整個系統(tǒng)的影響。根據(jù)結(jié)合SPIN的失效原因分析，分析人員已經(jīng)定位了產(chǎn)生失效的根源，此時應(yīng)該與設(shè)計開發(fā)人員一同提出改進(jìn)措施并修改設(shè)計或?qū)崿F(xiàn)。為了分析工作的完整性，為今后的工作提供依據(jù)，最后還應(yīng)該分別完成詳細(xì)級變量FMEA工作表等。

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

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

2發(fā)動機(jī)數(shù)字控制系統(tǒng)實例分析

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

模型分析人員根據(jù)軟件程序代碼，結(jié)合本文介紹的從C語言代碼到PROMELA模型的轉(zhuǎn)換方法，將這兩個部分分別建模。為了能夠?qū)@些程序模塊進(jìn)行驗證，模型分析人員還建立了一個環(huán)境進(jìn)程，負(fù)責(zé)產(chǎn)生各種輸入數(shù)據(jù)幀。其中數(shù)據(jù)接收函數(shù)的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;

在結(jié)合SPIN的發(fā)動機(jī)控制系統(tǒng)詳細(xì)級FMEA過程中，我們需要對失效模式進(jìn)行逐一驗證。

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

>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分析失效原因和影響

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

如本例中的“緩沖區(qū)數(shù)組下標(biāo)越界”這一失效模式，通過分析人員對反例的追蹤分析，發(fā)現(xiàn)導(dǎo)致失效模式的原因是在數(shù)據(jù)幀校驗失敗的分支中多了一句數(shù)組下標(biāo)向后移動的語句。

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

>spin -u2000 receive.pml

產(chǎn)生數(shù)據(jù)：1, 1, 11, 3, 5, 7, 21, 2/*不能通過校驗的數(shù)據(jù)幀*/

產(chǎn)生數(shù)據(jù)：1, 1, 12, 15, 3, 4, 11, 3/*正確的數(shù)據(jù)幀*/

產(chǎn)生數(shù)據(jù)：1, 1, 3, 12, 14, 1, 5, 13/*正確的數(shù)據(jù)幀*/

…

校驗不通過！

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

…

spin: indexing g_dRegister[36] - size is 100

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

表3　發(fā)控系統(tǒng)部分詳細(xì)級變量FMEA工作表

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

3結(jié)語

本文研究分析了傳統(tǒng)的SFMEA方法，針對該方法的不足，

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

本文的主要工作總結(jié)如下：

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

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

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

參考文獻(xiàn)

[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] 史長亭,張汝波.改進(jìn)SFMEA的AUV風(fēng)險評估方法[J].哈爾濱工程大學(xué)學(xué)報,2011,32(3):345-349.

[4] 劉俊麗.可信軟件失效模式和影響分析技術(shù)研究[J].電子商務(wù),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ī)載軟件適航認(rèn)證標(biāo)準(zhǔn)新進(jìn)展及展望[J].計算機(jī)工程與設(shè)計,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。國家自然科學(xué)基金項目(61272083)。劉暢，高工，主研領(lǐng)域：軟件安全性工程，軟件工程，需求驗證。李海峰，高工。沈國華，副教授。顧益，碩士。劉銀陵，碩士。

中圖分類號TP311

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

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