目標符合性論證中成本優化的證據收集方法*

李 璇，吳 際，劉 超，楊海燕

北京航空航天大學 計算機學院，北京 100191

1 引言

證據定義為用于符合性論證的數據[1]，即論證過程的輸入。證據收集成本用于描述將該證據“能證明目標滿足符合性要求”的置信度從x提升到x+?x所花費的絕對成本。其中，?x理解為證據收集力度。

在實際案例中，證據信息主要通過申請者從大量文檔、源文件和測試日志等收集獲得。依賴人主觀判斷的證據收集通常是耗時和易出錯的[2-3]，這主要歸因于以下兩方面：（1）收集者對目標的證據需求沒有建立準確的認知，而收集大量無效的信息作為證據。（2）論證結構中復雜的論證關系和論證方法使得收集者難以判斷證據效力，可能消耗大量成本在低效力證據收集上或在同效力證據項中錯誤選擇了高收集成本的證據。

在避免收集無效證據的問題上，Panesar-Walawege等人提出了一種基于UML的模型驅動方法[4-5]以獲得安全標準下所需要的證據；文獻[6]提出了一種基于systematic literature review（SLR）的安全證據收集、組織和論證的方法。但對于如何從已知有效的證據集中確定下一步待收集的證據和收集力度，以保證高效低成本地完成目標符合性從不滿足期望值到滿足期望值的提升，尤其對采用定量評估方法的目標符合性論證來說，仍缺少有效的方法。

結合上述問題，本文的目標是結合目標符合性論證結構和過程信息，為證據收集者提供一種成本優化的證據收集方法，以保證目標符合性能夠從不滿足期望值提升到滿足期望值。結合上述目標，本文基于動態規劃[7]的思想，提出了一種基于成本分配模型的證據收集方案。考慮到論證方法中定量評估[8]較定性評估[9]引入了置信度的概念和復雜計算，以及定量評估中 BBN（Bayesian belief network）[10]和D-S證據理論[11]方法在數學層次上的關系，本文針對采用D-S證據理論和事件概率論證方法的目標符合性論證展開，更具有實際意義和拓展性。

本文第2章介紹了相關背景知識。第3章介紹了基于成本分配模型的證據收集方案的相關細節。第4章以案例的形式描述方案的實際應用過程，說明本文方案的有效性。第5章介紹了相關研究工作。第6章對本文工作進行總結并指出進一步的研究方向。

2 背景

2.1 論證模式

論證模式描述了證據對目標的向上論證關系，特別指出，子目標在用于論證父目標符合性時，被視為具有依賴的證據，這類證據不同于普通證據能夠直接論證目標符合性，它們需要同其他子目標以“與”、“或”的方式來聯合論證目標符合性。

在適航認證領域，目標或直接受普通證據論證，或至少存在兩個子目標，存在子目標的目標不受普通證據直接論證，因為普通證據總能對應論證到該父目標的某一子目標項上。結合上述分析，論證結構主要包括4種基本論證模式，如圖1所示。

Fig.1 4 basic demonstration modes圖1 4種基本論證模式

其中，“單證據支持”表示目標符合性僅受單一普通證據論證，體現為1∶1的論證關系；“多證據支持”表示目標符合性受多條普通證據論證，體現為1∶n的論證關系；“與邏輯”定性描述為任意子目標符合性均滿足是目標符合性滿足的充要條件，體現為A&B→C的論證關系；“或邏輯”定性描述為存在子目標符合性滿足是目標符合性滿足的充要條件，體現為A|B→C的論證關系。文中將上述4種論證模式用一組統一描述規則定義如下：

其中，Object表示被論證的目標；ESet表示論證目標Object的證據集合；ArguType表示ESet對Object的向上論證關系，null表示ESet為普通證據集合，依據ESet中證據數量表現為單證據支持或多證據支持，and/or表示ESet為Object的子目標集，論證模式分別表現為“與邏輯”和“或邏輯”。

無法用上述4種論證模式直觀表達的論證關系稱為復雜論證模式。

2.2 D-S證據理論

D-S證據理論作為一種不確定推理方法，主要特點是：滿足比貝葉斯概率論更弱的條件；具有直接表達“不確定”的能力。本文對于“單證據支持”和“多證據支持”論證模式采用了D-S證據理論論證上級目標的符合性，主要涉及的領域概念如下：

（1）識別框架Θ

對于識別框架Θ，總存在以下假設，就是在框架Θ中存在且僅存在一種可能性是該判決問題的答案，即在Θ中存在著唯一的真值。

（2）mass函數（也稱為基本可信度分配）

（3）信度函數Bel

（4）m個mass函數的Dempster合成規則

對于?A?Θ，識別框架Θ的有限個mass函數m1，m2,…,mn的Dempster合成規則為：

2.3 事件概率

對于相互獨立事件A和B，A與B均發生A∩B的概率為P(AB)=P(A)×P(B)，A與B至少一件事件發生A∪B概率為P(A+B)=P(A)+P(B)-P(A)×P(B)=1-

本文對于“與邏輯”和“或邏輯”論證模式分別采用了交事件和合事件論證上級目標的符合性。

2.4 證據收集成本

依據工程經驗可知，證據收集成本與置信度的相關性可描述為同類證據同樣將置信度提升差值?t時，起始基準較小的證據所花費的成本會低于另一項，即置信度v從0提升到0.3花費的成本必定小于/等于v從0.6到0.9花費的成本，甚至有可能隨著起始基準的增加使得成本指數性增長。考慮到證據優化方案于提升證據置信度所花費的絕對成本，故而成本分布應依據證據置信度從當前值v提升?t所需的絕對成本f(?t,v)給出，實際使用中可借助Matlab等依據實際工程數據擬合獲得成本分布函數。

3 基于成本分配模型的證據收集方案

成本分配模型描述了提升頂級父目標符合性到期望值時所花費的最低證據收集總成本及對應的證據收集方案。

其中，MinCost表示頂級父目標從HisValue提升到ReqValue花費的最小成本；TraceList表示最小成本下的證據收集鏈集合。

成本分配模型的構建過程涉及到兩個模型、一項指南和3個規則。“兩個模型”分別為目標符合性論證模型和目標符合性與成本關聯模型，“一項指南”為原生復雜論證模式轉換指南，“3個規則”為目標符合性提升范圍劃定規則、關聯模型遍歷規則和證據收集鏈構建規則。

目標符合性論證模型分別對適航領域存在的4種基本論證模式構建了對應的目標符合性論證公式，是目標符合性與成本關聯模型構建要素之一。

目標符合性與成本關聯模型定位于描述深度為2的論證結構下的頂級目標符合性成本關聯關系，是成本分配模型實施過程的基本要素。

復雜論證模式轉換指南能夠保證上述兩個面向4種基本論證模式的模型即使在復雜論證模式的情況下也能成功構建。

目標符合性提升范圍劃定規則用于為目標符合性與成本關聯模型建立過程規避掉無效用的計算。

關聯模型遍歷規則描述了為論證結構中各目標建立關聯模型時應遵循的構建順序。

證據收集鏈構建規則描述了如何從頂級目標的關聯模型中回溯獲得最終的證據收集方案。

上述各模型與規則的作用關系如圖2所示。

3.1 目標符合性論證模型

目標符合性論證模型的定義如下：

其中，CPSet為證據“能證明目標滿足符合性要求”的置信度；ArguType為目標符合性論證方法。

當論證方法ArguType為D-S證據理論時，構建識別框架Θ={valid,unvalid,uncertain}，其中valid表示目標通過符合性認證這一斷言成立的可信度，unvalid表示目標通過符合性認證這一斷言不成立的可信度，uncertain表示不確定程度，則有：

Fig.2 Relationship between model and rule圖2 模型與規則作用關系圖

當論證方法ArguType為事件概率中的交事件時，目標通過符合性認證這一斷言成立的充分條件是各證據項均通過符合性認證，則有：

當論證方法ArguType為事件概率中的合事件時，目標通過符合性認證這一斷言成立的充分條件是存在證據項通過符合性認證，則有：

3.2 目標符合性與成本關聯模型

關聯模型以成本為目標函數，表示目標符合性程度每提升x所花費的證據收集成本。

其中，DP表示一種動態規劃方案，是形成該關聯模型的核心組件；HisValue表示目標符合性當前值；ReqValue表示目標符合性期望值；MinCost表示將目標符合性從HisValue提升到ReqValue的最小成本；ETuple表示收集成本為MinCost時的直接證據的收集方案，如下方式：

DP是以成本最低為目標的動態規劃方案，其規劃過程需要論證模式、論證方法、證據成本、目標符合性當前值和目標符合性期望值的支持。

其中，AM表示目標的論證模式；AU表示目標符合性論證函數；FSet表示證據成本集合；CPSet表示證據符合性程度當前值集合。

假設對目標g建立符合性與成本的關聯模型，其中目標g符合性受n個證據e1,e2,…,en論證，每個證據的初始符合性程度記為ci,i=1,2,…,n,則DP動態規劃方案執行步驟描述如下：

輸入：AM，AU，Fset，CPSet，HistValue，ReqValue。

輸出：C(g,k,k′)表示目標g符合性從k′提升到k所產生的最小成本；ETuple表示最小成本下的證據提升分配方案。

約束條件：

1.k=ReqValue,k′=HisValue

2.若AM.ArguType=null,n=1,即論證模式為“單證據支持”，則:

3.若AM.ArguType=null或AM.ArguType=and，即論證模式為“多證據支持”或“與邏輯”，則:

其中，Eg[k][i]表示最多提升目標g的前i個證據使得A符合性達到k的最低成本；pg(t1,t2,…,ti)表示目標g的前i個證據提升到ti所花費的成本。

4.若AM.ArguType=or即論證模式為“或邏輯”：

上述動態規劃方案，依據論證模型作為優化過程中的約束條件，使得輸出結果總能保證目標符合性達到期望值。該關聯模型的建立，將論證結構中各目標符合性的提升成本從未知轉為已知，使得后續成本分配模型得以展開。

3.3 復雜論證模式轉換指南

目標符合性與成本關聯模型應用場景建立在圖1所描述的4種基本論證模式上。在論證結構中，可能會存在復雜論證模式，這類論證模式無法直接支持目標符合性與成本關聯模型的建立。因此，本節給出一種轉換指南指導復雜論證模式到基本論證模式的轉換。轉換的前提是保證論證結構轉換前后的一致性，轉換后論證模式應為4種基本論證模式的簡單相加。

這里復雜論證模式指具有以下3種任意一種的表現形式：

（3）在同一目標→目標的論證維度下，無法用單一的“與邏輯”或“或邏輯”表示論證關系，表現為A&(B|C)→D或者A|(B&C)→D。

針對上述3種表現形式，建立轉換指南如圖3所示。

3.4 目標符合性提升范圍劃定規則

目標符合性提升范圍Ug=[a,b]定義了頂級父目標符合性達到期望值時目標g自身符合性允許的取值區間。其中，a表示目標g的符合性至少要提升到a才使得頂級父目標符合性可能達到期望值，b表示目標g的符合性提升到b時使得頂級父目標符合性必定達到期望值。

通過為目標g設定提升范圍，可以為后續目標符合性與成本關聯模型建立過程規避掉無效用的計算，因為提升目標g的置信度到b肯定比b+ε的成本要低，而目標g的置信度小于a時獲得的搜索組合無法使頂級目標置信度達到期望值。

Fig.3 Conversion guide圖3 轉換指南

目標符合性提升范圍由父目標符合性的提升范圍、目標符合性當前值及目標與父目標間的論證模式確定。依據上述要素，將影響性質劃分為3類：

第一類目標：該類目標必使得頂級目標“通過符合性審查”的置信度小于期望值。

第二類目標：非第一類和第三類的目標。

第三類目標：該類目標必使得頂級目標“通過符合性審查”的置信度大于期望值。

設目標g的符合性當前取值為HV，其父目標r的提升范圍為Up=[L,H]，則目標符合性提升范圍Ug的劃定規則如表1所示。

Table 1 Lifting rangeUg=[a,b]delineation rules表1 提升范圍Ug=[a,b]劃定規則

3.5 關聯模型遍歷規則

建立父目標的符合性與成本關聯模型的前提是其1級子目標均建立了成本關聯模型。在面向完整論證結構時，只有位于論證結構最底層的普通證據的成本分布是給定的，各級目標的成本均需要通過建立目標符合性與成本關聯模型獲得。

結合上述分析，將論證結構看作一棵論證樹，其中頂級父目標為樹的根節點，各級子目標按照論證層次作為樹中的各級節點，普通證據為樹的葉節點，定義關聯模型遍歷規則如下：

（1）后根遍歷論證樹的各目標子樹。

（2）訪問根節點，即頂級目標。

3.6 證據收集鏈構建規則

證據收集鏈是組成證據收集方案的基本單位，其具有以下性質：

（1）假設以父目標構建一棵樹，則其證據收集鏈即為以鏈首為根節點的n棵子樹，子樹葉節點構成該鏈首項的證據收集集合，所有子樹的葉節點構成該父目標的證據收集集合。

（2）證據收集鏈的總數表示了所需要提升的1級子目標數。

證據收集鏈的構建過程，即是基于廣度遍歷的關聯模型搜索過程。定義證據收集鏈構建規則如下：

（1）初始化n條證據收集鏈，n表示頂級父目標關聯模型下ETuple集中提升力度>0的項的總數，上述n項即為鏈首。

（2）建立一棵以頂級父目標為根節點的樹，其子節點即為上述n項目標。

（3）廣度遍歷樹，若節點為目標，則獲得該目標關聯模型下ETuple集中提升力度>0的m項，拓展為該節點的子節點；若節點為普通證據，不進行處理。

（4）當遍歷結束時，證據提升鏈構建完成。

4 案例分析

為了說明方案的有效性，案例全覆蓋了文中提到的各分支情況，包括4種基本論證模式、復雜論證模式、不同類別的目標，能夠很好地詮釋本文提出的方案在案例中的實施過程。案例分析的目標是說明方案的有效性：（1）方案能夠覆蓋標準符合性審查中的普遍論證模式；（2）依據方案能夠獲得滿足約束條件的證據收集建議。

選取RTCA DO-178C[12]中的目標“High-level requirements comply with system requirements.”作為頂級目標，其對應的目標符合性論證結構如圖4所示，數據信息如表2所示。

Fig.4 Argument structure圖4 論證結構關系圖

Table 2 Basic data information表2 基本數據信息表

A:High-level requirements comply with system requirements.

o1:All system requirements are satisfied by the high level requirements.

o2:Derived requirements and the reason for their existence are correctly defined.

o3:There is no derived requirements at all.

e1:Software verification results about the functional requirements compliance.

e2:Software verification results about the performance requirements compliance.

e3:Software verification results about the safety-related requirements compliance.

e4:Software verification results about the derived requirements compliance.

e5:Software verification results about the derived requirements recorded.

e6:Software verification results about the derived requirements recorded.

其中證據e1、e2、e3、e4到目標o1表現為多證據支持論證模式；證據e5到目標o2表現為單證據支持論證模式；證據e6到目標o3表現為單證據支持論證模式；目標o1、o2、o3到目標A表現為復雜論證模式。

其中，證據置信度與證據成本分布由申請人或專家提供，目標置信度通過上文中的目標符合性論證模型獲得。在這里，本文問題重心定位為“目標符合性論證中成本優化的證據收集方法”,故前提條件中的證據置信度和證據成本分布均為仿真數據，真實數據由申請人或專家提供。

通過建立目標符合性與成本關聯模型，獲得目標o1、o2和o3的目標符合性與最小成本的對應關系如圖5所示，其中x軸表示目標符合性取值，y軸表示最小成本，(x,y)表示將目標符合性從當前值提升到x所需的最小成本，數據標注描述了最小成本下的證據收集方案ETuple。

最后，對頂級父目標A建立關聯模型，獲得目標A符合性從0.89提升到0.94的最小成本為19.67，對應的直接收集方案為：提升目標o1符合性到0.97，提升目標o2符合性到0.95，提升目標o3符合性到0.40。依據證據收集鏈構建規則，獲得最終的證據收集方案為表3所示。

Fig.5 Relationship between object conformance and minimum cost圖5 目標符合性與最小成本對應關系圖

Table 3 Evidence collection表3 證據收集方案

在實際收集過程中，可圍繞提高證據的完備率或證據可信度展開。其中，證據的完備率表明了其支持目標通過符合性審查的能力，而證據收集方式的差異將會影響證據的可信度。舉例來說，支持軟件版本質量滿足目標“最新版本的測試失效數大于5”的要求的證據是”最新版本的測試失效數為2”，假設該證據的置信度（0.7,0.1,0.2），若要提升置信度到（0.9,0,0.1），則可以考慮從（1）測試覆蓋率；（2）RTOS4A復雜度；（3）測試成本；（4）測試方法等方面加以提升。

案例中覆蓋了“基于證據的目標符合性評審”中會涉及到的4種論證模式，能夠適用于符合性論證中的大多論證結構。同時，針對復雜的論證模式，給出了轉換指南以指導完成復雜論證模式到基本論證模式的轉換。說明目標符合性提升方案能夠適用于多種論證場景。

將案例返回的證據優化方案作為驗證信息，代入e1=(0.68,0.30,0.02)，e2=(0.50,0.20,0.30)，e3=(0.50,0.20,0.30)，e5=(0.70,0.10,0.20)，e6=(0.40,0.60,0)到目標A的符合性論證中獲得A(0.941,0.052,0.007)，由于0.941>0.940，說明目標符合性提升方案能夠保證目標A的符合性達到期望值0.940。

為驗證證據收集方案劃定的證據項是否滿足高效低成本的要求，對目標o1的證據e1、e2、e3、e4在收集力度?t=0.08下的效力和成本進行分析，得到表4。

Table 4 Effectiveness of evidence and cost under the same collection effort表4 同收集力度下的證據效力和成本

依據表4可知，在同等收集力度，證據e1不僅效力不低于其他證據，且成本最低，說明了證據收集方案結果的合理性。

依據案例中提供的各證據絕對成本分布函數繪制成本分布趨勢如圖6所示。

Fig.6 Evidence cost distribution圖6 證據成本分布圖

依據表3中的證據收集方案，觀察圖6可知，各證據的收集力度?t均控制在絕對成本f(?t,v)呈較低成本階段，說明本文提出的以最低成本為目標提升方案是有效的。

5 相關工作

雖然目前存在與證據收集相關的研究和方法，但主要集中在如何避免收集無效證據和如何簡化人工證據收集過程。

OMG（Object Management Group）在 2008年提出的SVBR（semantic business vocabulary and rules）[13]和在2011年提出的SACM（structured assurance case model）[14]，前者主要解決安全目標描述時自然語言表達的不一致性和二義性來描述安全目標,后者主要幫助構建和管理證據，但兩者均缺少對證據收集過程的描述。

文獻[5]提出了一種基于SLRs的安全證據收集、管理與評估的方法，但并未展開如何合理地組織證據來提高論證過程的相關研究。文獻[15-16]設計了用于證據收集的工具。

基于上述相關研究，能夠有效地幫助收集者收集與目標符合論證相關的有效證據，但忽略了有效證據間也存在論證效力和收集成本的差異。

本文從證據論證效力和收集成本出發，提出了一種新的證據收集角度來提升目標符合性論證結果，解決當前證據收集研究領域的局限性。

6 結束語

本文針對D-S證據理論和事件概率的目標符合性論證，提出了一種基于成本分配模型的證據收集方案，指導提升目標符合性到期望值的過程，以保證證據收集的成本較低。分析目標符合性論證結構，針對4種基本論證模式建立目標符合性關聯模型，并為復雜論證模式建立轉換指南以拓寬模型的適用性。在關聯模型建立階段，約束了目標符合性取值范圍，有效地規避了無效用計算。在以后的研究中，將在關聯模型的目標遍歷規則中依據劃分的目標類別構造遍歷優先級，來代替當前平等的后根遍歷算法以提高計算效率。此外，針對BNNs條件概率和主觀邏輯與本文方案采用論證方法具有相通性，可拓展方案到適用于上述兩種論證方法中。