苛求軟件可靠性方法、技術(shù)與模型研究

武延華 薛小平 王小平

（同濟(jì)大學(xué)電子與信息工程學(xué)院，201804，上海∥第一作者，碩士研究生）

近年來(lái)，軟件越來(lái)越多被應(yīng)用在安全苛求（Safety－Critical）、任務(wù)苛求（Mission－Critical）等領(lǐng)域，如航空航天、軌道交通、核工業(yè)等。但苛求系統(tǒng)需求增長(zhǎng)在一定程度上超出了構(gòu)建和維護(hù)這類系統(tǒng)的能力發(fā)展，因軟件失效造成關(guān)鍵任務(wù)失敗和生命財(cái)產(chǎn)損失的案例屢有報(bào)道［1－3］，軟件可靠性受到了廣泛關(guān)注。軟件可靠性定義為系統(tǒng)在給定時(shí)間和條件下完成其規(guī)定任務(wù)的能力，當(dāng)系統(tǒng)正常工作時(shí)（即可靠時(shí)）是安全的，即可靠性蘊(yùn)含安全性。為描述方便，本文中提及可靠性時(shí)，同時(shí)也包含了安全性。

軟件開(kāi)發(fā)活動(dòng)極其復(fù)雜，在整個(gè)生命周期中把握軟件可靠性本質(zhì)更為困難。受包括項(xiàng)目預(yù)算、開(kāi)發(fā)周期、團(tuán)隊(duì)管理水平、程序員能力經(jīng)驗(yàn)、商業(yè)軟件模塊、軟件運(yùn)行環(huán)境等在內(nèi)的多種因素影響，容易在不經(jīng)意的情況下引入錯(cuò)誤。

目前，保障軟件可靠性的方法很多，如N版本編程、恢復(fù)塊以及形式化方法等在軟件開(kāi)發(fā)不同階段較為有效地保證了可靠性。本文試圖從瀑布式開(kāi)發(fā)模型的角度，討論苛求系統(tǒng)中的軟件可靠性方法、技術(shù)和模型，包括需求形式化建模、多版本軟件容錯(cuò)、函數(shù)式程序設(shè)計(jì)及可靠度評(píng)估模型。

需求形式化建模雖然可有效提高軟件規(guī)格的質(zhì)量，但非形式化描述與形式化模型間的語(yǔ)義一致性及對(duì)其驗(yàn)證的可行性、可信性等仍是難題。因語(yǔ)義扭曲導(dǎo)致的規(guī)格錯(cuò)誤可能會(huì)帶來(lái)系統(tǒng)失效風(fēng)險(xiǎn)；多版本軟件容錯(cuò)試圖屏蔽設(shè)計(jì)錯(cuò)誤，卻對(duì)由規(guī)格錯(cuò)誤等原因?qū)е碌南到y(tǒng)共因失效（Common－Cause Failure，簡(jiǎn)為CCF）無(wú)能為力；函數(shù)式程序設(shè)計(jì)作為輕量級(jí)形式化實(shí)現(xiàn)技術(shù)，在編寫(xiě)可靠代碼方面有諸多特征和優(yōu)勢(shì)，但并未受到軟件界的廣泛重視；可靠度評(píng)估模型雖然無(wú)法直接改善軟件可靠性，但定量評(píng)估軟件可靠度卻能為可靠性改善提供依據(jù)和指導(dǎo)。

1 需求與規(guī)格形式化方法

目前，苛求系統(tǒng)開(kāi)發(fā)通常采用形式化方法，即通過(guò)數(shù)學(xué)方法對(duì)軟件生命周期中各個(gè)階段的活動(dòng)客體進(jìn)行建模，分析并驗(yàn)證其隱含性質(zhì)，并在開(kāi)發(fā)過(guò)程中采用V＆V（驗(yàn)證與確認(rèn)）方法達(dá)到安全和可靠的目的。文獻(xiàn)［4］指出，廣義的形式化方法可跨越軟件工程的整個(gè)生命周期，各個(gè)階段擁有其獨(dú)特的形式化方法。但狹義上的形式化方法大多特指需求階段的各種規(guī)格說(shuō)明語(yǔ)言（例如Z，VDM（維也納開(kāi)發(fā)方法），Alloy等）和并發(fā)建?？蚣埽ɡ鏑SP（通信順序進(jìn)程）、CCS（通信系統(tǒng)演示）等進(jìn)程代數(shù)）。

需求是軟件開(kāi)發(fā)活動(dòng)的基礎(chǔ)，需求規(guī)格錯(cuò)誤對(duì)可靠性的影響貫穿了整個(gè)軟件生命周期。文獻(xiàn)［5］對(duì)系統(tǒng)集成和測(cè)試階段發(fā)現(xiàn)的387個(gè)軟件錯(cuò)誤進(jìn)行研究后指出，與安全相關(guān)的大多數(shù)軟件錯(cuò)誤都出自不完整的需求規(guī)格或是對(duì)其的誤解，而文獻(xiàn)［6］指出傳統(tǒng)技術(shù)不足以捕捉許多需求錯(cuò)誤。

需求階段本身由多個(gè)活動(dòng)組成，例如需求獲取、需求分析、需求演化等。該階段的形式化方法也有多種。需求工程的形式化也稱早期需求的形式化，可解決需求過(guò)程中的二義性、不一致性、不完整性等，主要針對(duì)極易變動(dòng)的不穩(wěn)定需求進(jìn)行建模和驗(yàn)證。形式化規(guī)格則是等需求穩(wěn)定后，作為整個(gè)需求階段完成后的產(chǎn)出文檔。早期建模和驗(yàn)證活動(dòng)具有很多優(yōu)勢(shì)，如盡早排除需求中的錯(cuò)誤可進(jìn)一步指導(dǎo)完善規(guī)格并減少完整模型建立、驗(yàn)證、演化和維護(hù)的成本，而作為從最初非形式化需求到最終完整規(guī)格的中間過(guò)渡，早期模型為需求工程提供了更細(xì)粒度的可追蹤性等。

文獻(xiàn)［7］給出了形式化方法成功應(yīng)用于任務(wù)苛求系統(tǒng)早期需求建模的3個(gè)案例。由于采用輕量級(jí)形式化方法，這些模型并沒(méi)有完全保證目標(biāo)需求的完整性和正確性，而是通過(guò)盡可能揭示非形式化需求中的錯(cuò)誤來(lái)改善需求質(zhì)量和促進(jìn)可靠性保證等級(jí)。對(duì)早期需求建模，考慮到需求本身的粗略性和易變性，這種決策是合理的。另一方面，文獻(xiàn)［7］對(duì)3個(gè)案例分別采用了標(biāo)注（Annotated）流程圖、與或表（AND/OR table）和目標(biāo)建模技術(shù)（OMT）作為初始需求描述到需求模型轉(zhuǎn)換過(guò)程的中間結(jié)構(gòu)化表示，用以澄清二義性、深化對(duì)需求結(jié)構(gòu)的理解，進(jìn)一步確定采用何種合適的建模表示法，并給出了使用方法。此外，中間結(jié)構(gòu)化表示同樣為早期需求建?；顒?dòng)提供了更明晰的可追蹤性，保持模型與非形式化需求間緊密的同步一致性。

從需求的非形式化描述，到半形式化表示，再到形式化模型，這個(gè)過(guò)程通常采用轉(zhuǎn)換的方法。而轉(zhuǎn)換過(guò)程通常由人手動(dòng)完成，同一份需求的不同語(yǔ)法形式要保持其內(nèi)容之間的語(yǔ)義一致性十分困難。目前主流形式化框架中的B方法和SCADE（安全苛求應(yīng)用開(kāi)發(fā)）環(huán)境提供了完善的工具支持建模、設(shè)計(jì)、實(shí)現(xiàn)、驗(yàn)證一體化的廣譜式（Entire Spectrum）開(kāi)發(fā)方法［8］，即從形式化規(guī)格開(kāi)始，通過(guò)程序精化演算，將抽象模型逐步轉(zhuǎn)換為具體模型，最終生成可編譯執(zhí)行的程序語(yǔ)言代碼。每一步轉(zhuǎn)換都必須進(jìn)行模型驗(yàn)證和精化驗(yàn)證來(lái)保持語(yǔ)義，規(guī)格的形式化保證了該工作的可行性。然而，對(duì)需求模型進(jìn)行類似轉(zhuǎn)換和驗(yàn)證的難度在于，需求總是從非形式化描述開(kāi)始的，若要求將其自動(dòng)轉(zhuǎn)換為形式化模型并進(jìn)行驗(yàn)證，會(huì)涉及自然語(yǔ)言處理，且依賴于特定應(yīng)用領(lǐng)域。

文獻(xiàn)［9－11］基于這種思想，提出基于模板（Template）和模式（Pattern）的方法，將針對(duì)特定應(yīng)用領(lǐng)域模型的公共特征（Property）分段和分句成固定格式的半自然語(yǔ)言描述。需求分析師提取領(lǐng)域問(wèn)題中的參數(shù)并應(yīng)用到模板中就能得到需求規(guī)格實(shí)例，再利用集成自然語(yǔ)言處理的輕量級(jí)形式化方法及其支持工具［12］對(duì)這些規(guī)格實(shí)例進(jìn)行早期分析和驗(yàn)證。從本質(zhì)上看，需求分析對(duì)用戶需求最初總是采用非形式化的表述，非形式化需求和形式化規(guī)格間的語(yǔ)義一致性保證問(wèn)題仍然需要進(jìn)一步研究。

2 多版本軟件容錯(cuò)

基于B方法或者SCADE環(huán)境的苛求系統(tǒng)項(xiàng)目，設(shè)計(jì)僅僅作為規(guī)格到實(shí)際代碼的中間過(guò)渡階段，需求、設(shè)計(jì)和實(shí)現(xiàn)之間的區(qū)分變得模糊，基于嚴(yán)格數(shù)學(xué)定義的模型精化及每一步轉(zhuǎn)換完成的證明責(zé)任（Proof Obligation）確保不會(huì)引入設(shè)計(jì)錯(cuò)誤。但若采用了工具支持薄弱的Z表示法（Notation）或提倡輕量級(jí)形式化的Alloy表示法等建立規(guī)格，設(shè)計(jì)與實(shí)現(xiàn)活動(dòng)仍需開(kāi)發(fā)人員介入完成，容易造成規(guī)格與設(shè)計(jì)間的語(yǔ)義分歧，即導(dǎo)致設(shè)計(jì)錯(cuò)誤。

多版本軟件容錯(cuò)可不完全處理系統(tǒng)中的設(shè)計(jì)錯(cuò)誤，能保證軟件中某些失效不至于引起整個(gè)系統(tǒng)失效。如果說(shuō)形式化方法通過(guò)確定地排除軟件錯(cuò)誤而保證可靠性，多版本軟件容錯(cuò)就是一種不確定的、概率化的錯(cuò)誤屏蔽方法。作為傳統(tǒng)的軟件可靠性提高手段，20世紀(jì)70年代研究人員就提出的N版本編程（N－version Programming，簡(jiǎn)為 NVP）［13］和恢復(fù)塊（Recovery Block，簡(jiǎn)為 RB）［14］成為軟件可靠性開(kāi)發(fā)模式的典型代表。

NVP根據(jù)同一份需求構(gòu)建多份設(shè)計(jì)差異化（Design Diversity）的軟件版本，順序或并發(fā)運(yùn)行，對(duì)各版本輸出采取某種表決算法選出最優(yōu)解。設(shè)計(jì)差異化可降低各版本間因相同設(shè)計(jì)錯(cuò)誤而導(dǎo)致共因失效（CCF）的可能性，即系統(tǒng)不可檢錯(cuò)率。假設(shè)各軟件版本失效相對(duì)獨(dú)立，可靠度為Rm1，Rm2，…，Rmn，表決器采用多數(shù)表決（Majority Voting）且可靠度為Rv，則系統(tǒng)可靠度

RB則將各軟件版本順序運(yùn)行，用各版本對(duì)應(yīng)的接受測(cè)試（Acceptance Tests）代替NVP中表決器的職能，選擇最先通過(guò)接受測(cè)試的輸出為最優(yōu)解。假設(shè)各軟件版本和接受測(cè)試的失效兩兩間均相對(duì)獨(dú)立，前者可靠度為Rm1，Rm2，…，RmN，后者可靠度（包括若檢測(cè)出故障則正確回滾的概率）為Rt1，Rt2，…，RtN，則系統(tǒng)可靠度

由于RB只需一份軟件版本通過(guò)測(cè)試就能得到最優(yōu)解，而NVP要求多份版本正確無(wú)誤才能表決出最優(yōu)解，因此只要接受測(cè)試設(shè)計(jì)得當(dāng)，RB可獲得比NVP更高的系統(tǒng)可靠度。但RB的問(wèn)題在于：接受測(cè)試是依賴于其對(duì)應(yīng)軟件版本內(nèi)部邏輯的，沒(méi)有統(tǒng)一、明確地構(gòu)造簡(jiǎn)單而高可靠接受測(cè)試的普適方法。此外，本質(zhì)上RB要求各版本嚴(yán)格順序執(zhí)行，這導(dǎo)致了潛在的巨大延時(shí)風(fēng)險(xiǎn)。意味著對(duì)實(shí)時(shí)性要求較高的應(yīng)用并不適合，需結(jié)合監(jiān)視定時(shí)器（Watchdog Timer）［15］等機(jī)制予以輔助。

研究人員嘗試通過(guò)NVP和RB的組合來(lái)進(jìn)一步提高可靠性。文獻(xiàn)［16］提出的一致性恢復(fù)塊將NVP與RB串聯(lián)起來(lái)，并復(fù)用軟件版本甚至運(yùn)算結(jié)果；文獻(xiàn)［17］提出的接受表決（Acceptance Voting）將RB中的接受測(cè)試應(yīng)用于NVP中每一版本，使每個(gè)版本輸出只有通過(guò)接受測(cè)試才能參與系統(tǒng)輸出表決。這些方法雖然使系統(tǒng)比使用純NVP或純RB達(dá)到更高的可靠度，但依然存在諸如接受測(cè)試編寫(xiě)困難、潛在延時(shí)風(fēng)險(xiǎn)大的問(wèn)題。

NVP和RB也可采用數(shù)據(jù)差異化［18］實(shí)現(xiàn)某些變種（Variant）。其核心思想是尋求一種或多種數(shù)據(jù)重表達(dá)（Re－expression）算法，將系統(tǒng)輸入轉(zhuǎn)換成語(yǔ)義相同的不同形式，提交給各路冗余軟件。采取數(shù)據(jù)差異化形式的NVP變種稱為N副本（NCopy），其RB變種稱為重試塊（Retry Block）。數(shù)據(jù)差異化存在的問(wèn)題與RB類似，即數(shù)據(jù)重表達(dá)嚴(yán)重依賴于應(yīng)用領(lǐng)域，即便為某一特定應(yīng)用尋求完備、可靠的重表達(dá)算法也是相當(dāng)困難的。

設(shè)計(jì)差異化和數(shù)據(jù)差異化均無(wú)法消除CCF，如需求中遺留的錯(cuò)誤、設(shè)計(jì)人員做出的相同錯(cuò)誤決策、程序員錯(cuò)誤實(shí)現(xiàn)同一個(gè)算法等，都會(huì)為不同軟件版本埋下通向相同失效模式路徑的隱患。因此，CCF的存在使預(yù)測(cè)系統(tǒng)可靠度變得困難，而僅能在測(cè)試和運(yùn)行階段采用CCF模型或軟件可靠性增長(zhǎng)模型（Software Reliability Growth Model，簡(jiǎn)為SRGM）對(duì)其進(jìn)行評(píng)估（Estimation）。但在此之前，通過(guò)刪除和避免程序中的實(shí)現(xiàn)錯(cuò)誤來(lái)改善軟件代碼質(zhì)量，又對(duì)系統(tǒng)可靠性的改善做出一定貢獻(xiàn)。

3 函數(shù)式程序設(shè)計(jì)

函數(shù)式程序設(shè)計(jì)（Functional Programming，簡(jiǎn)為FP）是一種聲明式編程泛型，與軟件形式化方法協(xié)同發(fā)展起來(lái)，兩者共享絕大部分?jǐn)?shù)學(xué)基礎(chǔ)，尤其是FP的理論根基（λ演算）來(lái)自于形式化方法中基于演算的方法。大多數(shù)自動(dòng)定理證明器或輔助證明系統(tǒng)都采用FP語(yǔ)言編寫(xiě)，例如Coq、LCF（可計(jì)算數(shù)邏輯）、HOL（高階邏輯）、Isabelle等。FP把“軟件系統(tǒng)即求值器”的本質(zhì)在語(yǔ)法層面體現(xiàn)出來(lái)，每個(gè)函數(shù)作為最小模塊單元，具有優(yōu)良的數(shù)學(xué)性質(zhì)，即在任何時(shí)候?qū)ν瑯虞斎攵籍a(chǎn)生同樣輸出，沒(méi)有副作用。這種引用透明性既避免了命令式語(yǔ)言中常見(jiàn)的編碼錯(cuò)誤，又使得代碼驗(yàn)證近似于數(shù)學(xué)函數(shù)驗(yàn)證，無(wú)需繁復(fù)冗長(zhǎng)的證明規(guī)則指導(dǎo)。

文獻(xiàn)［19］闡述了FP的重要性，認(rèn)為FP優(yōu)勢(shì)的本質(zhì)在于提供了新的模塊化能力：高階函數(shù)將所執(zhí)行操作從具有共性的應(yīng)用模式中抽象出來(lái)，惰性求值則將某些迭代計(jì)算分離為生成器和篩選器兩個(gè)獨(dú)立模塊的組合。模塊化的軟件系統(tǒng)突顯了代碼本身及對(duì)代碼驗(yàn)證工作的重用性，使程序更易于理解、編寫(xiě)、測(cè)試和維護(hù)，對(duì)其可靠性的改善顯而易見(jiàn)。

3.1 FP應(yīng)用案例

愛(ài)爾蘭都柏林城市大學(xué)軟件工程中心主導(dǎo)開(kāi)發(fā)的SADLI（診斷實(shí)驗(yàn)室圖象安全保證）項(xiàng)目［20］通過(guò)在安全苛求方法學(xué)指導(dǎo)下采用FP實(shí)現(xiàn)診斷顯微鏡中的成像系統(tǒng)，以確定這種開(kāi)發(fā)方法在該領(lǐng)域中的優(yōu)勢(shì)和限制，其中探索了與FP相關(guān)的兩個(gè)方面：一是采用FP語(yǔ)言開(kāi)發(fā)復(fù)雜軟件系統(tǒng)的可能性；二是安全苛求軟件開(kāi)發(fā)過(guò)程中FP語(yǔ)言與傳統(tǒng)安全苛求方法學(xué)中最佳實(shí)踐準(zhǔn)則之間的協(xié)調(diào)一致性。

研究結(jié)果表明，雖然開(kāi)發(fā)該系統(tǒng)需要考慮的實(shí)踐問(wèn)題很多，包括用戶交互、硬件控制、圖像處理、圖像顯示、統(tǒng)計(jì)模式識(shí)別及與現(xiàn)有軟件的接口，F(xiàn)P依然能順利實(shí)現(xiàn)該系統(tǒng)運(yùn)行。這表明采用FP作為關(guān)鍵技術(shù)來(lái)實(shí)現(xiàn)具有相當(dāng)規(guī)模的復(fù)雜系統(tǒng)是切實(shí)可行的。圖1展示了SADLI的生命周期。

圖1 SADLI的生命周期

從圖1中可見(jiàn)該系統(tǒng)規(guī)格也采用了純FP語(yǔ)言Haskell（Gofer為早期Haskell解釋器）來(lái)描述（文獻(xiàn)［21］討論了該做法的可行性），將快速原型開(kāi)發(fā)和形式化方法結(jié)合起來(lái)（從而使得對(duì)設(shè)計(jì)和實(shí)現(xiàn)兩者都能進(jìn)行形式化驗(yàn)證），又使設(shè)計(jì)到實(shí)現(xiàn)的轉(zhuǎn)換在同一種泛型內(nèi)進(jìn)行，從兩方面將轉(zhuǎn)換中可能引入的錯(cuò)誤最少化。項(xiàng)目人員將SADLI基于IEC 61508標(biāo)準(zhǔn)［22］的早期版本進(jìn)行開(kāi)發(fā)，這就證實(shí)了FP與安全苛求系統(tǒng)開(kāi)發(fā)標(biāo)準(zhǔn)間的協(xié)調(diào)一致性。

3.2 領(lǐng)域?qū)Ｓ茫―omain Specific）FP語(yǔ)言

除了通用FP語(yǔ)言在苛求系統(tǒng)中的工業(yè)實(shí)踐外，研究人員更嘗試為苛求系統(tǒng)設(shè)計(jì)領(lǐng)域?qū)Ｓ玫腇P語(yǔ)言。LUSTRE［23］是一種專為實(shí)現(xiàn)反應(yīng)式系統(tǒng)或進(jìn)行硬件描述的同步數(shù)據(jù)流語(yǔ)言，兼并FP模型和并行模型，程序形式化與時(shí)態(tài)邏輯相似，使該語(yǔ)言既能編寫(xiě)代碼又能表達(dá)和驗(yàn)證時(shí)間屬性。LUSTRE作為法國(guó)Esterel公司安全苛求系統(tǒng)開(kāi)發(fā)環(huán)境SCADE的核心語(yǔ)言，在工業(yè)界應(yīng)用已有20年［24］，包括航空航天、軌道交通等領(lǐng)域的控制系統(tǒng)。

Hume［25］是一門(mén)較新的應(yīng)用于安全苛求系統(tǒng)的FP語(yǔ)言，其設(shè)計(jì)者指出圖靈完備語(yǔ)言的程序等價(jià)性（Equivalence）、終止性（Termination）及時(shí)間空間使用情況這些嚴(yán)格屬性都是不可判定的，而能判定這些屬性的語(yǔ)言（如有限狀態(tài)機(jī)）缺乏足夠強(qiáng)的表達(dá)能力。因此Hume的目標(biāo)是既能提供高層的抽象能力和表達(dá)能力，又能保證程序執(zhí)行時(shí)間和空間消耗這類動(dòng)態(tài)行為屬性。這其實(shí)反映了安全苛求系統(tǒng)將強(qiáng)制（Strong）的正確性要求和嚴(yán)格（Strict）的性能要求整合的意圖，而又使語(yǔ)言維持在高層次抽象。

來(lái)自Ericsson公司的Erlang語(yǔ)言［26］是一種現(xiàn)在廣泛應(yīng)用于電信領(lǐng)域的并發(fā)函數(shù)式語(yǔ)言。作為基礎(chǔ)設(shè)施，通信系統(tǒng)需要高可靠地完成所請(qǐng)求任務(wù)，即它們是任務(wù)苛求系統(tǒng)。此外，任何建設(shè)于這些系統(tǒng)之上的安全苛求系統(tǒng)，也使前者帶上了安全苛求的屬性。Erlang作為一種面向并發(fā)的分布式容錯(cuò)語(yǔ)言，最適合處理通信系統(tǒng)的動(dòng)態(tài)性、并發(fā)性和實(shí)時(shí)性，開(kāi)發(fā)出高可靠的分布式并發(fā)系統(tǒng)。

3.3 FP中的軟件容錯(cuò)

多版本軟件容錯(cuò)與語(yǔ)言無(wú)關(guān)，可用FP語(yǔ)言部署NVP和RB。此外，根據(jù)純FP語(yǔ)言引用透明性易于并行計(jì)算的特點(diǎn)，文獻(xiàn)［27］又提出了一種基于并行圖歸約的FP程序容錯(cuò)方法。在惰性求值的純FP程序中，作為表達(dá)式的整個(gè)程序可看作一個(gè)圖，求值過(guò)程意味著對(duì)該圖做歸約。并行體系中各節(jié)點(diǎn)接受該圖的子圖作為計(jì)算任務(wù)，并對(duì)其它節(jié)點(diǎn)的子圖進(jìn)行備份。一旦檢測(cè)到某節(jié)點(diǎn)進(jìn)程出錯(cuò)，則請(qǐng)求有其備份子圖的其它節(jié)點(diǎn)傳回該子圖，并通過(guò)檢查點(diǎn)和消息日志（Message Logging）等機(jī)制將出錯(cuò)節(jié)點(diǎn)回卷到初始狀態(tài)后重新歸約。由于引用透明性形成各子圖相互獨(dú)立，因此，可按任意順序歸約，這就賦予整個(gè)恢復(fù)過(guò)程最少限制和最大自由度。

4 可靠度評(píng)估模型

需求、設(shè)計(jì)和實(shí)現(xiàn)階段的任何可靠性方法和技術(shù)雖然提高了軟件質(zhì)量，卻無(wú)法完全屏蔽或消除軟件錯(cuò)誤，且沒(méi)有提供定量分析并以此為依據(jù)持續(xù)改進(jìn)可靠性。另一方面，通常并不要求苛求系統(tǒng)完全可靠，而是允許其具有既定閾值下的可接受失效率。軟件可靠度評(píng)估模型正是實(shí)現(xiàn)對(duì)系統(tǒng)可靠度進(jìn)行定量估計(jì)的一種統(tǒng)計(jì)方法。

4.1 CCF建模

在NVP和RB中，若假設(shè)各軟件版本失效相互獨(dú)立，則系統(tǒng)可靠度Rsys是組成系統(tǒng)各組件可靠度R1，R2，…，Rn的函數(shù)，即 Rsys＝f（R1，R2，…，Rn），如式（1）、（2）所示。這意味著在系統(tǒng)被真正構(gòu)建出來(lái)之前就可預(yù)測(cè)其可靠度。差異化嘗試使該獨(dú)立性假設(shè)趨于合理，然而Knight等人進(jìn)行的27版本實(shí)驗(yàn)［28］及對(duì)其進(jìn)行的故障分析卻揭示了復(fù)雜軟件開(kāi)發(fā)過(guò)程總會(huì)不經(jīng)意引入相關(guān)故障的事實(shí)，使差異化軟件系統(tǒng)仍會(huì)產(chǎn)生CCF。

4.1.1 CCF模型

CCF模型針對(duì)采用了容錯(cuò)技術(shù)的軟件結(jié)構(gòu)，考察組合軟件組件后引入的系統(tǒng)失效新質(zhì)。最流行的CCF模型是1975年Fleming提出的β因子模型［29］，僅用單個(gè)參數(shù)β描述冗余組件間的失效耦合。通常只能等系統(tǒng)真正構(gòu)建出來(lái)后通過(guò)測(cè)試和運(yùn)行并記錄歷史數(shù)據(jù)來(lái)估計(jì)CCF模型中的參數(shù)，然而β因子模型的簡(jiǎn)單性及其工程實(shí)踐經(jīng)驗(yàn)，使得針對(duì)特定應(yīng)用就能直接確定β值。例如Humphrey方法［30］、部分 （partial）β 因子法［31］和IEC 61508 標(biāo)準(zhǔn)［22］中β因子模型的查表（checklist）法等。

文獻(xiàn)［32］對(duì)其它CCF模型的現(xiàn)狀和趨勢(shì)進(jìn)行了總結(jié)，包括Fleming對(duì)β因子模型擴(kuò)展后提出的多希臘字母（Multiple Greek Letters，簡(jiǎn)為MGL）模型、Mosleh和Siu提出的α因子模型、Vesely提出的二項(xiàng)失效率（Binomial Failure Rate，簡(jiǎn)為BFR）模型等。

（1）MGL模型克服了β因子模型假設(shè)CCF為全部組件失效的局限，加入更多參數(shù)以表征不同數(shù)量組件失效間相關(guān)性的條件概率。

（2）α因子模型根據(jù)由共同原因造成k路組件失效率與系統(tǒng)失效率之間的比值αk為參數(shù)計(jì)算不同形式CCF的概率。

（3）BFR模型將系統(tǒng)組件失效分為獨(dú)立失效和由沖擊引起的任意數(shù)量組件失效。其中沖擊的發(fā)生滿足齊次泊松分布，且當(dāng)沖擊發(fā)生時(shí)每個(gè)組件以概率p失效，則因沖擊導(dǎo)致的失效組件數(shù)滿足二項(xiàng)分布B（n，p）。

國(guó)內(nèi)學(xué)者對(duì)CCF模型也進(jìn)行了廣泛而深入的研究。文獻(xiàn)［33］研究了應(yīng)用貝葉斯網(wǎng)絡(luò)建立CCF系統(tǒng)可靠性模型的方法，將系統(tǒng)中的共因元件分離為具有串聯(lián)關(guān)系的獨(dú)立失效子元件（失效率K1）和共因失效子元件（失效率K2），再分析它們與其它非共因元件的相應(yīng)關(guān)系（如串聯(lián)、并聯(lián)等），并對(duì)典型系統(tǒng)進(jìn)行了可靠性分析。文獻(xiàn)［34］提出的CCF新模型對(duì)假設(shè)失效相互獨(dú)立時(shí)所得的系統(tǒng)可靠度表達(dá)式進(jìn)行變換，加入表征CCF的影響因子，從而將可靠性預(yù)測(cè)與評(píng)估聯(lián)系起來(lái)，能更全面地計(jì)算系統(tǒng)元件之間的相關(guān)性，彌補(bǔ)了傳統(tǒng)CCF模型的信息遺漏問(wèn)題，避免了傳統(tǒng)CCF模型所面臨的組合爆炸問(wèn)題。

4.1.2 差異化模型

CCF模型并沒(méi)有解釋失效間相關(guān)性的產(chǎn)生原因，對(duì)差異化系統(tǒng)的分析造成困難。例如β因子模型假設(shè)各路組件完全相同，這對(duì)差異化系統(tǒng)顯然無(wú)法成立。對(duì)于差異化系統(tǒng)的CCF分析，一種方法是采用傳統(tǒng)CCF模型，在考慮差異化的背景下重新定義和解釋其參數(shù)，例如把β定義為各軟件版本失效率的幾何平均［32］。另一種方法是采用差異化模型［35］來(lái)解釋失效相關(guān)性，包括 Eckhardt－Lee（EL）模型［36］、Littlewood－Miller（LM）模型［37］等。

EL模型認(rèn)為軟件的運(yùn)行環(huán)境實(shí)際是其執(zhí)行時(shí)的輸入，即任何影響軟件行為的狀態(tài)變量。對(duì)所有可能開(kāi)發(fā)出的軟件版本及其輸入x，難度函數(shù)（Difficulty Function）θ（x）表示在該輸入下軟件失效的概率。若θ（x）越大，則表明輸入x的難度越大，多個(gè)軟件版本在該輸入下都失效的概率也越大，導(dǎo)致失效正相關(guān)性。

在EL模型中，設(shè)計(jì)差異化僅僅是選擇不同開(kāi)發(fā)團(tuán)隊(duì)隨機(jī)達(dá)到的，即仍然可能存在相同設(shè)計(jì)。而LM模型是EL模型的推廣，對(duì)不同版本間的設(shè)計(jì)差異進(jìn)行強(qiáng)制（Force），包括選擇不同的開(kāi)發(fā)過(guò)程、程序設(shè)計(jì)語(yǔ)言、測(cè)試方法等。例如，對(duì)版本A和B強(qiáng)制不同的設(shè)計(jì)方法學(xué)，使得當(dāng)版本A失效概率越大時(shí)，版本B失效概率越小，形成失效負(fù)相關(guān)性。

4.2 軟件可靠性增長(zhǎng)模型（SRGM）

大多數(shù)可靠度評(píng)估模型都屬于SRGM，通過(guò)對(duì)軟件測(cè)試和運(yùn)行階段收集到的失效數(shù)據(jù)應(yīng)用統(tǒng)計(jì)推理來(lái)估計(jì)軟件從時(shí)間維度上的可靠度演化曲線。其目的是預(yù)測(cè)為達(dá)到指定可靠度目標(biāo)所需的額外測(cè)試時(shí)間，或是預(yù)測(cè)當(dāng)測(cè)試結(jié)束時(shí)軟件的可靠度［38］。

現(xiàn)有的SRGM已有數(shù)百種，適用于不同的開(kāi)發(fā)過(guò)程和假設(shè)，不少文獻(xiàn)對(duì)已發(fā)表SRGM進(jìn)行了總結(jié)［39－40］。文獻(xiàn)［41］在此基礎(chǔ)上系統(tǒng)地分析了軟件可靠性建模方法的最新研究進(jìn)展，包括分別與混沌理論、未確知理論和機(jī)器學(xué)習(xí)相結(jié)合的研究方向。

文獻(xiàn)［42］指出尚不存在某個(gè)普適的SRGM能對(duì)所有情形下的軟件可靠度給出準(zhǔn)確評(píng)估，也沒(méi)有先驗(yàn)知識(shí)（Priori）能判定在某特定上下文中哪個(gè)模型是最優(yōu)的。于是文獻(xiàn)［43］提出了多模型加權(quán)平均的軟件可靠性綜合模型，用貝葉斯方法通過(guò)權(quán)值的動(dòng)態(tài)調(diào)整實(shí)現(xiàn)模型的選擇與混合，找出最適合待評(píng)估軟件的模型并綜合各模型的評(píng)估結(jié)果，以犧牲模型的高精度換取其穩(wěn)健性、實(shí)用性和可靠性。

近年來(lái)隨機(jī)過(guò)程類SRGM不少研究工作嘗試抽象現(xiàn)有模型并建立統(tǒng)一的框架對(duì)其進(jìn)行考察，例如文獻(xiàn)［44］通過(guò)使用加權(quán)算術(shù)平均、幾何平均、調(diào)和平均等，提出了非齊次泊松過(guò)程模型（NHPP）的統(tǒng)一框架，現(xiàn)所有NHPP模型都可通過(guò)該框架變換而得，從此框架中也可推導(dǎo)出一些新的NHPP模型。文獻(xiàn)［45］中推廣的NHPP模型則將不完全調(diào)試（Imperfect Debugging）和除錯(cuò)效率（Fault Removal Efficiency）考慮進(jìn)來(lái)。Ledoux在文獻(xiàn)［46］中則更進(jìn)一步，使用自激勵(lì)點(diǎn)過(guò)程（Self－Exciting Point Processes）作為基本工具對(duì)失效過(guò)程進(jìn)行建模，將大部分黑盒SRGM（即隨機(jī)過(guò)程類SRGM）統(tǒng)一起來(lái)。

SRGM一般用來(lái)對(duì)單版本軟件進(jìn)行可靠性評(píng)估，但對(duì)多版本軟件也同樣適用。文獻(xiàn)［47］首先提出了針對(duì)NVP系統(tǒng)的SRGM，但沒(méi)有考慮不完全調(diào)試對(duì)獨(dú)立失效和共因失效的影響，并且過(guò)于復(fù)雜，難以應(yīng)用于N＞3的多版本情形。Teng和Pham嘗試克服這些限制和困難，在為NVP建立SRGM同時(shí)考慮測(cè)試和調(diào)試階段的除錯(cuò)效率及新錯(cuò)誤引入率［48］。他們將NVP的失效分為共同失效和并發(fā)獨(dú)立失效，其中共同失效定義為由各版本功能對(duì)等模塊中的相似或相同錯(cuò)誤引起的失效，即CCF，因此可以將該NVP－SRGM看成一種動(dòng)態(tài)CCF模型。

5 結(jié)語(yǔ)

可靠性是衡量軟件質(zhì)量最重要的指標(biāo)之一，對(duì)苛求軟件系統(tǒng)來(lái)說(shuō)可靠性甚至是項(xiàng)目成敗的決定性因素，因而苛求系統(tǒng)的軟件開(kāi)發(fā)模型常采用較為保守、成熟的瀑布模型及其改進(jìn)變種。本文從瀑布式模型的需求、設(shè)計(jì)、實(shí)現(xiàn)、測(cè)試和運(yùn)行等各階段來(lái)分析了苛求軟件開(kāi)發(fā)過(guò)程中常用的方法、技術(shù)和模型，表1總結(jié)比較了這些方法、技術(shù)和模型所使用的開(kāi)發(fā)階段、所面向的目標(biāo)錯(cuò)誤類型及各自的優(yōu)缺點(diǎn)。

表1 苛求軟件可靠性方法、技術(shù)和模型的特點(diǎn)比較

［1］Lee L.The day the phones stopped ringing［M］.New York：Plume，1992.

［2］NASA.Mars climate orbiter mishap investigation board phase i report［R/OL］.［1999－11－10］.ftp：//ftp.hq.nasa.gov/pub/pao/reports/1999/MCO－report.pdf.

［3］Dalal S R，Horgan J R，Kettenring J R.Reliable software and communication：software quality，reliability，and safety［C］.//Proceedings of the 15th International Conference on Software Engineering.Los Alamito：IEEE Computer Society Press，1993：425.

［4］Woodcock J，Larsen P G，Bicarregui J，et al.Formal methods：practice and experience［J］.ACM Computing Surveys，2009，41（4）：19.

［5］Lutz R R.Analyzing software requirements errors in safetycritical，embedded systems［C］.// Proceedings of IEEE International Symposium on Requirements Engineering.Washington：IEEE Computer Society Press，1993：126.

［6］Kelly J C，SherifH J S，Hops J.An analysis of defect densities found during software inspections［J］.Journal of Systems and Software，1992，17（2）：111.

［7］Easterbrook S，Lutz R，Covington R，et al.Experiences using lightweight formal methods for requirements modeling［J］.IEEE Transactions on Software Engineering，1998，24（1）：4.

［8］肖美華，薛錦矛.形式化方法B及其程序規(guī)約機(jī)理［J］.計(jì)算機(jī)工程，2004，30（16）：16.

［9］Bertrand P，Darimont R，Delor E，et al.GRAIL/KAOS：an environment for goal－driven requirements engineering［C］.//Proceedings of the 20th International Conference on Software Engineering.Washington：IEEE Computer Society Press，1998：58.

［10］Dwyer M B，Avrunin G S，Corbett J C.Patterns in property specifications for finite－state verification［C］.//Proceedings of the 21st International Conference on Software Engineering.New York：ACM Press，1999：411.

［11］Denger C，Berry D M，Kamsties E.Higher quality requirements specifications through natural language patterns［C］.//Proceedings of the IEEE International Conference on Software－Science，Technology ＆ Engineering.Washington：IEEE Computer Society Press，2003：80.

［12］Gervasi V，Nuseibeh B.Lightweight validation of natural language requirements：a case study［J］.Software：Practice＆ Experience，2002，32（2）：113.

［13］Chen L，Avizienis A.N－version programming：a faulttolerance approach to reliability of software operation［C］.//Proceedings of the 8th International Symposium on Fault－Tolerant Computing.［S.l.］：［s.n.］，1978：3.

［14］Randell B.System structure for software fault tolerance［J］.IEEE Transactions on Software Engineering，1975，1（2）：220.

［15］Hecht H.Fault－tolerant software for real－time applications［J］.ACM Computing Surveys，1976，8（4）：391.

［16］Scott R K，Gault J W，Mcallister D F.Fault－tolerant software reliability modeling［J］.IEEE Transactions on Software Engineering，1987，13（5）：582.

［17］Brlli F，Jedrzejowicz P.Fault－tolerant programs and their reliability［J］.IEEE Transactions on Reliability，1990，39（2）：184.

［18］Ammann P E，Knight J C.Data diversity：an approach to software fault tolerance［J］.IEEE Transactions on Computers，1988，37（4）：418.

［19］Hughes J.Why functional programming matters［J］.The Computer Journal，1989，32（2）：98.

［20］Chudleigh M，Berridge C，May R，et al.The SADLI project：safety critical software research in the medical diagnostic domain［J］.Computing ＆ Control Engineering Journal，1995，6（5）：211.

［21］Butler J.Use of a functional programming language for formal specification［C］.//IEE Colloquium on Practical Application of Formal Methods.［S.l.］：［s.n.］，1995：2/1－2/3.

［22］IEC 61508， Functional safety of electrical/electronic/programmable electronic safety－related systems，parts 1－7［S］.

［23］Halbwachs N，Caspi P，Raymond P，et al.The synchronous data－flow programming language LUSTRE［J］.Proceedings of the IEEE，1991，79（9）：1305.

［24］Benveniste A，Caspi P，Edwards S A，et al.The synchronous languages 12years later［J］.Proceedings of the IEEE，2003，91（1）：64.

［25］Hammond K，Michaelson G. Hume：a domain－specific language for real－time embedded systems［C］.//Proceedings of the 2nd International Conference on Generative Programming and Component Engineering.New York：Springer，2003：37.

［26］Armstrong J，Vipding R，Wikstr M C，et al.Concurrent programming in ERLANG［M］.2nd ed.Hertfordshire：Prentice Hall PTR （UK），1996.

［27］Kitakami M，Kubota S，Ito H.Fault－tolerance of functional programs based on the parallel graph reduction［C］.//Proceedings of Pacific Rim International Symposium on Dependable Computing.Los Alamitos：IEEE Computer Society Press，2001：319.

［28］Brillant S S，Knight J C，Leveson N G.Analysis of faults in an n－version software experiment［J］.IEEE Transactions on Software Engineering，1990，16（2）：238.

［29］Fleming K N.A reliability model for common mode failures in redundant safety systems，report GA－A13284［R］.San Diego：General Atomic Company，1975.

［30］Humphreys R A.Assigning a numerical value to the beta factor common cause evaluation［C］.//Proceedings of the National Reliability Conference.［S.l.］：［s.n.］，1987：2C/5/1–2C/5/8.

［31］Johnston B D.A structured procedure for dependent failure analysis （DFA）［J］.Reliability Engineering，1987，19（2）：125.

［32］Hokstad P，Rausand M.Common cause failure modeling：status and trends［M］.New York：Springer，2008：621.

［33］尹曉偉，錢(qián)文學(xué)，謝里陽(yáng).基于貝葉斯網(wǎng)絡(luò)的系統(tǒng)可靠性共因失效模型［J］.中國(guó)機(jī)械工程，2009，20（1）：90.

［34］王學(xué)敏，謝里陽(yáng)，周金宇，等.相關(guān)失效系統(tǒng)的可靠性模型［J］.東北大學(xué)學(xué)報(bào)：自然科學(xué)版，2004，25（9）：887.

［35］Littlewood B，Popov P，Strigini L.Modeling software design diversity：a review［J］.ACM Computing Surveys，2001，33（2）：177.

［36］Eckhardt D E，Lee L D.A theoretical basis for the analysis of multiversion software subject to coincident errors［J］.IEEE Transactions on Software Engineering，1985，11（12）：1511.

［37］Littlewood B，Miller D R.Conceptual modelling of coincident failures in multiversion software［J］.IEEE Transactions on Software Engineering，1989，15（12）：1596.

［38］Dalal S R.Software reliability models：a selective survey and new directions［M］.New York：Springer，2003：201.

［39］Singpurwalla N D，Wilson S P.Software reliability modeling［J］.International Statistical Review，1994，62（3）：289.

［40］Gokhale S S，Marinos P N，Trivedi K S.Important milestones in software reliability modeling［C］.//Proceedings of the 8th International Conference on Software Engineering and Knowledge Engineering.［S.l.］：［s.n.］，1996：345.

［41］樓俊鋼，江建慧，帥春燕，等.軟件可靠性模型研究進(jìn)展［J］.計(jì)算機(jī)科學(xué)，2010，37（9）：13.

［42］Brocklehurst S，Chan P Y，Littlewood B，et al.Recalibrating software reliability models［J］.IEEE Transactions on Software Engineering，1990，16（4）：458.

［43］鄒豐忠，劉海青，王林.軟件可靠性綜合模型［J］.武漢大學(xué)學(xué)報(bào)：工學(xué)版，2003，36（1）：86.

［44］Huang C Y，Lyu M R，Kuo S Y.Unified scheme of some nonhomogenous poiss on process models for software reliability estimation［J］.IEEE Transactions on Software Engineering，2003，29（3）：261.

［45］Zhang X M，Teng X L，Pham H.Considering fault removal efficiency in software reliability assessment［J］.IEEE Transactions on Systems，Man and Cybernetics，Part A：Systems and Humans，2003，33（1）：114.

［46］Ledoux J.Software reliability modeling［M］.New York：Springer，2003.

［47］Kanoun K，Kaaniche M，Beounes C，et al.Reliability growth of fault－tolerant software［J］.IEEE Transactions on Reliability，1993，42（2）：205.

［48］Teng X L，Pham H.Software fault tolerance［M］.New York：Springer，2003.