面向DO-178C軟件測試過程的目標符合性論證模式

楊 陽 吳 際 苑春春 劉 超 楊海燕 邢 亮

1(北京航空航天大學(xué)計算機學(xué)院 北京 100191)2 (中航工業(yè)西安航空計算技術(shù)研究所 西安 710068) (yyangbuaa@sina.com)

面向DO-178C軟件測試過程的目標符合性論證模式

楊 陽1吳 際1苑春春1劉 超1楊海燕1邢 亮2

1(北京航空航天大學(xué)計算機學(xué)院 北京 100191)2(中航工業(yè)西安航空計算技術(shù)研究所 西安 710068) (yyangbuaa@sina.com)

安全關(guān)鍵軟件已廣泛應(yīng)用于眾多領(lǐng)域.鑒于其對防范災(zāi)害風(fēng)險方面的特殊要求，必須符合相關(guān)領(lǐng)域的安全性標準.但是目前對于如何建立面向標準的目標符合性論證模型，尚缺乏有效的方法.針對DO-178C標準中關(guān)于軟件測試過程目標的特征描述，提出了一個基于GSN的目標論證模式描述框架，分別從解決問題、解決方案、應(yīng)用方法和產(chǎn)生效果4個方面對目標論證模式進行描述；同時使用一種擴展的安全案例模式描述方式，用以描述面向標準的目標符合性論證模式.在此基礎(chǔ)上，提出了3種面向DO-178C軟件測試過程的目標符合性論證模式，分別是代碼-需求符合性論證模式、需求測試覆蓋率論證模式、結(jié)構(gòu)測試覆蓋率論證模式，并提出基于這些模式建立針對特定項目的目標符合性論證結(jié)構(gòu)的實例化方法，為建立面向DO-178C軟件測試過程的目標符合性論證結(jié)構(gòu)提供了有效指導(dǎo).通過一個機載嵌入式實時操作系統(tǒng)的案例，說明了提出的目標符合性論證模式的可用性和有效性.

安全關(guān)鍵性軟件；適航認證；DO-178C；GSN；論證模式

安全關(guān)鍵軟件(safety critical software)正在越來越廣泛地應(yīng)用于航空、航天、高鐵、汽車、能源、通信、醫(yī)療、金融、工業(yè)控制等眾多領(lǐng)域.這類軟件必須符合各自領(lǐng)域中規(guī)定的安全性相關(guān)標準，比如在航空領(lǐng)域，機載軟件必須符合最新的適航審定標準DO-178C[1]以及一系列相關(guān)標準，并通過局方的適航審定，才能投入使用.DO-178C針對不同安全等級的軟件分別提出了一系列目標，比如A級軟件必需滿足全部71個目標，其中針對A級軟件的單元測試，要求必需滿足語句覆蓋、分支覆蓋和MCDC覆蓋等測試充分性準則.機載軟件的開發(fā)方需要依據(jù)軟件開發(fā)過程中產(chǎn)生的各種數(shù)據(jù)和信息，提供必要證據(jù)，通過有效的論證過程說明其符合安全性標準中規(guī)定的目標.

但是，目前在建立面向標準的目標符合性論證結(jié)構(gòu)方面還存在3個基本問題：

1) 建立面向特定項目的論證結(jié)構(gòu)涉及的因素多且建立過程復(fù)雜.安全性相關(guān)標準中對產(chǎn)品開發(fā)過程及其制品以及相關(guān)影響因素的監(jiān)控等均有嚴格的要求，明確規(guī)定了必須滿足的一系列目標，包括蘊含的相關(guān)子目標和具體要求.為了對特定的安全關(guān)鍵軟件或系統(tǒng)的標準符合性進行有效論證，需要將其開發(fā)過程(包括各種相關(guān)活動及其采用的方法、準則、策略以及實際執(zhí)行結(jié)果中可提取的安全性相關(guān)證據(jù)等)與相關(guān)標準的具體目標和要求之間建立起明確的關(guān)聯(lián).因此，需要依據(jù)相關(guān)標準，建立針對具體項目的安全性論證結(jié)構(gòu)，以支持其安全論證體系的建設(shè)、安全性相關(guān)證據(jù)的采集和分析以及安全性目標的論證.然而，如何從標準中提取出必需滿足的各個目標及其相關(guān)子目標和具體要求，以建立安全性論證結(jié)構(gòu)，以及如何建立其與具體項目過程及其所產(chǎn)生的相關(guān)證據(jù)之間的關(guān)聯(lián)，目前尚沒有有效的方法.

2) 對于不同的軟件項目，由于其產(chǎn)品特點和開發(fā)過程等方面的差異，其論證結(jié)構(gòu)之間亦存在差異，致使項目相關(guān)的論證結(jié)構(gòu)難以重用.但是，由于在相關(guān)標準的約束下這些論證結(jié)構(gòu)之間顯然存在高度的相似性，因此有必要提煉共性特征，以方便論證結(jié)構(gòu)的快速建立.例如提煉具有共性的論證結(jié)構(gòu)模式，并據(jù)此自動生成針對項目的特定論證結(jié)構(gòu)實例.

3) 事實上，安全性相關(guān)標準中規(guī)定的各種目標之間存在一定關(guān)聯(lián)，其符合性論證結(jié)構(gòu)之間也存在一定的相似性，因此可以進一步提煉面向不同目標的論證結(jié)構(gòu)模式.

本文以DO-178C規(guī)定的軟件測試過程目標為研究對象，參考安全案例模式(safety case pattern)[2]，將可重用的結(jié)構(gòu)模式引入到目標符合性論證結(jié)構(gòu)設(shè)計中，提出了3種針對軟件測試過程目標符合性論證結(jié)構(gòu)的論證模式，以及通過對論證模式的實例化建立面向項目的論證結(jié)構(gòu)的方法.并以某實際項目為應(yīng)用案例，說明本文提出的目標符合性論證模式的可重用性和有效性.這種基于模式的目標符合性論證方法，對于其他面向標準的目標符合性論證同樣具有參考價值，適用于針對DO-178C等安全性相關(guān)標準的目標符合性論證結(jié)構(gòu)的建立.

1 適航軟件論證研究現(xiàn)狀

1.1 DO-178C標準

DO-178C[1]依據(jù)軟件失效帶來的危害等級，將軟件分為A，B，C，D，E五個級別.其中A級軟件對安全性要求最高，E級軟件則不需要滿足DO-178C標準中規(guī)定的目標.DO-178C規(guī)定了不同安全等級的機載軟件在軟件開發(fā)過程中必須符合的目標和相關(guān)要求，在機載軟件的安全性認證中已被廣泛采用.NASA的研究員Holloway[3-4]對于DO-178C中提出的總目標與軟件開發(fā)過程中需要達到的各個目標之間的證明與被證明關(guān)系進行了分析，并通過對這些目標的分類，利用GSN(goal structuring notation)[5]清楚地展示了針對不同安全等級的軟件，其過程目標與總目標之間的結(jié)構(gòu)關(guān)系.國內(nèi)也有針對DO-178BC的研究，文獻[6]將DO-178B標準與DO-178C標準進行比較，分析了DO-178C在軟件開發(fā)過程中新增或者變更的內(nèi)容；文獻[7]提出了滿足DO-178B中結(jié)構(gòu)覆蓋率分析的解決方案，并在實際的項目中應(yīng)用.

在基于DO-178C的認證方面，軟件審批指南(software approval guidelines)[8]為基于DO-178C的認證提供了指導(dǎo)，該指南指出在執(zhí)行基于DO-178C標準的認證時應(yīng)該考慮的因素，并得到了廣泛認可.

1.2 軟件的標準符合性論證方法

標準符合性論證指的是通過建立一種規(guī)范的論證結(jié)構(gòu)來支持對項目實施過程是否符合標準的論證.論證結(jié)構(gòu)中通常包括待論證的標準目標、結(jié)構(gòu)化的論證過程以及用來論證目標的數(shù)據(jù)或證據(jù).

為了論證軟件是否符合標準中規(guī)定的目標(如軟件測試過程需滿足的目標)，可以使用不同的論證方法.例如基于檢查單的論證、基于GQM[9](goal question metric)模型的論證、基于GSN[5]模型的論證等.

基于檢查單的論證是在工程實踐中常用的方法[10].這種方法將標準中規(guī)定目標的具體要求以檢查單的形式列舉出來，通過人工檢查來確認被論證的軟件是否符合檢查單中規(guī)定的各項要求.這種論證方法不僅工作量大，更重要的是通用的檢查單中無法體現(xiàn)具體項目的特點和差異，且無法建立目標與證據(jù)之間的關(guān)聯(lián)，論證結(jié)果常會受到論證人的主觀判斷的影響.

GQM是一種層次化的論證方法，以表格的形式表達，分為目標、問題和度量3層.首先確立目標，然后將目標分解成若干問題，并針對每個問題采用量化的度量來進行論證.然而，這種固定的3層結(jié)構(gòu)對復(fù)雜目標的分層細化難度很大，因此無法支持針對DO-178C這類標準的嚴謹論證.此外，在度量層，只考察了預(yù)定的度量數(shù)據(jù)，而不考慮各種復(fù)雜數(shù)據(jù)或證據(jù)之間的關(guān)系，以及開發(fā)人員能力等復(fù)雜的影響因素.因此，GQM也具有明顯的局限性.

GSN[11]是一種結(jié)構(gòu)化的表示論證組織形式的方法，其主要論證結(jié)構(gòu)為：總目標、可分層細化的子目標及其分解策略、子目標對應(yīng)的證據(jù).基于GSN的論證指的是針對每個待論證的目標，建立對應(yīng)的GSN結(jié)構(gòu)，并根據(jù)采集到的證據(jù)進行目標論證的方法.GSN是一種多層的論證結(jié)構(gòu)，可以根據(jù)標準對目標的定義和相關(guān)要求，將目標分解為若干個子目標，并可以準確描述目標的分解策略等，為目標論證提供必要依據(jù)和指導(dǎo).此外，圖形化的表達方式使得復(fù)雜的論證結(jié)構(gòu)更加直觀，易于理解.在GSN基礎(chǔ)上，GSN提出者通過文獻[11]從論證模式和模塊化表示2個方向進行擴展，使得GSN的適用范圍更加廣闊.

除了GSN提出者的研究團隊，其他的研究團隊針對GSN模型也從不同的側(cè)重點進行了擴展.Takai等人[12]提出在安全案例發(fā)生變更時，針對變更的表示方法，并通過案例說明了該方法的有效性.Matsuno等人[13]提出了基于GSN的安全案例模式的一種參數(shù)化表達方法，這種方法可以支持一致性檢查，避免使用安全案例模式進行參數(shù)實例化時出現(xiàn)的一致性錯誤.

1.3 安全案例和安全案例模式

安全案例用來論證在特定的上下文中，系統(tǒng)是否具有足夠安全的保證[2].安全案例是一種論證結(jié)構(gòu)，由論證目標、結(jié)構(gòu)化的論證過程以及證據(jù)組成.依據(jù)證據(jù)，通過結(jié)構(gòu)化的論證過程來論證預(yù)期的目標是否成立.目前，通常使用GSN來表示安全案例.

安全案例模式(safety case pattern)[2]的概念是由Kelly和McDermid在1998年提出的.安全案例模式使用GSN表示，并對GSN的符號進行了一定的擴展.安全案例模式將可復(fù)用的論證結(jié)構(gòu)這個概念引入了安全案例中.在此基礎(chǔ)上，Alexander等人[14]依據(jù)建立安全案例的經(jīng)驗，在2007年發(fā)表1份報告，針對先進控制軟件總結(jié)了14種安全案例模式，并且使用了參數(shù)化的表示方法來描述安全案例模式，為建立該類型軟件的安全案例提供了指導(dǎo).

2 基于GSN的目標論證模式框架

本文提出一種基于GSN的目標論證模式描述框架，分別從模式的解決問題、解決方案、應(yīng)用方法和產(chǎn)生效果4個方面對目標論證模式進行描述，并提出了一種擴展的安全案例模式描述方式，用于在解決方案中詳細定義面向標準的目標符合性論證模式.該描述方式針對安全案例模式進行擴展，下面對安全案例模式的主要結(jié)構(gòu)和本文擴展的部分進行介紹.

安全案例模式的主要結(jié)構(gòu)如下.

1) 主要論證元素：目標(矩形框表示)、策略(平行四邊形表示)、證據(jù)(圓形表示)；輔助論證元素：上下文(圓角矩形框表示)、假設(shè)(右下角有大寫字母A的橢圓形框)、論證(右下角有大寫字母J的橢圓形框)；關(guān)聯(lián)關(guān)系：實心箭頭建立主要論證元素之間的關(guān)聯(lián)、空心箭頭建立主要論證元素和輔助論證元素的關(guān)聯(lián).

2) 在目標和策略中引入模式變量(以下簡稱變量)，用{變量名}表示，并在其關(guān)聯(lián)的上下文中對變量進行進一步解釋說明，包括對其值域的定義，表達方式為

變量名: {值，…}.

這些變量可以指代目標論證所針對的軟件(項目)、待論證的性質(zhì)或要求、相關(guān)的活動或制品、候選策略、環(huán)境約束等.此外，定義#(Y)為集合Y中元素的數(shù)量.

3) 擴展的關(guān)聯(lián)關(guān)系.在關(guān)聯(lián)關(guān)系上增加了對實例化數(shù)量的約束，用“帶實心圓點的實心箭頭+實例化后的目標數(shù)量”表示；目標間“或”的關(guān)聯(lián)關(guān)系，用“實心箭頭+菱形”表示.

本文擴展的部分如下.

1) 目標關(guān)聯(lián)的上下文中定義目標約束條件.含義為：在進行論證模式實例化時，只有約束條件成立時，對應(yīng)的目標才會存在.

2) 證據(jù)關(guān)聯(lián)的上下文中必須定義對證據(jù)結(jié)構(gòu)的要求，只有提供的證據(jù)元素符合結(jié)構(gòu)的要求時，才能保證最終建立的論證結(jié)構(gòu)成立，可以進行論證推導(dǎo).

3) 建立與標準的關(guān)聯(lián).在各類節(jié)點中，用“(標準中相關(guān)條目編號或章節(jié)號)”方式注釋其與標準中相關(guān)條目的關(guān)聯(lián)性，方便檢查核對論證結(jié)構(gòu)與標準的對應(yīng)關(guān)系.

4) 添加含有字母T的矩形框，用于目標下方.表示該目標成立，不需要用證據(jù)證明.

Fig. 1 Code-requirement conformity argument pattern 1圖1 代碼-需求符合性模式1

為了清晰地區(qū)分出圖1～8定義的各種元素，圖1～8各個元素的標識符均使用大一號的字號；標準的關(guān)聯(lián)性注釋使用帶下劃線的字；所有變量名均使用斜體字.上述擴展元素的標識方式，參見第3節(jié).

此外，本文使用的復(fù)合目標，該符號源于文獻[11]對GSN的擴展.復(fù)合目標(類似文件夾的圖形表示符號，并在其中填寫名稱)，其本身是一個獨立的論證結(jié)構(gòu).引入復(fù)合目標，是為了提取可重用的論證結(jié)構(gòu)，避免在多個目標論證中對其進行重復(fù)定義.同時，通過對復(fù)合目標的引用，可以簡化復(fù)雜的論證結(jié)構(gòu).

3 面向DO -178C軟件測試過程的論證模式

通過對DO-178C標準中關(guān)于軟件測試過程目標和相關(guān)要求的分析，本文提出了針對此類過程的3種典型的論證模式，實現(xiàn)了其目標符合性論證結(jié)構(gòu)的可重用性.這種可重用性主要體現(xiàn)在2個層面：

1) 這種模式可以表示面向標準(即獨立于特定項目)的目標符合性論證結(jié)構(gòu)；

2) 這種模式可以表示針對1個項目中多個同類目標的符合性論證結(jié)構(gòu).

3.1 代碼-需求符合性論證模式

3.1.1 解決問題

DO-178C規(guī)定的基于需求的測試活動的主要目標是測試可運行目標代碼與需求之間是否符合、是否健壯.本節(jié)中提出的模式為建立目標代碼與高層需求和低層需求之間的符合性與健壯性目標(DO-178C附錄A中表A-6的目標1～4)的論證結(jié)構(gòu)提供具體指導(dǎo)，并可通過實例化該論證模式，進一步建立針對具體項目的論證結(jié)構(gòu).

3.1.2 解決方案

解決方案如圖1和圖2所示.

Fig. 2 Code-requirement conformity argument pattern 2圖2 代碼-需求符合性模式2

圖1描述了DO-178C規(guī)定的基于需求的測試活動的主要目標，包括測試可運行目標代碼與需求之間符合性(compliance)和健壯性(robustness).圖2是對復(fù)合目標G2的定義.在該模式定義中：

1) 目標G1中引用的模式變量S指代軟件名稱，在實例化時可直接使用具體的軟件名稱替代；X的取值是其上下文描述中定義的complies或is robust；Y的取值是high-level requirements(高層需求)或low-level requirements(低層需求).

2) 在上下文元素中分別定義了其對應(yīng)的目標或策略的約束條件.例如對策略S1，當(dāng)G1針對的是Y=high-level requirements時，要求論證T=hardwaresoftware integration testing(硬件軟件集成測試)的實現(xiàn)；否則，當(dāng)Y=low-level requirements時，則應(yīng)論證T=software integration testing and low-level test(軟件集成測試以及低層測試).類似地，對目標G2，如果G1針對的是X=complies，則G2中的Z=normal range(測試正常范圍)，否則Z=robustness(測試魯棒性).而對于目標G8，則規(guī)定只有當(dāng)需求中包括狀態(tài)轉(zhuǎn)換的內(nèi)容時，其才需要存在.

3) 針對證據(jù)的上下文描述中給出了對證據(jù)結(jié)構(gòu)的要求.例如對于證據(jù)E1，其上下文描述中定義了測試用例中應(yīng)該包含哪些元素，只有提供的證據(jù)元素符合上下文描述中對證據(jù)結(jié)構(gòu)提出的要求時，才能保證最終建立的論證結(jié)構(gòu)是成立的，可以進行論證推導(dǎo).

圖1和圖2所示的模式表達了DO-178C標準附錄A中表A-6的目標1～4的論證結(jié)構(gòu)，分別用于論證可運行目標代碼與高層需求或低層需求之間的符合性及健壯性.針對總目標G1(可運行目標代碼和需求之間的符合性或健壯性)的論證，被分成2個論證結(jié)構(gòu)，即測試用例的選擇符合標準定義的規(guī)則(S1→G2)以及對整個測試活動中追溯性的檢驗(S2→{G3,G4,G5}).論證1結(jié)構(gòu)依據(jù)S1進行分解論證，S1說明編寫的測試用例所屬測試類型，分解到G2目標，描述了針對各項具體需求編寫覆蓋正常范圍(或健壯性)的測試用例集，并通過擴展的關(guān)聯(lián)關(guān)系說明在實例化論證模式時，要求實現(xiàn)n個目標G2，其中n為需求的總數(shù)量(n=#(Y))，即變量R將實例化為一項具體需求，并且對應(yīng)每一項需求都將實例化出一個G2的實例.在圖2中，將G2按照策略S3向下分解，通過G6～G13將不同類型的需求(時間相關(guān)的需求、涉及到狀態(tài)轉(zhuǎn)換的需求、包含整型實型的需求)，在不同條件下(正常范圍內(nèi)的測試或者健壯性測試)需要選擇的測試用例的目標分別表示出來，并且每個目標的約束條件都以其上下文描述的形式給出定義，最終這些目標用證據(jù)E1論證目標是否實現(xiàn).論證2結(jié)構(gòu)依據(jù)S2進行分解論證，判斷需求、測試用例、測試程序、測試結(jié)果之間是否存在追溯性.其中，目標G3表達每個需求都至少存在一個測試用例，目標G4表達每個測試用例都由測試程序?qū)崿F(xiàn)，目標G5表達每個測試程序都有測試結(jié)果，最終用證據(jù)E2論證這些目標是否實現(xiàn).此外，對證據(jù)E1，E2的結(jié)構(gòu)要求定義在其對應(yīng)的上下文描述中.

3.1.3 應(yīng)用方法

實例化模式的方法分為5步:

1) 結(jié)合項目真實情況實例化論證模式中的模式變量，即將其賦值，并將模式中定義模式變量可能取值的上下文描述矩形框刪除.

2) 結(jié)合項目實際情況判斷是否滿足上下文描述中定義的約束條件，刪除不符合約束條件的子目標及其約束條件，并且在保留的子目標中，將對應(yīng)的約束條件保留，并以假設(shè)(右下角有大寫字母A的橢圓形框)的形式作為輔助論證結(jié)構(gòu)來支撐對應(yīng)的子目標，其含義是：當(dāng)這個假設(shè)成立時，對應(yīng)的子目標才可以進行是否成立的論證.

3) 項目中實際的證據(jù)結(jié)構(gòu)必須滿足模式中規(guī)定的證據(jù)結(jié)構(gòu)，否則無法進行目標符合性論證.

4) 依據(jù)項目實際情況，可以對現(xiàn)有的目標進行進一步的分解，或者添加原來模式中沒有但是項目中必需的子目標項，提供對應(yīng)證據(jù)，并給出對證據(jù)結(jié)構(gòu)的要求，以上下文描述的形式與對應(yīng)證據(jù)相關(guān)聯(lián).

5) 檢查最終實例化目標論證結(jié)構(gòu)，最終建立的論證結(jié)構(gòu)中，不能包括未實例化的模式變量；除證據(jù)結(jié)構(gòu)要求的上下文描述項，不能包含其他約束條件上下文描述項；如果沒有達到上述條件，則重復(fù)上述步驟繼續(xù)實例化.

本文以1個簡化的嵌入式實時操作系統(tǒng)(本文中稱作操作系統(tǒng)A)的論證目標DO-178C附錄A中表A-6的目標1為例，采用上述方法，通過實例化上述論證模式，建立了該項目中針對該目標的論證結(jié)構(gòu)，如圖3所示.

圖3中，首先對G1進行實例化，說明論證的總目標是操作系統(tǒng)A中可運行目標代碼和高層需求之間的符合性，并在其上下文描述對A進行說明.依據(jù)策略S1，S2將總目標G1向下分解.

1) 實例化策略S1的論證結(jié)構(gòu)，編寫高層需求的測試用例屬于軟件硬件集成測試.實例化圖1中的目標G2，該軟件存在9項高層需求，實例化為圖3中的目標G2.1～G2.9.G2.1描述了操作系統(tǒng)A中任務(wù)掛起需求的測試用例要求，按照本模式中的定義，這個需求屬于狀態(tài)轉(zhuǎn)換需求，對應(yīng)于圖2中的G8，除此之外，該需求不滿足這一層級其他目標的約束條件，因此對于這個目標來說，實例化時將刪除模式中的目標G6，G7，G9，G10，G11，G12，G13，只保留G8，并將G8中的約束條件轉(zhuǎn)換為圖3中目標G3.1相關(guān)聯(lián)的假設(shè)(右下方有大寫字母A的橢圓形)，保留模式中的G8被實例化為圖3中G3.1，來測試正常操作下所有狀態(tài)轉(zhuǎn)換.依據(jù)操作系統(tǒng)A的特點可以知道，當(dāng)任務(wù)處于就緒態(tài)或者休眠態(tài)，并且任務(wù)中沒有鎖(鎖機制是操作系統(tǒng)中保持數(shù)據(jù)一致性的一種機制，文獻[15]介紹了操作系統(tǒng)中鎖的實現(xiàn)原理)時可以掛起，因此在該模式的基礎(chǔ)上，還需要添加目標G4.1和目標G4.2，并通過證據(jù)E1證明是否符合目標.

Fig. 3 An example of code-high-level requirement conformity argument structure圖3 代碼-高層需求符合性論證結(jié)構(gòu)示例

由于篇幅限制，本文沒有將G2.2～G2.9的所有目標列舉出來，使用省略號表示，此外G2.9目標下的菱形框表示這個目標需要進一步分解.

2) 實例化策略S2的論證結(jié)構(gòu).圖1中的目標G3要求每個需求都要存在至少一個測試用例.為了節(jié)省篇幅，圖3沒有將每個具體需求的編號逐一展示，而使用“Every requirement has”(每個需求都要實現(xiàn))這樣的句型表示.圖1中的目標G4和G5實例化情況類似.因此，圖1中的G3，G4，G5目標分別對應(yīng)于圖3的G2.10，G2.11，G2.12，并通過證據(jù)E2證明是否符合目標.

3.1.4 產(chǎn)生效果

建立代碼-需求符合性論證模式，有助于為不同項目實現(xiàn)DO-178C附錄A中表A-6的目標1～4的論證結(jié)構(gòu)提供便利.論證模式包含了DO-178C針對這些目標規(guī)定的需要執(zhí)行的所有活動，即在該模式中標注了標準中規(guī)定的所有相關(guān)活動，因此最終建立的論證模型符合標準規(guī)定，并可通過規(guī)范的步驟實例化，從而最終建立簡明的論證結(jié)構(gòu).

此外，模式中為不同活動的執(zhí)行規(guī)定了約束條件，因此，可以依據(jù)項目的實際情況決定是否執(zhí)行該活動，對標準中規(guī)定的活動是否執(zhí)行提供了指導(dǎo)，在保證符合標準的前提下最大程度地提高了效率，避免執(zhí)行不必要的活動.

3.2 需求測試覆蓋率論證模式

3.2.1 解決問題

DO-178C規(guī)定的基于需求的測試活動需要驗證需求的測試覆蓋率.本節(jié)中提出的模式為建立需求測試覆蓋率目標(DO-178C附錄A中表A-7的目標3～4)的論證結(jié)構(gòu)提供具體指導(dǎo)，并可通過實例化該論證模式，進一步建立針對具體項目的論證結(jié)構(gòu).

3.2.2 解決方案

解決方案如圖4所示：

Fig. 4 Test coverage of requirements argument pattern圖4 需求測試覆蓋率論證模式

Fig. 5 An example of test coverage of requirements argument structure圖5 需求測試覆蓋率論證結(jié)構(gòu)示例

圖4描述了針對DO-178C附錄A中表A-7的目標3～4的論證模式，分別用于論證高層需求和低層需求的測試覆蓋率.論證目標G1，分成3個子論證結(jié)構(gòu)，即論證測試用例覆蓋了所有需求，論證所有的測試活動都是基于需求的，論證整個覆蓋率分析所執(zhí)行活動的過程中發(fā)現(xiàn)的缺陷都記錄并且解決了.論證1結(jié)構(gòu)依據(jù)S1進一步分解為目標G2，G2又分解為目標G6和G7.G6驗證基于需求的測試用例是否滿足規(guī)定的正常以及健壯性測試準則，用驗證結(jié)果E1論證該目標是否實現(xiàn).G7說明每個需求都存在正常和健壯性測試用例，用測試用例E2和追溯數(shù)據(jù)E3論證該目標是否實現(xiàn).論證2結(jié)構(gòu)依據(jù)S2分解為G3和G4，分別說明每個測試用例可以追溯到需求和必須存在測試程序可以追溯到測試用例.通過這2個目標來說明所有測試活動都是基于需求的，用追溯數(shù)據(jù)E3論證該目標是否實現(xiàn).論證3結(jié)構(gòu)依據(jù)S3分解為G5，說明所有發(fā)現(xiàn)的缺陷都被記錄并解決，用問題報告E4論證該目標是否實現(xiàn).其中對證據(jù)E1，E2，E3，E4的結(jié)構(gòu)要求定義在其對應(yīng)的上下文中.

3.2.3 應(yīng)用方法

實例化的步驟與3.1.3節(jié)應(yīng)用方法中的1，3，4，5一致，因為本模式中不存在需要刪除的子目標，也不能刪除任何子目標.即便在需求測試覆蓋率分析過程中沒有發(fā)現(xiàn)錯誤，G5中的模式變量D可以用null表示，但是G5是DO-178C中規(guī)定必須執(zhí)行的活動，因此不能刪除.

同樣以操作系統(tǒng)A為例，采用上述方法實例化論證模式建立了針對DO-178C附錄A中表A-7的目標3的論證結(jié)構(gòu)，如圖5所示.

Fig. 6 Test coverage of structure argument pattern 1圖6 結(jié)構(gòu)測試覆蓋率論證模式 1

圖5中，先對G1進行實例化，說明論證的總目標是高層需求的測試覆蓋率符合標準.依據(jù)模式中定義的策略S1，S2，S3將總目標G1向下分解：

1) 實例化策略S1的論證結(jié)構(gòu).即論證測試用例覆蓋了所有的高層需求，實例化圖4中的目標G2，得到圖5中的目標G2.1～G2.9，其中G2.1描述了操作系統(tǒng)A中任務(wù)掛起需求需要被測試用例覆蓋，G3.1說明該測試用例要滿足標準中的準則.依據(jù)DO-178C中對建立測試用例準則的描述，針對該需求需要建立正常操作以及異常操作下所有可能產(chǎn)生的狀態(tài)轉(zhuǎn)換的測試用例，因此添加目標G4.1來說明，判定是否建立了這樣的測試用例集，并通過證據(jù)E1來驗證.除此之外，還需要說明需求包含正常測試用例以及健壯性測試用例，在目標G3.2中說明，并通過證據(jù)E2和E3證明是否符合這項目標.

同樣篇幅限制，本文沒有將G2.2～G2.9的所有目標列舉出來，使用省略號表示.

2) 實例化策略S2的論證結(jié)構(gòu).圖4模式中G3目標要求每個測試用例都可以追溯到需求.為了節(jié)省篇幅，實例化時圖5沒有將每個具體的測試用例的編號逐一展示，而使用“Every test case is”(每個測試用例都要實現(xiàn))這個句型表示.圖4中的目標G4實例化時情況類似.因此，圖4中G3，G4目標分別對應(yīng)于圖5的G2.10，G2.11，并通過證據(jù)E3論證是否符合目標.

3) 實例化策略S3的論證結(jié)構(gòu).在本例中由于沒有在論證需求的測試覆蓋率所執(zhí)行的活動過程中發(fā)現(xiàn)錯誤，因此在子目標G2.12下添加含有內(nèi)容T的矩形框，表示其自動成立，不需要通過證據(jù)證明.

3.2.4 產(chǎn)生效果

建立需求測試覆蓋率論證模式，有助于對不同項目實現(xiàn)DO-178C附錄A中表A-7的目標3～4的論證結(jié)構(gòu)提供便利.論證模式包含了DO-178C針對這些目標規(guī)定的需要執(zhí)行的所有活動，即在該模式中標注了標準中規(guī)定的所有相關(guān)活動，并且在標準規(guī)定的基礎(chǔ)上，對實現(xiàn)這些活動的途徑進行了擴展，因此最終建立的論證模型不僅符合標準規(guī)定，而且具有可行性，并可通過規(guī)范的步驟實例化，從而最終建立簡明的論證結(jié)構(gòu).需要注意的是，本模式中所有的子目標都必須包含并進行論證，否則將不滿足標準的規(guī)定.

3.3 結(jié)構(gòu)測試覆蓋率論證模式

3.3.1 解決問題

DO-178C規(guī)定的基于需求的測試活動需要驗證結(jié)構(gòu)測試覆蓋率.本節(jié)中提出的模式為結(jié)構(gòu)測試覆蓋率目標(DO-178C附錄A中表A-7的目標5～7)的論證結(jié)構(gòu)提供具體指導(dǎo)，并可通過實例化該論證模式，進一步建立針對具體項目的論證結(jié)構(gòu).

Fig. 7 Test coverage of structure argument pattern 2圖7 結(jié)構(gòu)測試覆蓋率論證模式 2

3.3.2 解決方案

圖6和圖7描述的是針對DO-178C附錄A中表A-7的目標5～7的論證模式，分別用于語句覆蓋率、分支覆蓋率以及MCDC覆蓋率.論證目標G1分成3個論證結(jié)構(gòu)：1)當(dāng)待論證軟件是A級軟件時，需要驗證額外代碼[1](即由編譯器、鏈接器或者其他方式生成的不能直接追溯到源代碼語句的代碼)；2)論證代碼的結(jié)構(gòu)化覆蓋率；3)論證整個覆蓋率分析過程所執(zhí)行的活動中發(fā)現(xiàn)的缺陷都記錄并且解決.論證1結(jié)構(gòu)的論證目標是G2(與DO-178C附錄A中表A-7的目標9一致)，需要驗證額外代碼，用驗證結(jié)果E1論證該目標是否實現(xiàn).論證2結(jié)構(gòu)依據(jù)S1進行分解論證，G3說明結(jié)構(gòu)覆蓋率達到了規(guī)定的要求，也要用驗證結(jié)果E1論證該目標是否實現(xiàn).論證3結(jié)構(gòu)依據(jù)S2進行分解論證，G4說明所有的問題都被記錄并解決，并依據(jù)問題的不同，提出需要滿足的不同的要求G5，G6，G7，G8(如圖7所示)，并在對應(yīng)的上下文描述中說明其約束條件，其中G8依據(jù)不同的停用代碼使用情況，分解成目標G9，G10，并在目標G9,G10的上下文描述中說明其約束條件.最終用問題報告E2論證該目標是否實現(xiàn).其中對證據(jù)E1，E2的結(jié)構(gòu)要求定義在其對應(yīng)的上下文中.

3.3.3 應(yīng)用方法

實例化的步驟與3.1.3節(jié)應(yīng)用方法中的1，2，3，4，5一致.如果在結(jié)構(gòu)測試覆蓋率分析過程中沒有發(fā)現(xiàn)錯誤，那么G4中的變量P使用null表示，由于G4是DO-178C中規(guī)定必須執(zhí)行的活動，因此G4不能刪除.

需要特別指出的是，如果規(guī)定的項目不是A級軟件，應(yīng)刪除子目標G2，否則不刪除.

以操作系統(tǒng)S為例，采用上述方法實例化論證模式，最終建立了其針對DO-178C附錄A中表A-7的目標7的論證結(jié)構(gòu)，如圖8所示:

Fig. 8 An example of test coverage of structure argument structure圖8 結(jié)構(gòu)測試覆蓋率論證結(jié)構(gòu)示例

圖8中，先對G1進行實例化，說明論證的總目標是A級軟件S的語句覆蓋率符合標準.依據(jù)模式中定義的策略S1，S2和目標G2，將總目標G1向下分解.

1) 實例化目標G2的論證結(jié)構(gòu).描述A級軟件必須對額外代碼進行驗證，通過證據(jù)E1證明是否符合這項目標.

2) 實例化策略S1的論證結(jié)構(gòu).在本例中，計算軟件的語句覆蓋率，依據(jù)實際情況，需要論證源代碼語句覆蓋率(目標G3)，并通過證據(jù)E1來證明是否符合這項目標.

3) 實例化策略S2的論證結(jié)構(gòu).在本例中，由于在結(jié)構(gòu)覆蓋率分析過程中發(fā)現(xiàn)存在停用代碼的問題，因此需將圖6中的G4實例化為圖8中的G3.1，在進一步向下分解時，刪除圖7模式中其他不符合的目標G5，G6和G7.停用代碼F1由于已經(jīng)被其他代碼取代因而不會再被調(diào)用，因此圖8中G5.1對應(yīng)于圖7中的G9，并將圖7中G9的約束條件以假設(shè)的形式添加到圖8中的目標G5.1中，即保證該代碼在任何情況下都不能被調(diào)用.并通過證據(jù)E2證明是否符合這項目標.

3.3.4 產(chǎn)生效果

建立結(jié)構(gòu)測試覆蓋率論證模式，有助于對不同項目實現(xiàn)DO-178C附錄A中表A-7的目標5～7的論證結(jié)構(gòu)提供便利.論證模式包含了DO-178C針對這些目標規(guī)定的所有需要執(zhí)行的活動，即在該模式中標注了標準中規(guī)定的所有相關(guān)活動，并且列舉出了不同等級軟件需要實現(xiàn)的不同目標，因此最終建立的論證模型符合標準規(guī)定，并可通過規(guī)范的步驟實例化.在實例化的過程中，對于前2個論證結(jié)構(gòu)(圖6中的G2和S1)，不同的項目之間區(qū)別不大，但是對最后一個論證結(jié)構(gòu)(圖6中的S2)，則需依據(jù)項目的實際情況進行實例化，不同的項目之間存在差別.

3.4 論證模式關(guān)聯(lián)

本文提出了上述3種針對DO-178C軟件測試過程目標的論證模式.依據(jù)DO-178C中對軟件測試活動的定義，軟件測試活動分為執(zhí)行不同類型的測試、進行需求測試覆蓋率分析和進行結(jié)構(gòu)測試覆蓋率分析這3種，主要實現(xiàn)的目標是DO-178C中附錄A中表A-6以及表A-7中包含的目標.本文提出的3種模式可以實現(xiàn)DO-178C規(guī)定的軟件測試過程中的9個目標.同時，這3種模式在軟件測試過程目標的論證中缺一不可、相輔相成.

4 方法對比分析

4.1 描述內(nèi)容對比

以3.1.3節(jié)提到的機載操作系統(tǒng)A為例，本節(jié)分別使用本文提出的目標符合性論證模式以及GQM方法進行論證，建立論證結(jié)構(gòu)，并對論證效果進行對比.

圖9所示為論證操作系統(tǒng)A是否滿足DO-178C附錄A中表A-7的目標7的GQM論證結(jié)構(gòu).對其中的每個問題，都對應(yīng)著1個度量來回答該問題.

通過圖9建立的模型，論證人員可以找到度量中提到的數(shù)據(jù)來評估該操作系統(tǒng)是否滿足目標.

基于本文提出的目標符合性論證模式建立的DO-178C附錄A中表A-7的目標7的論證結(jié)構(gòu)如圖8所示.將這2種方法進行對比，可以發(fā)現(xiàn)圖9建立的模型相對簡單，因此只能粗略地列舉需要論證的目標和所需的度量，難以根據(jù)需要逐層細化復(fù)雜論證結(jié)構(gòu)，比如在圖9中：

1) 論證的過程只能分為3層，因此描述的論證結(jié)構(gòu)過于簡單，難以進一步細化復(fù)雜的論證問題.例如問題3：是否所有存在問題都已經(jīng)解決，沒有明確說明對于不同類型的問題，什么樣的處理方式才是合適的.

2) 針對論證目標，對應(yīng)的度量數(shù)據(jù)難以進一步細化定義，因此可能存在歧義.對數(shù)據(jù)的理解不同會直接影響論證的結(jié)果.例如，需要語句覆蓋率的運算結(jié)果，但是沒有說明語句覆蓋率的來源及其必需包含的內(nèi)容.

GoalPurposeIssueObject(Process)ViewpointAchieveStatementcoverageSoftwareverificationprocessFromthecertificationauthoritiesQuestion1Whatisthecurrentstatementcoverage？Metrics1Statementcoverage=Testedstatement∕AllstatementQuestion2Isthestatementcoverageachieved？Metrics2StatementcoverageSubjectiveevaluationofcertificationauthori?tiesQuestion3Allproblemsaresolvedornot？Metrics3Problemreports

Fig. 9 The GQM model of objective 7 in table A-7
圖9 表A-7目標7的GQM論證結(jié)構(gòu)

對于圖9中存在的上述問題，在圖8建立的論證結(jié)構(gòu)中都得到了解決.依據(jù)本文提出的方法建立論證結(jié)構(gòu)，對論證目標及其上下文的約束和證據(jù)及其數(shù)據(jù)結(jié)構(gòu)約束等都有更加完整明確的規(guī)定和清晰的表達方式.

4.2 成本對比

此外，本文提出的基于模式的目標符合性論證方法可以顯著提高論證結(jié)構(gòu)的可重用性，有效地降低面向標準的目標論證結(jié)構(gòu)的建立成本，即工作量.假設(shè)建立1個論證結(jié)構(gòu)的成本為1.由于建立1個GSN論證結(jié)構(gòu)與建立1種相應(yīng)的論證模式的成本是大體相當(dāng)?shù)模嗫梢暈?，因為其主要工作量主要是對標準的理解和論證要素的提取.由于實例化論證模式相對簡單，絕大多數(shù)步驟僅僅是對模式變量值的選擇等，因此其成本可以忽略不計.

以另一個機載嵌入式實時操作系統(tǒng)B為例，表1展示了直接使用GSN建立論證結(jié)構(gòu)，以及使用本文提出的模式建立論證結(jié)構(gòu)來論證DO-178C軟件測試過程目標的成本.

Table 1 The Cost of Constructing Argument Structure

在操作系統(tǒng)B中，高層需求共有708項，低層需求共有3 207項.依據(jù)高層需求，整個系統(tǒng)分為4個子系統(tǒng).依據(jù)低層需求，整個系統(tǒng)分為52個模塊.在建立DO-178C附錄A中表A-6的目標1～2的論證結(jié)構(gòu)時，需要為每個子系統(tǒng)的每種特征(包含時間相關(guān)需求的子集、包含狀態(tài)轉(zhuǎn)換需求的子集、包含其他需求的子集)分別建立論證結(jié)構(gòu)，用以分別判斷其對應(yīng)的測試用例是否符合DO-178C標準中規(guī)定的測試用例設(shè)計準則，因此，需要為每個目標分別建立12個論證結(jié)構(gòu).同理，在建立DO-178C附錄A中表A-6的目標3～4的論證結(jié)構(gòu)時，針對52個模塊，需要為每個目標分別建立156個論證結(jié)構(gòu).因此，對論證DO-178C附錄A中表A-6的目標1～2，直接建立GSN論證結(jié)構(gòu)的成本均為12.對論證DO-178C附錄A中表A-6的目標3～4，直接建立GSN論證結(jié)構(gòu)的成本均為156.然而，建立上述4個目標的論證結(jié)構(gòu)，如采用本文提出的第1種論證模式，通過實例化來建立上述論證結(jié)構(gòu)，則其成本則近似為1.

同樣，由于有4個子系統(tǒng)，所以，針對論證目標DO-178C附錄A中表A-7的目標3～4 和DO-178C附錄A中表A-7的目標5～7，直接建立GSN論證結(jié)構(gòu)的成本均為4，合計20.而采用本文提出的方法，則僅需要分別實例化第2種和第3種論證模式，因此，基于模式建立論證結(jié)構(gòu)的成本均為1，合計為2.

通過本案例可以看出，本文提出的模式能夠應(yīng)用于目標論證結(jié)構(gòu)的建立和實例化工作中，并且能夠有效的降低建立論證結(jié)構(gòu)的成本，提高了效率.

5 結(jié)束語

本文提出一種基于論證模式的標準符合性論證方法，并重點針對DO-178C對軟件測試過程提出的主要目標和要求，提出了3種對應(yīng)的目標符合性論證模式，以及基于這些模式建立面向特定軟件項目的目標符合性論證結(jié)構(gòu)的實例化方法.本文提出的3種論證模式覆蓋了軟件測試過程涉及到的主要目標.在第4節(jié)中，以1個機載操作系統(tǒng)軟件項目為案例，說明了利用本文提出的模式建立論證結(jié)構(gòu)的有效性.接下來，我們的工作重點是如何將這種基于論證模式的目標符合性論證方法進一步應(yīng)用于DO-178C的其他過程目標論證以及其他安全性標準的目標論證工作中.

[1]RTCA. DO-178C software considerations in airborne systems and equipment certification[S]. Washington: RTCA Inc, 2011

[2]Kelly T, McDermid J. Safety case patterns—Reusing successful arguments[C]Proc of IEE Colloquium on Understanding Patterns & Their Application to Systems Engineering. London: IET, 1998

[3]Holloway C M. Explicate’78: Discovering the implicit assurance case in DO-178C[C]Proc of the 23rd Safety-Critical Systems Symp. North Charleston, South Carolina, USA: CreateSpace Independent Publishing Platform, 2015: 205-225

[4]Holloway C M. Towards understanding the DO-178CED-12C assurance case[C]Proc of the 7th IET Int Conf on System Safety, Incorporating the Cyber Security Conf. London: IET, 2012: 1-6

[5]Spriggs J. GSN—The Goal Structuring Notation: A Structured Approach to Presenting Arguments[M]. Berlin: Springer, 2012

[6]Hu Ning. Study on airworthiness concerns of changes of DO-178C[J]. Aeronautical Computing Technique, 2014, 44(4): 94-98 (in Chinese)(胡寧. 從DO-178C的新變化透視軟件適航關(guān)注點[J]. 航空計算技術(shù), 2014, 44(4): 94-98)

[7]Zhang Juncai, Wang Juan, Pan Wei, et al. Research on structural coverage analysis based on DO-178B[J]. Aeronautical Computing Technique, 2011, 41(4): 67-69 (in Chinese)(張軍才, 王娟, 潘衛(wèi), 等. 基于DO-178B的結(jié)構(gòu)覆蓋分析研究[J]. 航空計算技術(shù), 2011, 41(4): 67-69)

[8]Federal Aviation Administration (FAA). Order 8110.49 Software Approval Guidelines[S]. Washington: Federal Aviation Administration (FAA), 2003

[9]Basili V R, Caldiera G, Rombach H D. The goal question metric approach[J]. Encyclopedia of Software Engineering, 1994, 2: 528-532

[10]Object Management Group (OMG). Kernel and Language for Software Engineering Methods (Essence), Version 1.1[S]. Needham, MA: Object Management Group (OMG), 2015

[11]Goal Structuring Notation Working Group. GSN Community Standard, Version 1[S]. York: Origin Consulting (York) Limited, 2011

[12]Takai T, Kido H. A supplemental notation of GSN aiming for dealing with changes of assurance cases[C]Proc of 2014 IEEE Int Symp on Software Reliability Engineering Workshops. Piscataway, NJ: IEEE, 2014: 461-466

[13]Matsuno Y, Taguchi K. Parameterised argument structure for GSN patterns[C]Proc of the 11th Int Conf on Quality Software. Piscataway, NJ: IEEE, 2011: 96-101

[14]Alexander R, Kelly T, Kurd Z, et al. Safety cases for advanced control software: Safety case patterns, FA8655-07-1-3025[R]. York: Department of Computer Science, University of York, 2007

[15]quainzk. The implementation of lock in operating system[EBOL]. [2016-05-08]. http:blog.sina.com.cnsblog_75f0b54d0100r7af.html (in Chinese)(quainzk. 操作系統(tǒng)中鎖的實現(xiàn)原理[EBOL]. [2016-05-08]. http:blog.sina.com.cnsblog_75f0b54d0100r7af.html)

Yang Yang, born in 1991. Master. Her main research interests include safety certification and software engineering.

Wu Ji, born in 1974. Associate professor and PhD in Beihang University. Member of CCF. His main research interests include software safety, software engineering, software testing and requirement engineering.

Yuan Chunchun, born in 1985. PhD candidate in Beihang University. His main research interests include software engineering, software safety and software reliability (yccnankai@buaa.edu.cn).

Liu Chao, born in 1958. Professor and PhD supervisor in Beihang University. Senior member of CCF. His main research interests include software engineering, software safety and software testing (liuchao@buaa.edu.cn).

Yang Haiyan, born in 1974. Master and lecturer in Beihang University. Her main research interests include software engineering, software testing, software safety and requirement engineering (yhy@buaa.edu.cn).

Xing Liang, born in 1983. Engineer in Xi’an Aeronautics Computing Technique Research Institute, Aviation Industry Corporation of China. His main research interests include safety certification and software engineering (lionxing@163.com).

Objectives Conformity Argument Patterns for Software Testing Process in DO-178C

Yang Yang1, Wu Ji1, Yuan Chunchun1, Liu Chao1, Yang Haiyan1, and Xing Liang2

1(SchoolofComputerScienceandEngineering,BeihangUniversity,Beijing100191)2(Xi’anAeronauticsComputingTechniqueResearchInstitute,AviationIndustryCorporationofChina,Xi’an710068)

Safety-critical software has been widely used in many fields. As the specific requirement of safety-critical software is preventing catastrophes, this kind of software must comply with its relevant safety standards. But now it does not have any effective ways to construct objectives conformity argument model for standards. By analyzing the features of objectives of software testing process in DO-178C, an objective conformity argument pattern description framework based on GSN is proposed, and these patterns are described through four fields: the problems that we need to solve, the specification for the solution, the approach to use them and the effect after using them. At the same time, some extensions for safety case patterns are proposed to describe the objectives conformity argument patterns. On this basis, three objectives conformity argument patterns based on software testing process in DO-178C are proposed, which are code-requirement conformity argument pattern, test coverage of requirements argument pattern and test coverage of structure argument pattern. At the same time, the instantiated method to build the objectives conformity argument structure for a specific program based on these patterns is proposed. People can construct objectives conformity argument structure for objectives of software testing process in DO-178C effectively through the proposed way. At last, one case study, which is an embedded real-time operating system, indicates that the objectives conformity argument patterns proposed here are useful and effective.

safety-critical software; airworthiness certification; DO-178C; GSN; argument patterns

2015-12-09；

2016-11-04

吳際(wuji@buaa.edu.cn)

TP311