面向適航標(biāo)準(zhǔn)的機(jī)載軟件測試驗證工具綜述

劉友林，鄭 巍，譚莉娟，樊 鑫，楊豐玉

1.南昌航空大學(xué) 軟件學(xué)院，南昌330063 2.南昌航空大學(xué) 軟件測評中心，南昌330063

機(jī)載軟件是安裝在航空設(shè)備中作為核心控制作用的計算機(jī)軟件，是一種典型的嵌入式軟件。隨著嵌入式技術(shù)在航空航天領(lǐng)域的廣泛應(yīng)用，軟件所實現(xiàn)的功能比例也越來越高，航電系統(tǒng)80%的功能都依賴于機(jī)載軟件實現(xiàn)，機(jī)載軟件已經(jīng)成為機(jī)載設(shè)備系統(tǒng)的核心[1]，而因軟件故障引起的事故時有發(fā)生。2018年印尼獅航因為飛機(jī)搭載的自動防失速系統(tǒng)做出錯誤判斷導(dǎo)致空難。機(jī)載軟件具有安全攸關(guān)（safety-critical）的特性，因此所有機(jī)載設(shè)備軟件以及飛機(jī)交聯(lián)的軟件系統(tǒng)進(jìn)行安全認(rèn)證才能投入使用[2]。航空領(lǐng)域廣泛采用的是美國航空無線電委員會（Radio Technical Commission for Aeronautics，RTCA）提出的航空適航認(rèn)證標(biāo)準(zhǔn)DO-178C[3]及其增補(bǔ)標(biāo)準(zhǔn)。

基于適航認(rèn)證標(biāo)準(zhǔn)的軟件驗證能最大程度上發(fā)現(xiàn)軟件中的錯誤，保障軟件安全與質(zhì)量，滿足適航審定的要求。機(jī)載嵌入式軟件因其實時性、高安全可靠性和軟硬件高耦合度等特點，驗證的工作量和難度大大提升。如何對日漸復(fù)雜的機(jī)載軟件系統(tǒng)進(jìn)行高效的驗證成為了研究熱點，對機(jī)載嵌入式驗證工具的研究同樣也變得十分迫切。

DO-178C中軟件驗證的方法包括了審查（review）、測試和分析。而當(dāng)前，國內(nèi)外不少學(xué)者主要側(cè)重于軟件測試及其工具的研究。Sneha K等[4]按照功能導(dǎo)向?qū)y試工具劃分為功能測試工具、測試管理工具、負(fù)載測試工具三類；Mustafa K M等[5]根據(jù)測試工具的適用范圍將其劃分為web應(yīng)用、嵌入式軟件、數(shù)據(jù)庫、網(wǎng)絡(luò)協(xié)議等八類，但僅給出兩種適用于嵌入式軟件測試的工具。上述研究從不同角度對軟件測試及其工具進(jìn)行了研究，但是其主要研究對象并不是機(jī)載嵌入式軟件，而且覆蓋的工具也較少。因此本文在系列適航標(biāo)準(zhǔn)的基礎(chǔ)上對機(jī)載軟件的驗證工具進(jìn)行全面的研究綜述。

DO-178C及其增補(bǔ)標(biāo)準(zhǔn)包括了工具鑒定（DO-330）、基于模型的開發(fā)和驗證（DO-331）、面對對象技術(shù)（DO-332）、形式化方法（DO-333）、常溫問題的問答（DO-248）等，如圖1所示。面對對象技術(shù)（DO-332）到目前還沒廣泛應(yīng)用到航空業(yè)中，工具鑒定（DO-330）是機(jī)載軟件生命周期中所使用工具的適航審定標(biāo)準(zhǔn)，因此本文從DO-178C、模型驅(qū)動、形式化方法三個方面，介紹機(jī)載軟件測試驗證工具。

圖1 適航認(rèn)證標(biāo)準(zhǔn)

1 面向DO-178C的測試驗證工具

DO-178C是民用航空機(jī)載軟件研制和審定的指南標(biāo)準(zhǔn)，確保研制的軟件實現(xiàn)預(yù)期的功能和滿足適航的要求。DO-178C將軟件生命周期分為軟件計劃過程、軟件開發(fā)過程和軟件綜合過程，如圖2。針對每個過程，DO-178C規(guī)定了一些系列的指南，包括過程的目標(biāo)、達(dá)到目標(biāo)所需要的活動和設(shè)計考慮、證明目的已經(jīng)達(dá)到的證據(jù)。

圖2 DO-178C軟件生命周期

軟件計劃過程定義了軟件計劃和軟件標(biāo)準(zhǔn)，用來指導(dǎo)軟件開發(fā)和軟件綜合過程。軟件開發(fā)過程實現(xiàn)了軟件產(chǎn)品自上而下的生成。軟件綜合過程包含了驗證軟件產(chǎn)品、管理軟件產(chǎn)品和監(jiān)控軟件產(chǎn)品，以保證軟件產(chǎn)品及其生成過程的正確、受控和可信。軟件綜合過程中的軟件驗證過程不僅包含對軟件開發(fā)過程的驗證，還包括對軟件驗證過程輸出結(jié)果的驗證即對驗證的驗證。驗證是對軟件開發(fā)過程和軟件驗證過程結(jié)果的技術(shù)評估[3]。軟件驗證包括了評審（review）、分析、測試等方法，并通過不同的方法對不同的軟件過程進(jìn)行驗證。DO-178C將測試作為軟件驗證的一部分考慮，主要是對開發(fā)出的源代碼進(jìn)行評估，執(zhí)行測試用例以驗證代碼是否滿足了需求。在軟件需求不能用測試用例測試時，可以采用分析的方法驗證。

1.1 評審

評審?fù)ㄟ^檢查單或類似的方法進(jìn)行人工定性檢查，是早期發(fā)現(xiàn)問題的有效手段，通過評審可以發(fā)現(xiàn)其他方法難以發(fā)現(xiàn)的錯誤評。評審貫穿了軟件研發(fā)的生命周期，包括軟件需求、設(shè)計、代碼、測試用例、配置項管理等過程。評審工具主要包括各階段的評審檢查單和生命周期數(shù)據(jù)等文檔，設(shè)計合理充分的審查文檔是保證評審質(zhì)量的關(guān)鍵。

1.2 分析

軟件分析可用于檢查軟件部件的功能、性能、安全性等，是可重復(fù)、可自動化的。軟件分析的對象不僅僅是程序，還包括文檔等其他形態(tài)的軟件制品，如追蹤性分析、源代碼與目標(biāo)代碼的對應(yīng)分析等。程序分析與形式化方法聯(lián)系緊密，因此本文將其放在形式方法部分中歸納。

追蹤性分析即在系統(tǒng)需求、高層需求、底層需求、代碼、測試用例之間建立追蹤關(guān)系，并對追蹤關(guān)系進(jìn)行分析。追蹤性分析是為了確保需求測試的完整性，是軟件驗證活動的一部分，追蹤關(guān)系和分析結(jié)果均需保存在驗證報告中。軟件需求階段建立系統(tǒng)需求和軟件高層需求間的鏈接，軟件設(shè)計階段建立高層需求和底層需求間的鏈接，軟件編碼階段建立底層需求和代碼間的鏈接，集成過程建立測試和需求、設(shè)計間的鏈接。工業(yè)界常使用IBM Engineering Requirements Management DOORS等需求管理工具，手動創(chuàng)建和維護(hù)追蹤關(guān)系。該方法耗時長、成本高、維護(hù)較為困難。此外機(jī)載軟件規(guī)模大、復(fù)雜度高，人工的追蹤性分析不可避免地會存在問題。學(xué)術(shù)界對可追蹤性的研究主要集中在追蹤建立方法的研究上，并且大多數(shù)研究是在理論層面，基于相關(guān)理論的需求追蹤工具的設(shè)計與實現(xiàn)是追蹤性研究未來的主要工作之一[6]。

DO-178C（A7-9）指出機(jī)載軟件需要進(jìn)行源代碼到目標(biāo)代碼的追溯分析，以確保源代碼與目標(biāo)代碼的對應(yīng)關(guān)系，保證編譯器不會引入錯誤。源代碼和目標(biāo)代碼對應(yīng)分析最直接的方式是將源代碼與目標(biāo)碼逐步對比分析，檢測編譯過程是否引入錯誤。但是該方法受軟件研制過程影響大、分析成本高、工作量大。針對這種情況，上海愛韋訊提出了基于MISRA-2004的SCK-178語言安全子集，對安全子集內(nèi)符合編碼標(biāo)準(zhǔn)的參考代碼進(jìn)行了源代碼與目標(biāo)碼的追溯分析，確保子集內(nèi)的編碼標(biāo)準(zhǔn)在編譯環(huán)境不變的情況下不會引入錯誤。但是SCK-178安全子集尚無應(yīng)用實例，其有效性存疑。

1.3 測試

DO-178C基于需求提出了三種測試方法：低層需求測試、軟件集成測試、軟件/硬件集成測試。低層需求測試主要測試軟件是否滿足底層需求。軟件集成測試主要測試軟件組件間的內(nèi)部關(guān)系和軟件體系結(jié)構(gòu)。軟件/硬件集成測試檢查運行在目標(biāo)機(jī)硬件上的軟件是否滿足需求，并排查目標(biāo)硬件環(huán)境下可能出現(xiàn)的問題。DO-178C中的三種測試方法并不是自底向上、層層遞進(jìn)的關(guān)系，而是并列可選的關(guān)系即根據(jù)需求選擇某種方法進(jìn)行某項功能的測試。當(dāng)系統(tǒng)需求比較簡單，軟件/硬件集成測試或者軟件集成測試已經(jīng)覆蓋高層測試需求時，就沒必要進(jìn)行低層需求測試。

DO-178C還對測試的覆蓋性也提出了要求，包括需求覆蓋、軟件結(jié)構(gòu)覆蓋。需求覆蓋包括了高級測試需求和低級測試需求，軟件結(jié)構(gòu)覆蓋包括了語句覆蓋、判斷覆蓋、MC/DC覆蓋、數(shù)據(jù)耦合和控制耦合，測試流程如圖3所示。

圖3 測試流程圖

1.3.1 需求覆蓋

需求覆蓋最重要的部分是根據(jù)需求編寫的測試用例。測試用例自動生成、測試用例復(fù)用、測試用例優(yōu)化策略等技術(shù)一直在發(fā)展。文獻(xiàn)[7]基于馬爾可夫鏈定義系統(tǒng)模型并根據(jù)系統(tǒng)間狀態(tài)轉(zhuǎn)換的概率生成測試用例，系統(tǒng)間狀態(tài)轉(zhuǎn)換的概率會根據(jù)導(dǎo)致內(nèi)存泄露的測試路徑而迭代更新；文獻(xiàn)[8]提出基于線性融合的用戶協(xié)同過濾算法，有效地提高了測試用例推薦的精度，但是存在成本過高、泛化性等問題；文獻(xiàn)[9]提出基于測試用例錯誤傳播概率的測試用例優(yōu)先級度量，根據(jù)該度量選擇出的測試用例與Bug發(fā)現(xiàn)能力存在高相關(guān)性。但是根據(jù)軟件需求人工編寫測試用例仍是主要手段，相關(guān)技術(shù)與工具僅僅作為輔助。

1.3.2 結(jié)構(gòu)覆蓋

結(jié)構(gòu)覆蓋中的語句覆蓋、判斷覆蓋、MC/DC覆蓋是軟件測試中自動化程度較高的部分，是軟件測試工具主要的功能之一。本文結(jié)合DO-178C結(jié)構(gòu)覆蓋要求，選擇了市場上主流且具有實際項目支撐的測試工具，包括了Testbed、Cantata等，并對其進(jìn)行對比分析，如表1所示。

表1 測試覆蓋工具

LDRA（Liverpool Data Research Associates）公司推出以Testbed為核心的測試套件，適用于軟件開發(fā)、測試和維護(hù)等各個階段。目前，國內(nèi)各大航天航空企業(yè)、相關(guān)研究機(jī)構(gòu)均已引進(jìn)LDRA Testbed測試套件，作為主要的測試工具。北京航天自動控制研究所通過測試實例闡述Testbed在航空航天機(jī)載軟件測試中的應(yīng)用方案[10]；中航工業(yè)第一飛機(jī)設(shè)計研究院基于Testbed實現(xiàn)了機(jī)載航電系統(tǒng)綜合數(shù)據(jù)記錄系統(tǒng)的單元測試[11]。LDRA Testbed是第一個被用來證明空地系統(tǒng)符合DO-178B的工具，在機(jī)載軟件測試領(lǐng)域擁有深厚的經(jīng)驗，且已占據(jù)我國機(jī)載軟件測試工具主流市場，實際應(yīng)用項目較多，工具可信度高。LDRA還可提供資質(zhì)支持包來幫助客戶通過DO-178B/C的認(rèn)證。

Cantata[12]是QA SYSTEM公司研發(fā)的CC++代碼的單元與集成測試工具，除了常規(guī)的代碼覆蓋率分析等功能外，還有健壯性測試、測試驅(qū)動開發(fā)等其他工具很少采用的測試方法和覆蓋的功能。文獻(xiàn)[13]以DO-178C為依據(jù)，通過規(guī)格化的用例設(shè)計方法生成測試用例，借助Cantata批量自動執(zhí)行，發(fā)現(xiàn)的缺陷由13個增長至97個。

除此之外，還有Parasoft C/C++test[14]、VectorCAST[15]、Rapita Verification Suite[16]等測試工具，其綜合性較強(qiáng)，其功能基本滿足了DO-178C結(jié)構(gòu)覆蓋的要求，還涵蓋了一些如時間性能分析、結(jié)構(gòu)化分析等功能。但這些工具實際支撐項目較少，可信度未知。

1.3.3 耦合覆蓋

耦合分析包括了數(shù)據(jù)耦合和控制耦合，DO-248C給出了數(shù)據(jù)耦合和控制耦合的示例[17]，以便理解，如圖4所示。主函數(shù)調(diào)用了計算空速和空速顯示子程序，計算出的空速作為全局變量在兩個子程序間傳遞。主程序與子程序間存在控制耦合，子程序間存在數(shù)據(jù)耦合。耦合覆蓋是結(jié)構(gòu)覆蓋中特殊的一項。DO-178B中明確提出了耦合覆蓋的要求，DO-178C進(jìn)一步強(qiáng)調(diào)了耦合覆蓋的適航要求。但是適航標(biāo)準(zhǔn)中并沒有給出明確的覆蓋準(zhǔn)則，甚至沒有給出覆蓋準(zhǔn)則的指導(dǎo)思想。這使得耦合分析的開展比較困難，很難直接使用測試工具滿足覆蓋要求，需要綜合評審、分析和測試的方法，流程如圖5。

圖4 數(shù)據(jù)耦合和控制耦合示例

LDRA Testbed提供了控制流和數(shù)據(jù)流分析的功能，也可用于耦合分析。SA-Covalyzer[18]是針對耦合覆蓋分析研發(fā)的工具，自動識別部件間的耦合關(guān)系，推薦適用的覆蓋準(zhǔn)則，針對覆蓋點進(jìn)行低膨脹率的插樁，在測試過程中收集和統(tǒng)計覆蓋情況，對未覆蓋到的情形進(jìn)行輔助分析，并自動生成覆蓋分析報告。SA-Covalyzer是愛韋訊基于自身機(jī)載軟件驗證經(jīng)驗研制的工具，主觀性較大，尚未實例，其可信度與實用性存疑。

圖5 耦合分析流程

1.4 小結(jié)

國外嵌入式軟件測試驗證工具的研發(fā)起步早，一方面通過內(nèi)部版本的迭代優(yōu)化軟件的功能，另一方面通過收購、合并其他公司和產(chǎn)品壯大自身，如開發(fā)CodeTest的AMC（Applied Microsystems Corporation）最后被并入恩智浦公司；研發(fā)Logicscope的Telelogic公司被IBM收購，其產(chǎn)品逐漸成熟，占據(jù)了主要市場甚至達(dá)到了壟斷的地步。機(jī)載軟件的測試驗證工具作為一種工業(yè)軟件，其研發(fā)在國內(nèi)起步較晚，與國外仍有較大差距，發(fā)展水平與中國航空工業(yè)的發(fā)展速度不匹配。很多測試驗證工具的實驗性開發(fā)只能小范圍落地使用甚至止步于實驗室，缺乏用戶的使用反饋數(shù)據(jù)，不利于相關(guān)的經(jīng)驗積累和技術(shù)積淀，無法對軟件進(jìn)行更好的優(yōu)化，提高其綜合競爭力。國產(chǎn)機(jī)載軟件測試工具的發(fā)展落后存在多方面的原因。一是因為沒有明確的政策導(dǎo)向，缺乏扶持和資金支持；二是國外主流的測試工具基本壟斷了國內(nèi)市場，國產(chǎn)的軟件生存發(fā)展空間被壓縮；三是國內(nèi)工業(yè)軟件相應(yīng)的生態(tài)環(huán)境不成熟，用戶沒有使用國產(chǎn)機(jī)載測試工具的習(xí)慣。

2 面向模型驅(qū)動的測試驗證工具

2011年RTCA發(fā)布的DO-178C，正式將模型驅(qū)動的概念引入航空航天領(lǐng)域，并增補(bǔ)標(biāo)準(zhǔn)DO-331[19]對基于模型的機(jī)載軟件研發(fā)進(jìn)行規(guī)范和指導(dǎo)。DO-331基于DO-178C，僅對采用模型的開發(fā)和驗證的部分進(jìn)行增加和修改?；谀Ｐ偷尿炞C方式主要是測試，因此本章側(cè)重于基于模型的測試（Model-Based Testing，MBT）（圖6）及其相應(yīng)工具的研究。

圖6 基于模型測試的流程

隨著基于模型和以測試為中心的開發(fā)方法變得成熟，基于模型的測試也不斷在發(fā)展。文獻(xiàn)[20]梳理了近年來與MBT方法相關(guān)的文獻(xiàn)，重點選取了78篇論文，詳細(xì)分析了MBT方法的應(yīng)用領(lǐng)域、特點和局限性等，比較的標(biāo)準(zhǔn)包括表示模型、支持工具、測試覆蓋準(zhǔn)則等。

基于模型的測試是測試的一種變體，其依賴于明確的行為模型，該行為模型可以對被測系統(tǒng)的預(yù)期行為或者其環(huán)境進(jìn)行編碼[21]。MBT提供一種使用從軟件開發(fā)中提取的模型來自動生成測試用例的技術(shù)，以降低成本控制軟件質(zhì)量。大部分現(xiàn)有的MBT工具主要支持測試用例自動生成，可用于功能測試、性能測試和安全性測試等。借鑒文獻(xiàn)[22]提出的分類方法，從建模方法的維度將MBT工具分為基于狀態(tài)的建模、基于遷移的建模、基于統(tǒng)計概率的建模、基于數(shù)據(jù)流的建模。

2.1 基于狀態(tài)的建模

基于狀態(tài)建模的方法使用一組變量構(gòu)建模型，該變量表示系統(tǒng)執(zhí)行到特定點處的狀態(tài)，包括了前置條件和后置條件。前置條件定義了初始狀態(tài)集合，后置條件指定了最終可保證狀態(tài)的集合。每個操作都指定為前置或者后置關(guān)系。狀態(tài)建模的工具有Spec Explorer和基于Z語言的工具等。

Spec Explorer是微軟研發(fā)的基于模型測試的工具，常使用Spec#或者C#作為描述系統(tǒng)模型的語言。Spec#在C#的基礎(chǔ)上引入方法前置和后置條件、框架條件，對象不變式等形式化機(jī)制，并拓展了異常安全性、非空類型等用于提高程序可靠性的特性[23]。Spec Explorer對一個軟件系統(tǒng)的期望行為進(jìn)行建模，然后通過模型自動生成測試用例。模型可以用C#進(jìn)行開發(fā)，然后通過Cord語言腳本對模型進(jìn)行配置和裁剪，選擇測試中需要的場景，因此Spec Explorer能有效解決狀態(tài)爆炸的問題。文獻(xiàn)[24]使用Spec Explorer工具進(jìn)行測試，相較于手動測試，測試效率提高了42%。

Z語言是基于一階謂詞邏輯和集合論的形式規(guī)格說明語言[25]。Z語言具有一種特殊的圖形方式（Scheme），主要由兩部分組成：一是聲明部分，定義各種變量的類型；另一個是謂詞表達(dá)式。謂詞表達(dá)式可以推理出所描述軟件的所有狀態(tài)行為。文獻(xiàn)[26]給出了基于Z規(guī)格說明的測試用例自動生成的方法和框架。文獻(xiàn)[27]研究了從Object-Z規(guī)格說明中產(chǎn)生測試用例的自動化過程，并在此基礎(chǔ)上設(shè)計實現(xiàn)了相應(yīng)的測試工具。Object-Z是在Z語言基礎(chǔ)上增加了面對對象的封裝和繼承的描述能力。

2.2 基于遷移的建模

基于遷移建模的方法假設(shè)系統(tǒng)在某個時刻總處于某個狀態(tài)并且當(dāng)前的狀態(tài)決定了系統(tǒng)可能的輸入，而且從該狀態(tài)遷移到其他狀態(tài)的遷移決定于當(dāng)前的輸入。遷移建模對應(yīng)的工具有TestMaster和基于統(tǒng)一建模語言（United Modeling Language，UML）的工具等。

TestMaster[28]基于擴(kuò)展有限狀態(tài)機(jī)來建立系統(tǒng)模型，并基于識別可遷移的輸入序列來生成測試用例。每個生成的輸入序列代表被測系統(tǒng)的一個測試用例，并且該工具還可以根據(jù)用戶指定的路徑覆蓋方案生成測試用例。TestMaster使用基本圖遍歷算法的組合，如深度優(yōu)先搜索、寬度優(yōu)先搜索和最小生成樹等，來導(dǎo)出EFSM的路徑。

想想佛羅倫薩、巴黎、倫敦、紐約。第一次去這些城市的人也不會覺得它們陌生，因為他已經(jīng)在繪畫、小說、歷史書和電影中去過這些地方了……格拉斯哥對我們多數(shù)人來說是什么？一所房子、工作的地方、足球或高爾夫球場、幾家酒吧和縱橫的街道。就這些。不，我錯了，還有電影院和圖書館?！窭垢缭谌藗兊挠∠笾兄皇且魳窂d里的一首歌和幾本糟糕的小說。（Gray 2002：243；以下此書引用僅標(biāo)注頁碼）格拉斯哥已經(jīng)一無是處，等待它的只能是“死亡”。

基于UML的軟件測試已經(jīng)取得一定成果，包括基于UML各種圖元的軟件測試研究[29-31]、基于UML的軟件可靠性測試與評估[32-33]等。文獻(xiàn)[34]研制了基于UML的軟件測試的工具Cow-Suite，該工具首先根據(jù)UIT（Use Interaction Testing）方法生成測試用例，再從生成的測試用例中選擇合適的用例執(zhí)行；文獻(xiàn)[35]開發(fā)的驗證性測試用例工具UMLTest，實現(xiàn)了對Rational Rose模型文件的解析，生成狀態(tài)圖并根據(jù)相應(yīng)的測試準(zhǔn)則產(chǎn)生測試用例；文獻(xiàn)[36-37]定義了加入統(tǒng)計測試約束的UML用例圖、序列圖以及用例執(zhí)行順序關(guān)系的形式化描述，并在其基礎(chǔ)上給出從UML模型構(gòu)造馬爾可夫鏈模型的算法，還設(shè)計實現(xiàn)了相關(guān)工具。

UML具有很好的面向?qū)ο笮院拓S富的建模表達(dá)能力，但是UML在非功能屬性的表達(dá)上比較欠缺?；赨ML的測試相關(guān)研究已經(jīng)比較成熟，但是大多數(shù)集中于理論方面，對其相關(guān)工具的研發(fā)大幅度滯后，導(dǎo)致其使用門檻也居高不下，無法規(guī)?；赝茝V使用。

2.3 基于統(tǒng)計概率的建模

基于統(tǒng)計概率的建模對應(yīng)的工具有MaTeLo Testing Tool（MTT），該工具使用馬爾可夫鏈建模。馬爾可夫鏈?zhǔn)且环N以統(tǒng)計理論為基礎(chǔ)的統(tǒng)計模型，其本質(zhì)是一種具有概率特征的有限狀態(tài)機(jī)，不僅可以根據(jù)狀態(tài)間遷移概率自動產(chǎn)生測試用例，還可以分析測試結(jié)果，對軟件性能指標(biāo)和可靠性指標(biāo)等進(jìn)行度量。文獻(xiàn)[38]利用缺陷關(guān)聯(lián)信息擴(kuò)展受控Markov鏈模型，以缺陷的三種屬性作為決策選取權(quán)值，將測試過程看做帶權(quán)最優(yōu)路徑求解問題，優(yōu)化測試策略。

MTT是在MaTeLo[39]（Markov Test Logic）項目中開發(fā)的工具。該工具使用馬爾可夫鏈建模，從被測軟件的預(yù)期使用中生成測試用例。MTT關(guān)注的不是需求覆蓋，而是覆蓋被測軟件的所有使用路徑，以便檢測使用中可能出現(xiàn)的關(guān)鍵故障。

2.4 基于數(shù)據(jù)流的建模

在基于模型的設(shè)計使用中，數(shù)據(jù)流模型是嵌入式系統(tǒng)中軟件開發(fā)與測試中常用的模型?；跀?shù)據(jù)流模型的模型有Simulink Verification and Validation（SVAV）[40]和GAtel[41]。

SVAV提供包括IEC 61508等在內(nèi)的行業(yè)規(guī)范的檢查，還可以創(chuàng)建自定義檢查標(biāo)準(zhǔn)。SVAV還可用于模型和代碼覆蓋率分析，以衡量模型和生成的代碼的測試完整度。GAtel主要目的是根據(jù)以Luster語言編寫的規(guī)范自動生成測試用例，Lustre是應(yīng)用于關(guān)鍵應(yīng)用程序的同步語言，具有語義形式化和模塊化的特點。

2.5 小結(jié)

在對MBT的認(rèn)知上，學(xué)術(shù)界與業(yè)界脫節(jié)較為嚴(yán)重。學(xué)術(shù)界對MBT研究比較廣且深入，認(rèn)為MBT已經(jīng)成熟到可以較大規(guī)模應(yīng)用，也開發(fā)了不少的原型工具投入使用，但是工業(yè)界不少測試從業(yè)者不了解MBT，MBT的商業(yè)化工具也僅有少量的研發(fā)，MBT在業(yè)界的應(yīng)用仍處于起步狀態(tài)。一是因為測試模型的選擇、構(gòu)建大多還是以經(jīng)驗為基礎(chǔ)，且要求使用者具備建模語言、形式化方法等相關(guān)知識，知識儲備要求高，建模自動化程度低，工具開發(fā)難度大，使用門檻高；二是MBT不支持安全性、可靠性以及性能等方面的測試，功能比較單一；三是MBT通常不能與軟件開發(fā)環(huán)境集成，還缺少版本控制、模型試調(diào)等上下游工具鏈的支持。上述都是MBT科研成果向工業(yè)化、商業(yè)化產(chǎn)品轉(zhuǎn)化過程中亟待克服的難題。

3 面向形式化方法的測試驗證工具

形式化方法是一種建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上的用于設(shè)計、規(guī)范和驗證的方法，廣泛地應(yīng)用在軟硬件、通信協(xié)議、嵌入式控制系統(tǒng)等方面[42]。DO-178C及其增補(bǔ)的DO-333首次正式將形式化方法引入到航空機(jī)載軟件開發(fā)領(lǐng)域并確定了其有效性。文獻(xiàn)[43]采用形式化方法對機(jī)載安全等級依賴的合法性進(jìn)行了分析，文獻(xiàn)[44]面向適航標(biāo)準(zhǔn)采用形式化方法對機(jī)載襟縫翼控制單元進(jìn)行安全性分析。

形式化方法是由形式化語言、形式化規(guī)約、形式化驗證等形成的整體[45]，其中形式驗證的方法主要有模型檢測、定理證明等。

3.1 模型檢測

模型檢測的基本思想是將一個過程或者系統(tǒng)抽象成有窮的狀態(tài)模型，加以分析驗證[46]。模型檢測的自動化驗證依賴于有效的軟件工具的支持，本文選取了部分典型的模型檢測工具SPIN[47]、UPPAAL[48]、CMBC[49]進(jìn)行了對比，如表2所示。美國噴氣推進(jìn)實驗室設(shè)計了SPIN模型檢查器，對火星探測器的控制系統(tǒng)進(jìn)行了驗證[50]；文獻(xiàn)[51]使用UPPAAL的衍生品UPPAAL-TRON對實時嵌入式系統(tǒng)進(jìn)行黑盒一致性測試；文獻(xiàn)[52]使用CBMC工具自動化驗證程序覆蓋率并應(yīng)用在鐵路系統(tǒng)中。除此之外還有很多模型檢測工具被廣泛地應(yīng)用在軟硬件的驗證上，如SMV[53]、SLAM[54]等。

表2 模型檢測工具

模型檢測因為自動化程度相對較高，被廣泛地應(yīng)用在航空航天、軌道交通等領(lǐng)域。但是當(dāng)模型檢測在驗證一些狀態(tài)比較復(fù)雜的系統(tǒng)時，會出現(xiàn)空間爆炸的問題。目前，模型檢測的主要研究方向就是如何減輕空間爆炸帶來的影響。

3.2 定理證明

定理證明的基本思想是選定某個公理化系統(tǒng)，將驗證的代碼進(jìn)行形式化描述為該系統(tǒng)的邏輯表述，利用公理與推理規(guī)則構(gòu)造對程序的證明。本文選取了ACL2[55]和PVS[56]兩個定理證明器進(jìn)行了對比研究，如表3所示。

表3 定理證明工具

ACL2已被用來驗證各種系統(tǒng)，如Sum公司的JAVA虛擬機(jī)系統(tǒng)，浮點單元、全真模擬系統(tǒng)等[57]；PVS被用于證明AAMP5處理器的正確性，該處理器被航空公司用于飛行控制[58]。定理證明工具還有Isabelle[59]、COQ[60]等。

定理證明可以有效地避免空間爆炸問題，但是因其自動化程度較低，對使用者的邏輯及數(shù)學(xué)知識儲備要求較高，限制了定理證明在工業(yè)界的應(yīng)用。目前，定理證明的研究方向主要是提高定理證明的自動化程度和自動化效率。

形式化驗證還有抽象解釋[61]、約束求解[62]、符號執(zhí)行[63]等。

3.3 程序分析

軟件分析是對軟件進(jìn)行自動化分析，以驗證、確認(rèn)或發(fā)現(xiàn)軟件的某種性質(zhì)、規(guī)約或者約束[64]。軟件分析的對象不僅僅包括代碼，還包括文檔等其他形態(tài)的軟件制品，本節(jié)軟件分析所涉及的對象主要是程序。程序分析需要給出正確的程序不變性，而形式化驗證只需要檢查給定的程序不變性是否正確[65]。兩者有嚴(yán)格的定義，但是在實際場景中混用比較多，文獻(xiàn)[66]便將部分形式化驗證方法作為程序分析的理論基礎(chǔ)，如圖7所示。

圖7 主要程序分析技術(shù)

程序分析可分為靜態(tài)分析技術(shù)和動態(tài)分析技術(shù)，而靜態(tài)分析又包括基本分析技術(shù)、基于形式化的分析技術(shù)和其他分析技術(shù)[67]。

基本分析技術(shù)包括語法分析、類型分析、數(shù)據(jù)流分析、控制流分析等?；痉治黾夹g(shù)發(fā)展比較成熟，應(yīng)用也比較廣泛。基于詞法分析的ITS4、Rats，基于語義分析的PC-lint[68]，基于規(guī)則檢查的Helix QACC++、Metal[69]，基于數(shù)據(jù)流分析的CppCheck、騰訊Tscancode，基于控制流分析和結(jié)構(gòu)分析的Klocwork，基于規(guī)則檢查和語義分析的北京關(guān)鍵科技EagleEye、Splint[70]，基于數(shù)據(jù)流分析和字節(jié)流分析的findbugs，基于數(shù)據(jù)流、控制流分析和代碼結(jié)構(gòu)分析的Fortify SCA等。

融合多技術(shù)進(jìn)行代碼驗證是近年來的發(fā)展趨勢之一，其中CPAchecker[71]是影響最為廣泛的工具，該工具將模型檢測與抽象解釋進(jìn)行結(jié)合。主流的軟件安全分析與檢測工具，如PolySpace、Coverity Prevent、CodeSonar等，基本都是多技術(shù)融合的產(chǎn)物。

具有獨立自主知識產(chǎn)權(quán)的國產(chǎn)商業(yè)安全分析與缺陷檢測工具的發(fā)展逐漸成熟，填補(bǔ)了我國缺陷檢測、安全漏洞檢測工具上的空白。CoBOT是北京大學(xué)軟件工程中心研發(fā)團(tuán)隊打造的國內(nèi)首款具有獨立自主產(chǎn)權(quán)的代碼安全類檢測工具，打破了國外產(chǎn)品在軟件缺陷檢測和安全漏洞分析領(lǐng)域的壟斷。SpecCheck是北京軒宇開發(fā)的缺陷檢測工具，支持安全編碼標(biāo)準(zhǔn)符合性檢查、運行時缺陷檢測和代碼質(zhì)量度量等。源傘科技的Pinpoint[72-73]是由香港科技大學(xué)孵化的一款商業(yè)化程度較高的靜態(tài)缺陷分析工具，其服務(wù)對象覆蓋了互聯(lián)網(wǎng)、航天軍工、通訊等行業(yè)。本文對上述軟件安全分析與缺陷檢測工具進(jìn)行簡要介紹與對比，如表4所示。

表4 安全分析與缺陷檢測工具

3.4 小結(jié)

機(jī)載軟件安全關(guān)鍵的特性要求從設(shè)計、需求到軟件開發(fā)的每個階段都要為機(jī)載軟件的安全性與可靠性提供保證，測試與驗證是其中的重要方法。當(dāng)前測試仍是保證軟件可靠性的主要且有效的手段，但是隨著可靠性的增長，通過測試發(fā)現(xiàn)下一個bug的時間越來越長即可靠性增長相對于測試時間和代價是數(shù)量級。而在公理系統(tǒng)、驗證工具正確的前提下，形式化方法能夠嚴(yán)格保證軟件符合其形式化規(guī)約。如果其形式化規(guī)約足夠全面，則代碼具有很高的可靠性。實際上，測試與驗證往往是交錯進(jìn)行的。形式化方法對于提高軟件質(zhì)量的作用已經(jīng)形成了共識，但是形式化方法的發(fā)展與應(yīng)用同樣存在困難。一是缺乏明確的規(guī)約或規(guī)格說明。大部分需求是非形式化描述的，并且分布在代碼的各處。二是驗證的粗粒度問題。粗粒度的驗證會導(dǎo)致代碼中仍存在bug，可靠性不高，細(xì)粒度的驗證工作量大、成本高，并且非形式化的規(guī)約不好細(xì)化。

4 總結(jié)

本文按照適航標(biāo)準(zhǔn)系列文檔，從DO-178C、基于模型的開發(fā)與驗證、形式化方法的角度對工具的功能、特性及應(yīng)用進(jìn)行了詳細(xì)介紹并對其發(fā)展現(xiàn)狀進(jìn)行小結(jié)。在對機(jī)載軟件的測試與驗證工具研究過程中，發(fā)現(xiàn)了以下問題并給出相應(yīng)的建議。

（1）國產(chǎn)軟件測試工具的競爭力弱，軟件生命周期各個階段的配套測試工具比較匱乏。具有獨立知識產(chǎn)權(quán)且競爭力較強(qiáng)的測試工具，基本上是技術(shù)含量較低的缺陷管理工具、測試管理工具。國產(chǎn)自主化的功能性、安全性等方面的測試工具研發(fā)還處于起步狀態(tài)，大部分市場份額被一些國外主流工具占據(jù)。縮小我國在工具研發(fā)等方面與國外之間差距，關(guān)鍵是加快建設(shè)國內(nèi)科研-工業(yè)-商業(yè)的轉(zhuǎn)化體系，在得到大量使用反饋之后優(yōu)化測試驗證工具，進(jìn)一步提高國產(chǎn)測試驗證工具的競爭力。

（2）大多數(shù)適用于機(jī)載軟件測試的工具均支持國際民用航空適航標(biāo)準(zhǔn)DO-178B/C的驗證，但是很少支持國內(nèi)的標(biāo)準(zhǔn)，如GJB 2786A—2009（軍用軟件開發(fā)通用要求）、SJ 21141.1—2016（軍用軟件C/C++編程要求）、中國民航總局（CCAC）的CCAR 25.1309（民航設(shè)備、系統(tǒng)、安裝方面的安全性要求）等。隨著我國航空工業(yè)的發(fā)展，軍用機(jī)載軟件適航要求的提出和民用航空行業(yè)的開放，探索國際適航標(biāo)準(zhǔn)與我國軍用、民用機(jī)載軟件標(biāo)準(zhǔn)體系融合的方法、研發(fā)支持國際適航標(biāo)準(zhǔn)和國內(nèi)標(biāo)準(zhǔn)的測試工具勢在必行。

在對機(jī)載軟件的測試驗證工具研究過程中，還總結(jié)了一些關(guān)于機(jī)載軟件測試驗證及其工具研發(fā)的發(fā)展趨勢。

（1）測試工具的集成化與一體化。單一化功能的測試工具以插件的形式集成到大型的測試工具中，一些市場上主流的測試工具被收購后集成到開發(fā)測試驗證一體化的工具中，還有諸如DevOps、云測試等集成概念的提出以及實踐，都反映了工具集一體化的趨勢。不僅僅是測試工具，基本上所有的軟件工具的研發(fā)都呈現(xiàn)集成化、一體化的趨勢。

（2）人工智能與軟件測試的融合發(fā)展更加緊密，智能化測試技術(shù)快速發(fā)展。基于深度神經(jīng)網(wǎng)絡(luò)的測試用例生成、軟件缺陷預(yù)測與修復(fù)和基于知識圖譜的測試用例推薦等都是智能化測試研究的熱點。而人機(jī)交互智能的進(jìn)一步發(fā)展，可能幫助計算機(jī)提高認(rèn)知，實現(xiàn)從感知向認(rèn)知演化，實現(xiàn)真正意義上的智能化自動測試。

（3）對適航標(biāo)準(zhǔn)中新增的形式方法和模型驅(qū)動技術(shù)的進(jìn)一步研究。一方面，形式化方法與模型驅(qū)動工程的自動化研究及工具研發(fā)，能降低其使用門檻，提高易用性和擴(kuò)展性，能夠更好應(yīng)用于保障機(jī)載軟件的安全性與可靠性分析中；另一方面，人工智能技術(shù)與形式化方法交叉研究也是重要的課題，如基于神經(jīng)網(wǎng)絡(luò)的分析與驗證、大數(shù)據(jù)程序的錯誤分析等。

（4）隨著工具在機(jī)載軟件研發(fā)過程中更加廣泛的使用，為保障機(jī)載軟件的安全性，針對工具的鑒定也會更加細(xì)化和嚴(yán)格。DO-178B僅將工具進(jìn)行簡單劃分，并沒有對工具鑒定有特定的要求。而DO-178C中不僅修訂了工具類的劃分，還給出了嚴(yán)格的審定認(rèn)證條件，使得工具的鑒定更加客觀。機(jī)載軟件的不斷演化和測試驗證的實踐中的反饋，使得工具鑒定的審定條件也不斷在調(diào)整、更新。