基于不變量的軟件可靠性計算

關鍵詞：程序不變量;軟件可靠性;冗余不變量

0 引言（Introduction）

軟件可靠性是描述系統質量的重要度量指標，一般與軟件缺陷和故障直接相關[1-2]。傳統方法往往只關注實際輸出與期望輸出的差異，忽略了程序內部的運行狀況。僅僅根據輸入輸出信息計算軟件可靠性的方法存在以下問題：①測試用例不能覆蓋所有的輸入情況，如果測試用例的質量不高，軟件可靠性計算的準確性則無法得到保證;②存在偶然性正確的情況[3-4]。測試用例執行了錯誤的代碼行，結果卻與標準程序輸出一致，此類測試用例將導致軟件的可靠性計算出現偏差。

為了解決以上問題，需要獲取程序內部數據用于計算可靠性，如程序內部結構、動態行為等。不變量是程序運行當中保持不變的性質，能夠反映內部的動態行為，受外部輸入測試用例的影響較小。因此，本文提出一種基于不變量的可靠性計算方法，將不變量作為失效數據輸入可靠性模型計算，同時利用函數調用關系圖消除冗余，提升失效數據的獨立性。實驗結果表明，對于單一故障程序，不變量約簡后較約簡前可靠性平均提升50.502%，方差較小，更能準確反映軟件的可靠性。

1 方法概述（Overview of the method）

程序不變量以前置條件與后置條件、循環不變量、斷言等形式表現，在程序驗證、文檔完善、程序維護、缺陷定位和修復等方面得到廣泛應用[5]。通過程序執行動態發現的不變量是必然適用于有限輸入的謂詞，但并非對全部輸入都成立，因此被稱為似然不變量，一般直接稱為不變量。從一組成功執行輸入中提取的不變量，如果某個失敗的測試用例違反了這個結果，通常是出現錯誤的跡象。在這種思路下，將失效不變量作為失效數據輸入軟件可靠性模型，首先編譯程序并執行測試套件，分別獲取成功測試用例和失敗測試用例的執行軌跡，使用Daikon工具讀取數據跟蹤和推導程序不變量，利用InvariantDiff檢查異常不變量，并依據函數調用關系進行不變量約簡，得到最終失效數據并輸入Nelson模型計算軟件的可靠性。方法的工作流程如圖1所示。

2 程序不變量（Software invariants）

程序不變量是在一個或多個特定程序點上為真的屬性，它們能夠解釋數據結構和算法，幫助軟件開發人員在比代碼更高的抽象級別上記錄設計決策[6]。Daikon實現了對不變量進行動態檢測，它通過程序插樁監視程序特定位置（一般是方法入口處和出口處）的變量值，并將變量值與一組模板進行匹配，以創建候選不變量，最終輸出過程前置和后置條件，以及在每個公共方法入口和出口處保持的對象不變量與置信程度[7-8]。Daikon可以理解為搜索一大組表示不變量的表達式，并刪除與執行軌跡相矛盾的、與其他不變量冗余的或頻率與偶然性相差不大的表達式[9]。輸出結果可以用作文檔，也可以作為斷言添加到源程序中，或者用作其他工具的輸入[10-12]。Daikon工具實現動態不變量檢測流程如圖2所示。

2.1 獲得程序不變量

如果已知錯誤程序的正確版本，可以通過以下5個步驟獲取失效不變量。

（1）生成測試用例集，在啟用gdwarf-2標志的情況下編譯程序，以生成DWARF-2格式的調試信息和程序，并執行測試用例。

（2）獲得程序執行軌跡文件。C語言程序使用Kvasir作為前端工具，這會生成與每個測試用例的執行相對應的.dtrace和.decls文件。

（3）定義Daikon不變量類型和配置控制參數。不變量的形式有常數（x=a），范圍（a

（4）從軌跡文件中推導不變量。Daikon枚舉了所有簡單的候選不變量，并只保留了出現在所有軌跡文件上的不變量。

（5）消除冗余不變量。Daikon工具報告了3種情況下的冗余不變量。①若兩個或多個不變量總是相等，則所有相等的不變量都具有任一不變量所表示的性質。例如，如果x=y，那么對于任何不變量f，f（x）意味著f（y）。②如果變量等于常數值，它將滿足其他一些不變性質。例如，若x=5，則意味著x 是奇數，x≥5等。③對于兩個程序點A 和點B，如果點B 的所有樣本也出現在點A 處，那么在點B 處的任何不變量在點A 處都必然為真，在點B 中檢測到的不變量是冗余的[14]。這種關系形式轉化為偏序?D，其中較小的元素接收由較高元素接收的樣本的子集，而較高的元素包含在較低元素處為真的不變量的子集。

2.2 異常不變量

對比不變量生成結果發現，正確程序和錯誤程序生成的不變量存在較大差異。這些異常不變量以（type，relationship）的形式出現，例如不變量（Una，DJJ）中出現DJJ關系，即兩個不變量不同（Different）、均得到確認（Justified），暗示著程序出現了影響可靠性的異常。如果將正確程序生成的不變量集合表示為集合A，錯誤程序生成的不變量集合表示為集合B，異常不變量在絕大多數情況下出現在差集B＼A 中。

2.3 依據調用關系約簡

上文提及，Daikon消除了3種情形下的冗余不變量，但不變量之間的關聯性仍未得到完全消除。許多函數的異常不變量是由其調用的函數引起的，即其他函數的錯誤狀態傳遞到了該函數，這些不變量會導致統計的失效數據偏多，進而影響可靠性計算的準確性，因此需要進一步區分。

定義1：如果異常不變量是由其程序錯誤直接導致的，那么這類異常不變量稱為根因不變量;由于所在函數和錯誤函數之間存在依賴關系，即因錯誤傳播引起的異常不變量，這類異常不變量稱為非根因不變量。

根據上述定義，約簡異常不變量需要獲得函數間的依賴關系，研究人員使用Doxygen[15]和Graphiz解析源文件生成函數調用關系圖，可以剔除一些與失效無關的函數，盡量只保留根因不變量。

假定存在函數fi、fj，fi 是fj 的父函數，Enfi表示函數fi∷Enter 處，即函數入口處的異常不變量集合，Exfi 表示函數fi∷Exit處，即函數出口處的異常不變量集合。按照以下公式，對不變量進行約簡：

公式（1）與公式（2）基于的約簡規則主要有以下4條。

（1）移除主函數因命令行參數差異導致的差異不變量。

（2）移除在函數入口處和出口處保持一致的不變量。

形如lt;1，yΔxgt;或lt;yΔx，1gt;（Δ∈{==，！ =，gt;=，lt;=，lt;，gt;}）的失效不變量出現在函數入口處，同時出口處出現對應的lt;1，yΔorig（x）gt;或lt;yΔorig（x），1gt;。

形如或的差異不變量出現在函數入口處，同時出口處出現對應的或。

orig（x）是指進入函數時變量的值（因函數主體可能會修改的值），如果函數出口處仍保持進入函數時的變量的值，說明函數未對變量進行修改。這些失效不變量是由之前調用的函數引起的，只作傳遞使用，因此予以移除。

（3）移除父函數和子函數出口處一致的不變量。

在父函數出口處和子函數出口處保持一致的不變量，只保留子函數出口處的不變量。父函數出口處的差異不變量是由子函數的差異不變量引起的，只需保留子函數出口處的差異不變量。例如，getccl∷Exit 及dodash ∷Exit 均出現= 3{0-}，i[] elementsgt;=1{1+}gt;（Una，DUJ），并且函數getccl調用函數dodash。因此，推斷函數getccl處的差異不變量是因調用dodash引起的，予以移除。

（4）移除可合并的異常不變量。

在函數入口處或出口處，形如和的異常不變量可合并，實際不存在異常不變量;在函數入口處或出口處，出現兩組幾乎一致只有置信度不同的異常不變量，可移除這兩組異常不變量。

不變量約簡程序實現中，將函數調用圖G 作為輸入，圖節點數據包含每個程序點入口處和出口處的失效不變量集合，遍歷該有向圖所有節點，依據約簡規則從數據集合中刪除非根因不變量，約簡過程偽代碼見算法1。

3 可靠性計算模型（Reliability calculation model）

3.1 可靠性模型

本文使用Nelson模型評估軟件的可靠性，Nelson認為，計算機程序可看成一個可計算函數F 的說明[16]。

程序的輸入數據域E= Ei|i=1，2，3，…，N ，其中Ei是程序單次運行時輸入數據，E 是全部輸入數據的集合，N 為集合E 中的數據總數。

每一次函數運行Ei，產生對應的結果F'（Ei），表示函數此次運行的實際輸出結果，而函數的真值為F（Ei）。Δj 表示函數實際輸出值F'（Ei）與真值F（Ei）容許的最大誤差，當差值超過這個范圍，即F（Ei）-F'（Ei） gt;Δj，則認為程序發生了一次失效。

當程序運行時選用的數據不服從均勻分布，可用Pi 表示Ei 被選用的概率，當Ei∈El 時，yi=1;當Ei∈Er 時，yi=0。程序按選用數據概率分布運行一次的失效概率定義為

其中：n 表示輸入數據域數據總數，P（Ei）表示此次輸入域Ei數據中被選中的概率，Ki 表示Ei 域中被選中的數據個數，fi 表示Ki 中導致程序失效的數據個數。

3.2 可靠性計算方法

在獲取程序不變量的示例中，研究人員介紹了如何在已知正確程序的情況下獲得錯誤程序的失效不變量。在軟件的實際運行過程中，不存在“正確程序”，無法獲得“正確程序”的不變量。本文將成功測試用例執行中推導得到的不變量作為“正確程序”的不變量，將失敗測試用例執行中推導得到的不變量作為“錯誤程序”的不變量，并利用這兩組不變量進行軟件可靠性的計算。

以西門子程序包中replace程序V1為例，闡述如何計算程序的可靠性，具體步驟如下。

（1）根據“2 程序不變量”節的描述，分別獲取成功執行和失敗執行測試用例，運行程序并收集軌跡數據，推導程序不變量。

（2）replace程序生成函數調用關系圖（圖3）。

（3）異常不變量約簡，依據“2.3 依據調用關系約簡”小節中描述的約簡規則，盡可能地移除非根因不變量，得到最終失效不變量。replace V1程序點共有42處，異常不變量所在程序點共有10處，失效不變量所在程序點有3處。

（4）統計程序點、失效不變量、每個程序點失效不變量出現的概率，計算得到replace程序V1可靠性為96.96%。

4 實驗與分析（Experiment and analysis）

4.1 程序來源

本文選取的實驗程序為西門子程序包，來源于SIR（Software-artifact Infrastructure Repository），包括print_tokens、print_tokens2、replace、schedule、schedule2、tcas、tot_info七個程序[17]。每個程序包含一個正確版本和若干個錯誤版本，某個程序對應的每個錯誤版本只包含一個人工植入的錯誤，西門子程序包見表1。

4.2 傳統方法計算軟件可靠性

對西門子程序包中的7個程序進行實驗發現，132個錯誤版本中的一部分版本無法使用：①執行時發生了段錯誤，不能收集到完整的覆蓋信息;②沒有失敗的測試用例;③錯誤發生在頭文件變量聲明中。排除這些錯誤版本，余下每個程序選擇4個錯誤版本執行所有測試用例，通過對比實際輸出值與期望值獲取程序失效數據，傳統方法計算的可靠性結果見表2。

4.3 不變量計算軟件可靠性

程序不變量是在程序運行過程中始終保持真的屬性，使用傳統方法獲得的軟件可靠性在很大程度上依賴于測試用例的質量，測試用例無法覆蓋錯誤代碼或是存在多個偶然性正確的測試用例，都會導致計算結果產生誤差，而基于不變量的方法依賴的失效數據刻畫了程序的動態行為，對程序內部發生的過程有更深入的理解。研究人員獲取失敗測試用例產生的不變量違反正確測試用例產生的不變量程序點數量和總不變量程序點數量，使用Nelson模型可計算得到軟件可靠性。西門子程序包中的7個程序不變量約簡前使用Nelson模型計算的可靠性結果見表3。

這些不變量中也存在一些無用的非根因不變量，會影響計算結果的準確性。因此，結合函數調用關系圖約簡可能產生偏差的不變量，能夠進一步提升Nelson模型可靠性計算的準確性，依據約簡規則篩除部分不變量后，表4為西門子程序包中的7個程序不變量約簡后使用Nelson模型計算的可靠性結果。

圖4展示了西門子程序包中的7個程序各4個示例的軟件可靠性結果。這些示例分別通過3種不同的方法計算軟件可靠性：傳統的計算方法、在Nelson模型中應用約簡前不變量的方法，以及在Nelson模型中應用約簡后不變量的方法。從中可以發現，基于不變量的可靠性計算方法經過不變量約簡，可靠性大幅提升，并且通過本文方法得到的同一程序的4個示例可靠性結果方差較小。這是由于約簡之前的差異不變量之間存在較大的相關性，例如一些不變量之間具有等價關系或者不變量之間的關系具有傳遞性，導致最后獲取的失效數據較實際情況偏多。不變量約簡后可靠性結果和傳統方法比較，數值上還存在一定差距，分析其原因，一是選擇的程序測試用例數量較大，其中影響可靠性結果的測試用例占比較小，二是約簡后失效數據還存在一定相關性。

5 結論（Conclusion

本文以程序不變量收集失效數據，并通過函數調用關系圖約簡非根因不變量，從而更準確地評估軟件的可靠性。軟件的可靠性是由其內部信息決定的，從不變量角度刻畫可靠性能反映整體行為。實驗結果表明，基于不變量的可靠性計算方法約簡后計算得到的可靠性結果，較約簡前平均提升50.502%，其中print_tokens2最小方差可達到0。該方法應用于單故障程序得到的可靠性數據較穩定，更接近實際可靠性，但與傳統方法計算結果相比，數值上仍存在一定差距，因此在未來研究中，還需要進一步消除冗余不變量，提高失效數據的獨立性。