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

武延華 薛小平 王小平

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

近年來，軟件越來越多被應用在安全苛求（Safety－Critical）、任務苛求（Mission－Critical）等領域，如航空航天、軌道交通、核工業等。但苛求系統需求增長在一定程度上超出了構建和維護這類系統的能力發展，因軟件失效造成關鍵任務失敗和生命財產損失的案例屢有報道［1－3］，軟件可靠性受到了廣泛關注。軟件可靠性定義為系統在給定時間和條件下完成其規定任務的能力，當系統正常工作時（即可靠時）是安全的，即可靠性蘊含安全性。為描述方便，本文中提及可靠性時，同時也包含了安全性。

軟件開發活動極其復雜，在整個生命周期中把握軟件可靠性本質更為困難。受包括項目預算、開發周期、團隊管理水平、程序員能力經驗、商業軟件模塊、軟件運行環境等在內的多種因素影響，容易在不經意的情況下引入錯誤。

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

需求形式化建模雖然可有效提高軟件規格的質量，但非形式化描述與形式化模型間的語義一致性及對其驗證的可行性、可信性等仍是難題。因語義扭曲導致的規格錯誤可能會帶來系統失效風險；多版本軟件容錯試圖屏蔽設計錯誤，卻對由規格錯誤等原因導致的系統共因失效（Common－Cause Failure，簡為CCF）無能為力；函數式程序設計作為輕量級形式化實現技術，在編寫可靠代碼方面有諸多特征和優勢，但并未受到軟件界的廣泛重視；可靠度評估模型雖然無法直接改善軟件可靠性，但定量評估軟件可靠度卻能為可靠性改善提供依據和指導。

1 需求與規格形式化方法

目前，苛求系統開發通常采用形式化方法，即通過數學方法對軟件生命周期中各個階段的活動客體進行建模，分析并驗證其隱含性質，并在開發過程中采用V＆V（驗證與確認）方法達到安全和可靠的目的。文獻［4］指出，廣義的形式化方法可跨越軟件工程的整個生命周期，各個階段擁有其獨特的形式化方法。但狹義上的形式化方法大多特指需求階段的各種規格說明語言（例如Z，VDM（維也納開發方法），Alloy等）和并發建模框架（例如CSP（通信順序進程）、CCS（通信系統演示）等進程代數）。

需求是軟件開發活動的基礎，需求規格錯誤對可靠性的影響貫穿了整個軟件生命周期。文獻［5］對系統集成和測試階段發現的387個軟件錯誤進行研究后指出，與安全相關的大多數軟件錯誤都出自不完整的需求規格或是對其的誤解，而文獻［6］指出傳統技術不足以捕捉許多需求錯誤。

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

文獻［7］給出了形式化方法成功應用于任務苛求系統早期需求建模的3個案例。由于采用輕量級形式化方法，這些模型并沒有完全保證目標需求的完整性和正確性，而是通過盡可能揭示非形式化需求中的錯誤來改善需求質量和促進可靠性保證等級。對早期需求建模，考慮到需求本身的粗略性和易變性，這種決策是合理的。另一方面，文獻［7］對3個案例分別采用了標注（Annotated）流程圖、與或表（AND/OR table）和目標建模技術（OMT）作為初始需求描述到需求模型轉換過程的中間結構化表示，用以澄清二義性、深化對需求結構的理解，進一步確定采用何種合適的建模表示法，并給出了使用方法。此外，中間結構化表示同樣為早期需求建模活動提供了更明晰的可追蹤性，保持模型與非形式化需求間緊密的同步一致性。

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

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

2 多版本軟件容錯

基于B方法或者SCADE環境的苛求系統項目，設計僅僅作為規格到實際代碼的中間過渡階段，需求、設計和實現之間的區分變得模糊，基于嚴格數學定義的模型精化及每一步轉換完成的證明責任（Proof Obligation）確保不會引入設計錯誤。但若采用了工具支持薄弱的Z表示法（Notation）或提倡輕量級形式化的Alloy表示法等建立規格，設計與實現活動仍需開發人員介入完成，容易造成規格與設計間的語義分歧，即導致設計錯誤。

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

NVP根據同一份需求構建多份設計差異化（Design Diversity）的軟件版本，順序或并發運行，對各版本輸出采取某種表決算法選出最優解。設計差異化可降低各版本間因相同設計錯誤而導致共因失效（CCF）的可能性，即系統不可檢錯率。假設各軟件版本失效相對獨立，可靠度為Rm1，Rm2，…，Rmn，表決器采用多數表決（Majority Voting）且可靠度為Rv，則系統可靠度

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

由于RB只需一份軟件版本通過測試就能得到最優解，而NVP要求多份版本正確無誤才能表決出最優解，因此只要接受測試設計得當，RB可獲得比NVP更高的系統可靠度。但RB的問題在于：接受測試是依賴于其對應軟件版本內部邏輯的，沒有統一、明確地構造簡單而高可靠接受測試的普適方法。此外，本質上RB要求各版本嚴格順序執行，這導致了潛在的巨大延時風險。意味著對實時性要求較高的應用并不適合，需結合監視定時器（Watchdog Timer）［15］等機制予以輔助。

研究人員嘗試通過NVP和RB的組合來進一步提高可靠性。文獻［16］提出的一致性恢復塊將NVP與RB串聯起來，并復用軟件版本甚至運算結果；文獻［17］提出的接受表決（Acceptance Voting）將RB中的接受測試應用于NVP中每一版本，使每個版本輸出只有通過接受測試才能參與系統輸出表決。這些方法雖然使系統比使用純NVP或純RB達到更高的可靠度，但依然存在諸如接受測試編寫困難、潛在延時風險大的問題。

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

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

3 函數式程序設計

函數式程序設計（Functional Programming，簡為FP）是一種聲明式編程泛型，與軟件形式化方法協同發展起來，兩者共享絕大部分數學基礎，尤其是FP的理論根基（λ演算）來自于形式化方法中基于演算的方法。大多數自動定理證明器或輔助證明系統都采用FP語言編寫，例如Coq、LCF（可計算數邏輯）、HOL（高階邏輯）、Isabelle等。FP把“軟件系統即求值器”的本質在語法層面體現出來，每個函數作為最小模塊單元，具有優良的數學性質，即在任何時候對同樣輸入都產生同樣輸出，沒有副作用。這種引用透明性既避免了命令式語言中常見的編碼錯誤，又使得代碼驗證近似于數學函數驗證，無需繁復冗長的證明規則指導。

文獻［19］闡述了FP的重要性，認為FP優勢的本質在于提供了新的模塊化能力：高階函數將所執行操作從具有共性的應用模式中抽象出來，惰性求值則將某些迭代計算分離為生成器和篩選器兩個獨立模塊的組合。模塊化的軟件系統突顯了代碼本身及對代碼驗證工作的重用性，使程序更易于理解、編寫、測試和維護，對其可靠性的改善顯而易見。

3.1 FP應用案例

愛爾蘭都柏林城市大學軟件工程中心主導開發的SADLI（診斷實驗室圖象安全保證）項目［20］通過在安全苛求方法學指導下采用FP實現診斷顯微鏡中的成像系統，以確定這種開發方法在該領域中的優勢和限制，其中探索了與FP相關的兩個方面：一是采用FP語言開發復雜軟件系統的可能性；二是安全苛求軟件開發過程中FP語言與傳統安全苛求方法學中最佳實踐準則之間的協調一致性。

研究結果表明，雖然開發該系統需要考慮的實踐問題很多，包括用戶交互、硬件控制、圖像處理、圖像顯示、統計模式識別及與現有軟件的接口，FP依然能順利實現該系統運行。這表明采用FP作為關鍵技術來實現具有相當規模的復雜系統是切實可行的。圖1展示了SADLI的生命周期。

圖1 SADLI的生命周期

從圖1中可見該系統規格也采用了純FP語言Haskell（Gofer為早期Haskell解釋器）來描述（文獻［21］討論了該做法的可行性），將快速原型開發和形式化方法結合起來（從而使得對設計和實現兩者都能進行形式化驗證），又使設計到實現的轉換在同一種泛型內進行，從兩方面將轉換中可能引入的錯誤最少化。項目人員將SADLI基于IEC 61508標準［22］的早期版本進行開發，這就證實了FP與安全苛求系統開發標準間的協調一致性。

3.2 領域專用（Domain Specific）FP語言

除了通用FP語言在苛求系統中的工業實踐外，研究人員更嘗試為苛求系統設計領域專用的FP語言。LUSTRE［23］是一種專為實現反應式系統或進行硬件描述的同步數據流語言，兼并FP模型和并行模型，程序形式化與時態邏輯相似，使該語言既能編寫代碼又能表達和驗證時間屬性。LUSTRE作為法國Esterel公司安全苛求系統開發環境SCADE的核心語言，在工業界應用已有20年［24］，包括航空航天、軌道交通等領域的控制系統。

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

來自Ericsson公司的Erlang語言［26］是一種現在廣泛應用于電信領域的并發函數式語言。作為基礎設施，通信系統需要高可靠地完成所請求任務，即它們是任務苛求系統。此外，任何建設于這些系統之上的安全苛求系統，也使前者帶上了安全苛求的屬性。Erlang作為一種面向并發的分布式容錯語言，最適合處理通信系統的動態性、并發性和實時性，開發出高可靠的分布式并發系統。

3.3 FP中的軟件容錯

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

4 可靠度評估模型

需求、設計和實現階段的任何可靠性方法和技術雖然提高了軟件質量，卻無法完全屏蔽或消除軟件錯誤，且沒有提供定量分析并以此為依據持續改進可靠性。另一方面，通常并不要求苛求系統完全可靠，而是允許其具有既定閾值下的可接受失效率。軟件可靠度評估模型正是實現對系統可靠度進行定量估計的一種統計方法。

4.1 CCF建模

在NVP和RB中，若假設各軟件版本失效相互獨立，則系統可靠度Rsys是組成系統各組件可靠度R1，R2，…，Rn的函數，即 Rsys＝f（R1，R2，…，Rn），如式（1）、（2）所示。這意味著在系統被真正構建出來之前就可預測其可靠度。差異化嘗試使該獨立性假設趨于合理，然而Knight等人進行的27版本實驗［28］及對其進行的故障分析卻揭示了復雜軟件開發過程總會不經意引入相關故障的事實，使差異化軟件系統仍會產生CCF。

4.1.1 CCF模型

CCF模型針對采用了容錯技術的軟件結構，考察組合軟件組件后引入的系統失效新質。最流行的CCF模型是1975年Fleming提出的β因子模型［29］，僅用單個參數β描述冗余組件間的失效耦合。通常只能等系統真正構建出來后通過測試和運行并記錄歷史數據來估計CCF模型中的參數，然而β因子模型的簡單性及其工程實踐經驗，使得針對特定應用就能直接確定β值。例如Humphrey方法［30］、部分 （partial）β 因子法［31］和IEC 61508 標準［22］中β因子模型的查表（checklist）法等。

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

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

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

（3）BFR模型將系統組件失效分為獨立失效和由沖擊引起的任意數量組件失效。其中沖擊的發生滿足齊次泊松分布，且當沖擊發生時每個組件以概率p失效，則因沖擊導致的失效組件數滿足二項分布B（n，p）。

國內學者對CCF模型也進行了廣泛而深入的研究。文獻［33］研究了應用貝葉斯網絡建立CCF系統可靠性模型的方法，將系統中的共因元件分離為具有串聯關系的獨立失效子元件（失效率K1）和共因失效子元件（失效率K2），再分析它們與其它非共因元件的相應關系（如串聯、并聯等），并對典型系統進行了可靠性分析。文獻［34］提出的CCF新模型對假設失效相互獨立時所得的系統可靠度表達式進行變換，加入表征CCF的影響因子，從而將可靠性預測與評估聯系起來，能更全面地計算系統元件之間的相關性，彌補了傳統CCF模型的信息遺漏問題，避免了傳統CCF模型所面臨的組合爆炸問題。

4.1.2 差異化模型

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

EL模型認為軟件的運行環境實際是其執行時的輸入，即任何影響軟件行為的狀態變量。對所有可能開發出的軟件版本及其輸入x，難度函數（Difficulty Function）θ（x）表示在該輸入下軟件失效的概率。若θ（x）越大，則表明輸入x的難度越大，多個軟件版本在該輸入下都失效的概率也越大，導致失效正相關性。

在EL模型中，設計差異化僅僅是選擇不同開發團隊隨機達到的，即仍然可能存在相同設計。而LM模型是EL模型的推廣，對不同版本間的設計差異進行強制（Force），包括選擇不同的開發過程、程序設計語言、測試方法等。例如，對版本A和B強制不同的設計方法學，使得當版本A失效概率越大時，版本B失效概率越小，形成失效負相關性。

4.2 軟件可靠性增長模型（SRGM）

大多數可靠度評估模型都屬于SRGM，通過對軟件測試和運行階段收集到的失效數據應用統計推理來估計軟件從時間維度上的可靠度演化曲線。其目的是預測為達到指定可靠度目標所需的額外測試時間，或是預測當測試結束時軟件的可靠度［38］。

現有的SRGM已有數百種，適用于不同的開發過程和假設，不少文獻對已發表SRGM進行了總結［39－40］。文獻［41］在此基礎上系統地分析了軟件可靠性建模方法的最新研究進展，包括分別與混沌理論、未確知理論和機器學習相結合的研究方向。

文獻［42］指出尚不存在某個普適的SRGM能對所有情形下的軟件可靠度給出準確評估，也沒有先驗知識（Priori）能判定在某特定上下文中哪個模型是最優的。于是文獻［43］提出了多模型加權平均的軟件可靠性綜合模型，用貝葉斯方法通過權值的動態調整實現模型的選擇與混合，找出最適合待評估軟件的模型并綜合各模型的評估結果，以犧牲模型的高精度換取其穩健性、實用性和可靠性。

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

SRGM一般用來對單版本軟件進行可靠性評估，但對多版本軟件也同樣適用。文獻［47］首先提出了針對NVP系統的SRGM，但沒有考慮不完全調試對獨立失效和共因失效的影響，并且過于復雜，難以應用于N＞3的多版本情形。Teng和Pham嘗試克服這些限制和困難，在為NVP建立SRGM同時考慮測試和調試階段的除錯效率及新錯誤引入率［48］。他們將NVP的失效分為共同失效和并發獨立失效，其中共同失效定義為由各版本功能對等模塊中的相似或相同錯誤引起的失效，即CCF，因此可以將該NVP－SRGM看成一種動態CCF模型。

5 結語

可靠性是衡量軟件質量最重要的指標之一，對苛求軟件系統來說可靠性甚至是項目成敗的決定性因素，因而苛求系統的軟件開發模型常采用較為保守、成熟的瀑布模型及其改進變種。本文從瀑布式模型的需求、設計、實現、測試和運行等各階段來分析了苛求軟件開發過程中常用的方法、技術和模型，表1總結比較了這些方法、技術和模型所使用的開發階段、所面向的目標錯誤類型及各自的優缺點。

表1 苛求軟件可靠性方法、技術和模型的特點比較

［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及其程序規約機理［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］尹曉偉，錢文學，謝里陽.基于貝葉斯網絡的系統可靠性共因失效模型［J］.中國機械工程，2009，20（1）：90.

［34］王學敏，謝里陽，周金宇，等.相關失效系統的可靠性模型［J］.東北大學學報：自然科學版，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］.計算機科學，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］.武漢大學學報：工學版，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.