航天嵌入式軟件數(shù)據(jù)訪問沖突基準(zhǔn)測試集研究

陳睿，楊孟飛

1.北京控制工程研究所，北京100190 2.北京軒宇信息技術(shù)有限公司，北京100190 3.中國空間技術(shù)研究院，北京100094

?

航天嵌入式軟件數(shù)據(jù)訪問沖突基準(zhǔn)測試集研究

陳睿1，2，楊孟飛3，*

1.北京控制工程研究所，北京100190 2.北京軒宇信息技術(shù)有限公司，北京100190 3.中國空間技術(shù)研究院，北京100094

針對數(shù)據(jù)訪問沖突問題的檢測方法及工具的研究很多，但缺少對其進行評估的基準(zhǔn)測試集。文章基于大量真實航天嵌入式軟件中斷數(shù)據(jù)訪問沖突案例研究的結(jié)果，總結(jié)出影響數(shù)據(jù)訪問沖突檢測的6類要素，設(shè)計開發(fā)了嵌入式軟件中斷數(shù)據(jù)訪問沖突基準(zhǔn)測試集程序RaceBench，對SpaceDRC工具進行了指標(biāo)評估。結(jié)果表明，RaceBench能夠有效評估工具的適用性。

數(shù)據(jù)訪問沖突；基準(zhǔn)測試集；航天嵌入式軟件；數(shù)據(jù)競爭；軟件測試

數(shù)據(jù)訪問沖突問題是嵌入式軟件中一類典型的并發(fā)缺陷，曾經(jīng)引發(fā)嚴(yán)重的安全事故[1-2]，也是當(dāng)前航天型號軟件開發(fā)中最難解決的問題之一[3]。在學(xué)術(shù)領(lǐng)域或工程領(lǐng)域，數(shù)據(jù)競爭(Data Race)、原子性問題、數(shù)據(jù)訪問沖突或共享數(shù)據(jù)問題都屬于這一概念。這類問題發(fā)生在中斷驅(qū)動型程序或多任務(wù)程序中，當(dāng)兩個不同的中斷(或任務(wù))對同一個共享數(shù)據(jù)進行同時的讀寫訪問，且至少存在一次寫操作時。由于兩次訪問的時序不可確定，程序會因此產(chǎn)生異常行為，如關(guān)鍵數(shù)據(jù)被非預(yù)期地修改，嚴(yán)重時甚至導(dǎo)致系統(tǒng)或軟件失效。例如，某衛(wèi)星翼板驅(qū)動線路盒轉(zhuǎn)角跳變導(dǎo)致控制偏差等。根據(jù)數(shù)據(jù)統(tǒng)計，近五年在中國衛(wèi)星總裝集成測試階段發(fā)現(xiàn)的軟件質(zhì)量問題中，超過13%都與數(shù)據(jù)訪問沖突問題密切相關(guān)。這些問題一旦遺漏至實際飛行階段，后果將不堪設(shè)想。

值得注意的是，數(shù)據(jù)訪問沖突問題發(fā)生概率小、難以復(fù)現(xiàn)，往往在特殊的外部條件和中斷(或任務(wù))交迭情況下才會出現(xiàn)，難以通過傳統(tǒng)的軟件測試方法發(fā)現(xiàn)，遺漏率較高。因此，近年來數(shù)據(jù)訪問沖突自動檢測方法已成為研究熱點，國家自然科學(xué)基金“可信軟件基礎(chǔ)研究”重大研究計劃及民用航天預(yù)先研究等都先后資助了相關(guān)課題，產(chǎn)生了一批有價值的方法或工具成果[4-13]，隨著研究的不斷深入，未來還將產(chǎn)生更多的成果。

不同的數(shù)據(jù)訪問沖突檢測方法或工具在實際代碼中應(yīng)用時，檢出率、誤報率、性能等技術(shù)指標(biāo)存在較大差異。一方面，在工程實踐中選取合適的工具時需要一個統(tǒng)一的評價標(biāo)準(zhǔn)進行指導(dǎo)；另一方面，工具的研究設(shè)計者也希望了解自己的成果在工程實踐中的適用性及與其他競爭成果的優(yōu)劣比較，為進一步改進研究提供指導(dǎo)。

基準(zhǔn)測試集是一種有效、低成本的評估和度量手段。一個獲得廣泛認(rèn)可的基準(zhǔn)測試集具有重要的技術(shù)價值和社會影響。目前有很多應(yīng)用廣泛的標(biāo)準(zhǔn)測試集，如用于性能評估的SPEC[14]和TPC[15]系列。對于代碼缺陷檢測，近年來也出現(xiàn)一些基準(zhǔn)測試集，如BegBunch[16]，BugBench[17]及美國國家標(biāo)準(zhǔn)技術(shù)研究院的SAMATE SRD項目[18]。這些基準(zhǔn)測試集都基于開源軟件建立，多面向非嵌入式程序和通用類型缺陷，由于數(shù)據(jù)訪問沖突問題的特殊性及嵌入式軟件的封閉性和多樣性，并不能用于評估針對數(shù)據(jù)訪問沖突的檢測工具。

因此本文對航天嵌入式軟件數(shù)據(jù)訪問沖突基準(zhǔn)測試集開展研究，通過對大量真實案例的系統(tǒng)研究得出6類影響數(shù)據(jù)訪問沖突檢測的關(guān)鍵要素，基于此設(shè)計開發(fā)了已知首個中斷數(shù)據(jù)訪問沖突基準(zhǔn)測試集RaceBench，該基準(zhǔn)測試集的構(gòu)建遵循代表性、多樣性、公平性和適應(yīng)性原則。本文基于RaceBench對一個已有的數(shù)據(jù)競爭檢測工具SpaceDRC進行評估，驗證了該基準(zhǔn)測試集能夠有效評估工具的檢出率和誤報率等指標(biāo)。我們計劃未來公開RaceBench的源代碼，可為其他研究中斷數(shù)據(jù)訪問沖突問題的學(xué)者提供開放的測試集。

1 中斷數(shù)據(jù)訪問沖突問題要素

本文對大量真實航天嵌入式軟件數(shù)據(jù)訪問沖突案例進行系統(tǒng)分析，綜合檢測技術(shù)、軟件特征、缺陷特征等多種因素，提煉出數(shù)據(jù)訪問沖突問題的關(guān)鍵要素，作為構(gòu)建基準(zhǔn)測試集的基礎(chǔ)。

本節(jié)對問題特征分析的方法學(xué)和結(jié)果進行說明。

1.1 案例分析方法概述

首先，對航天嵌入式軟件第三方評測問題庫、第三方評測遺漏問題庫和北京控制工程研究所軟件問題案例進行了分析，通過關(guān)鍵字查詢的方式初步篩選出124個相關(guān)缺陷。經(jīng)過進一步的去重和精化，最終獲得100個樣本缺陷。

然后，進行缺陷特征信息采集，包括：1)確定與缺陷特征與統(tǒng)計分析相關(guān)的因素，包括軟件名、運行環(huán)境、并發(fā)體系結(jié)構(gòu)、規(guī)模、問題，描述、代碼片段、共享數(shù)據(jù)類型、問題處理方式；2)設(shè)計相應(yīng)的表格收集缺陷信息。缺陷特征信息的收集是一個迭代的過程，在此過程中，需要查看問題管理系統(tǒng)中的問題描述、定位代碼，比對獲取后續(xù)版本的修改策略。

最后，經(jīng)過統(tǒng)計分析，得出特征結(jié)果。

1.2 數(shù)據(jù)訪問沖突問題要素

經(jīng)案例分析得出，數(shù)據(jù)訪問沖突問題有軟件特征和缺陷特征兩方面的要素，如圖1所示。其中，軟件特征包括并發(fā)體系結(jié)構(gòu)、開發(fā)語言及運行環(huán)境等；缺陷特征包括并發(fā)關(guān)系、數(shù)據(jù)訪問方式、共享數(shù)據(jù)的類型、控制流場景和缺陷模式。

1.2.1 要素1：軟件并發(fā)體系結(jié)構(gòu)

數(shù)據(jù)訪問沖突是一種典型的并發(fā)缺陷，軟件的并發(fā)體系結(jié)構(gòu)與缺陷檢測之間存在直接的關(guān)系。航天嵌入式軟件是典型的強實時系統(tǒng)，且存在多種并發(fā)方式。主要采用兩種并發(fā)體系結(jié)構(gòu)：

(1)主循環(huán)+中斷結(jié)構(gòu)(Round-Robin with Interrupts)

在簡單輪詢式結(jié)構(gòu)的基礎(chǔ)上引入中斷，稱為主循環(huán)+中斷結(jié)構(gòu)(Round Robin with Interrupts，RRI)。在這種結(jié)構(gòu)下，緊急任務(wù)可以在中斷服務(wù)程序中得到處理，某些情況下可能在中斷中設(shè)置標(biāo)志，在主循環(huán)中完成后續(xù)處理，圖2給出了一個RRI架構(gòu)的示例程序。主循環(huán)+中斷結(jié)構(gòu)提高了對高優(yōu)先級任務(wù)的響應(yīng)能力，但與此同時，引入了新的問題，即共享數(shù)據(jù)的訪問沖突。如果中斷在使用共享變量進行計算的過程中發(fā)生，并且修改了共享變量的值，則會導(dǎo)致數(shù)據(jù)訪問沖突問題。這種情況下，必須采取措施保護低優(yōu)先級計算過程的原子性，例如通過中斷屏蔽方式保護臨界代碼段。

(2)實時多任務(wù)操作系統(tǒng)+中斷結(jié)構(gòu)

隨著航天嵌入式系統(tǒng)功能越來越復(fù)雜，軟件的模塊和規(guī)模越來越大，使用實時多任務(wù)操作系統(tǒng)(Real Time Operating System，RTOS)逐漸變得普遍。在基于RTOS的應(yīng)用程序中，沒有主循環(huán)，通過創(chuàng)建新任務(wù)可以實現(xiàn)主循環(huán)的功能。由于航天嵌入式系統(tǒng)對外部事件響應(yīng)的實時性要求高、與外界交互多，一般在RTOS中也引入中斷，用于處理非常關(guān)鍵的外部事件，形成一種異構(gòu)的并發(fā)體系結(jié)構(gòu)，本文稱之為RTOS-ISR。在這種并發(fā)結(jié)構(gòu)中，高優(yōu)先級和低優(yōu)先級任務(wù)之間可以對稱交迭，但中斷與任務(wù)的搶占關(guān)系是非對稱的，即只有中斷可以搶占任務(wù)，反之則不行。

(3)并發(fā)體系結(jié)構(gòu)分布分析

根據(jù)案例分析數(shù)據(jù)統(tǒng)計，并發(fā)體系結(jié)構(gòu)為RR-ISR的缺陷占82%，RTOS-ISR占18%。這種差異主要是由于航天嵌入式軟件本身采用的并發(fā)體系結(jié)構(gòu)分布導(dǎo)致的。需要注意的是，RTOS-ISR結(jié)構(gòu)的程序呈上升趨勢，為研究帶來新的問題。本文在構(gòu)建基準(zhǔn)測試集時考慮到了這種統(tǒng)計差異。

1.2.2 要素2：軟件形態(tài)及運行環(huán)境

軟件形態(tài)包括編程語言和軟件規(guī)模兩個方面。

一般而言，無論是動態(tài)還是靜態(tài)的檢測工具都依賴于被測軟件的編程語言，其中動態(tài)工具需要對源代碼進行插樁以獲取運行時信息，靜態(tài)工具直接面向源程序。在本文所研究的案例中，95%的軟件采用C語言編程，其余采用相應(yīng)體系架構(gòu)(如SPARC、x86等)的匯編語言，語法及特征并不統(tǒng)一，因此本文研究的基準(zhǔn)測試集僅考慮C語言程序。

軟件規(guī)模從數(shù)百行到上萬行不等，并發(fā)流個數(shù)與體系結(jié)構(gòu)相關(guān)，中斷服務(wù)程序少于5個。

航天嵌入式軟件的硬件運行環(huán)境多樣，以SPARC、x86、MCS-51、DSP等體系結(jié)構(gòu)的處理器為主。中斷并發(fā)機制與處理器架構(gòu)相關(guān)，多為固定優(yōu)先級非對稱搶占，各種處理器都有類似的中斷屏蔽機制實現(xiàn)中斷并發(fā)的互斥。

表1給出了案例在不同處理器上的分布數(shù)據(jù)。其中，68%的缺陷發(fā)生在8051平臺上，這類軟件多為中小規(guī)模。同時，隨著SPARC處理器及DSP處理器在航天領(lǐng)域的廣泛應(yīng)用，在中大規(guī)模的軟件中該類缺陷也逐漸增多。

表1 數(shù)據(jù)訪問沖突缺陷處理器分布

1.2.3 要素3：共享數(shù)據(jù)類型及訪問方式

共享數(shù)據(jù)的類型是影響中斷數(shù)據(jù)訪問沖突檢測的關(guān)鍵因素。不同數(shù)據(jù)類型的共享數(shù)據(jù)在沖突方式上表現(xiàn)不同，例如結(jié)構(gòu)體變量的沖突多發(fā)生在不同成員訪問的不一致性，數(shù)組變量的沖突發(fā)生在不同元素訪問中，因此對檢測工具的能力要求也不同。目前航天嵌入式軟件并發(fā)問題中表現(xiàn)出的沖突變量類型包括：

1)基本類型：共享數(shù)據(jù)為int、short、double等多字節(jié)基本類型，對這類變量的沖突發(fā)生在單個變量單次訪問、單個變量多次訪問或者多個變量一致性訪問等幾種情況中。基本類型的數(shù)據(jù)也包括對I/O端口的訪問。

2)數(shù)組：共享數(shù)據(jù)的類型為數(shù)組。當(dāng)按照一定順序依次訪問數(shù)組多個元素時，可能發(fā)生多個元素訪問不一致的情況。

3)結(jié)構(gòu)體：共享數(shù)據(jù)采用結(jié)構(gòu)體類型，同一個數(shù)據(jù)的不同成員之間可能由于沖突導(dǎo)致完整性被破壞。

4)聯(lián)合體：代碼中對聯(lián)合體不同成員的訪問應(yīng)當(dāng)作對同一數(shù)據(jù)單元的操作，但是很多檢測工具往往不能進行這種處理，因此是否支持聯(lián)合體是對工具評估的一項要素。

5)指針類型：指針變量本身發(fā)生沖突，可能導(dǎo)致被訪問的具體數(shù)據(jù)是不一致的。

在C語言程序中，對上述類型的共享數(shù)據(jù)進行訪問的方式通常有兩種，一是通過變量賦值和讀取，二是通過指針解引用間接訪問。其中，工具對前者的支持相對容易，對后者的支持需要引入稍復(fù)雜的指針分析技術(shù)，而是否精確又取決于所采用的指針分析算法的精度。在本文研究的案例中，通過指針解引用進行共享數(shù)據(jù)訪問占到15%，共享數(shù)據(jù)訪問方式也是對工具評估的要素之一。

1.2.4 要素4：控制流場景

無論動態(tài)或靜態(tài)檢測技術(shù)，控制流場景都可能影響分析的精度和效率。在航天嵌入式軟件中，控制流場景包括：

1)函數(shù)嵌套：對于靜態(tài)檢測，對函數(shù)嵌套的支持需要引入過程間分析技術(shù)，否則將無法正確識別出通過底層函數(shù)對共享數(shù)據(jù)的讀寫操作。

2)中斷嵌套：中斷嵌套可被看作一種特殊的函數(shù)嵌套，但與函數(shù)調(diào)用不同，內(nèi)層中斷的觸發(fā)不是顯式的，具有不確定性。對中斷嵌套的支持意味著分析的復(fù)雜度會指數(shù)級增長。

3)分支訪問：分支訪問會影響檢測工具的誤報率，當(dāng)沒有引入路徑敏感分析時，工具不能識別出兩個互斥分支是不可行路徑，將導(dǎo)致較高的誤報率。

1.2.5 要素5：并發(fā)關(guān)系

在不同并發(fā)體系結(jié)構(gòu)下，數(shù)據(jù)訪問沖突涉及的并發(fā)關(guān)系對工具的檢測能力是一項挑戰(zhàn)。并發(fā)關(guān)系包括：

1)任務(wù)與中斷：任務(wù)中的數(shù)據(jù)訪問被中斷搶占而發(fā)生沖突。其中任務(wù)泛指主循環(huán)任務(wù)或?qū)崟r操作系統(tǒng)中的任務(wù)；

2)中斷與中斷：指低優(yōu)先級中斷被高優(yōu)先級中斷搶占而發(fā)生沖突。

3)任務(wù)與任務(wù)：在實時操作系統(tǒng)下，多個任務(wù)之間未正確進行同步或互斥導(dǎo)致發(fā)生數(shù)據(jù)訪問沖突。

在不同并發(fā)關(guān)系下，數(shù)據(jù)訪問沖突發(fā)生的場景及缺陷特征表現(xiàn)不同，因此對檢測技術(shù)及工具的要求也不同。

1.2.6 要素6：缺陷模式

根據(jù)本文前期研究[6]，航天嵌入式軟件中存在共7種數(shù)據(jù)訪問沖突缺陷模式。其中模式1、模式2、模式3、模式5等4種缺陷模式可在軟件代碼上體現(xiàn)，且適合用工具進行自動化檢測。模式4屬于系統(tǒng)設(shè)計導(dǎo)致的缺陷，需從設(shè)計層面解決；模式6通過相關(guān)編碼規(guī)范來進行約束，并不屬于一般數(shù)據(jù)訪問沖突檢測工具研究的重點；模式7無法采用自動化的方法，一般通過代碼審查即可有效識別。本文所關(guān)注的4種模式(詳見文獻[6])如下：

1)模式1：單變量訪問序模式。

2)模式2：多個關(guān)聯(lián)變量訪問一致性被破壞。

3)模式3：多字節(jié)變量訪問原子性被破壞。

4)模式5：重復(fù)加鎖解鎖。

2 數(shù)據(jù)訪問沖突基準(zhǔn)測試集 RaceBench

2.1 設(shè)計準(zhǔn)則

基于第1節(jié)研究的要素集，本文按照以下原則設(shè)計開發(fā)了一個航天嵌入式軟件數(shù)據(jù)訪問沖突基準(zhǔn)測試集RaceBench：

1)代表性?；鶞?zhǔn)測試集要能夠接近真實程序，代表真實軟件和真實缺陷。由于嵌入式軟件的封閉性，RaceBench無法像其他基準(zhǔn)測試集一樣通過收集開源程序完成，而是基于一個廣泛應(yīng)用于航天型號的實時嵌入式操作系統(tǒng)SpaceOS2開發(fā)。該操作系統(tǒng)具有多任務(wù)管理和中斷管理特性，能夠支持航天嵌入式軟件常用的兩種并發(fā)體系結(jié)構(gòu)，在軟件特征方面與真實嵌入式軟件保持一致，保證RaceBench的真實性和代表性。

2)多樣性。要能夠覆蓋不同類型的程序及程序不同的特征，包括程序的體系結(jié)構(gòu)、程序的語法特征、缺陷模式類型；RaceBench通過選取或設(shè)計相應(yīng)的程序，覆蓋航天嵌入式軟件特征及數(shù)據(jù)訪問沖突缺陷特征的各個要素，保證基準(zhǔn)測試集具有多樣性。

3)適應(yīng)性?；鶞?zhǔn)測試集要能夠適應(yīng)不同的硬件平臺，具有平臺無關(guān)性；RaceBench將平臺無關(guān)的特征考慮到構(gòu)建中，而與平臺相關(guān)的一些特性對檢測方法研究并不具有普適性，本文并未考慮。

4)公平性?；鶞?zhǔn)測試集的設(shè)計不應(yīng)傾向于某個特定的工具或方法，保證具有公平的評價能力。RaceBench的設(shè)計和選取完全來源于案例及其要素，不依賴于特定的方法和工具。

一個完善的基準(zhǔn)測試集需要持續(xù)地開發(fā)豐富，RaceBench采用模塊化設(shè)計，便于對新要素覆蓋的擴展。未來我們計劃開源RaceBench，為其他研究中斷數(shù)據(jù)訪問沖突檢測方法的學(xué)者提供研究基礎(chǔ)。

2.2 RaceBench的設(shè)計與實現(xiàn)

RaceBench是一個運行在SpaceOS2上的應(yīng)用程序，采用實時多任務(wù)操作系統(tǒng)+中斷結(jié)構(gòu)，由主控調(diào)度程序及若干用例程序組成。其中，主控調(diào)度程序根據(jù)并發(fā)場景的設(shè)計調(diào)用各個用例程序，不同的用例程序覆蓋不同的數(shù)據(jù)訪問沖突要素集合。

目前RaceBench包含14個用例程序，所有用例程序都來源于代表性的航天嵌入式軟件案例，各個用例程序的覆蓋情況如表2所示。表格填充表示測試程序?qū)υ撘馗采w。例如：用例1覆蓋了缺陷模式1中R-W-R的訪問序情況，涉及了一個基本類型的共享變量，沖突發(fā)生在任務(wù)與中斷中，程序通過變量讀寫的方式訪問共享數(shù)據(jù)，控制流場景中涉及了分支訪問。

從表2可以看出，RaceBench的用例程序?qū)Ω鱾€要素都進行了完整的覆蓋，具有多樣性的特征。在并發(fā)設(shè)計上，主控程序包括5個任務(wù)及4個中斷，優(yōu)先級各不相同。任務(wù)為循環(huán)運行方式，每次循環(huán)完畢調(diào)用延時任務(wù)以實現(xiàn)任務(wù)的切換。4個中斷中3個為隨機觸發(fā)，1個為定時觸發(fā)。用例程序與各個任務(wù)和中斷的關(guān)系如表3所示。

主控程序負責(zé)發(fā)起5個任務(wù)，向操作系統(tǒng)掛載4個中斷，并在各個任務(wù)和中斷入口函數(shù)中按照設(shè)計調(diào)用用例程序。各個任務(wù)和中斷的屬性如表4所示。通過上述并發(fā)場景設(shè)計，RaceBench能夠模擬多級中斷嵌套和多種并發(fā)搶占，對檢測方法或工具的可伸縮性能夠較好地評估。

基于RaceBench可擴展性設(shè)計，未來還將不斷加入新的樣例程序。

表2 用例程序?qū)Ω鱾€要素的覆蓋

表3 用例程序與任務(wù)和中斷的關(guān)系

表4 RaceBench中各個任務(wù)的屬性

3 試驗評估

為了驗證RaceBench對數(shù)據(jù)訪問沖突檢測工具進行評估的能力，本文選取一個靜態(tài)中斷數(shù)據(jù)競爭檢測工具SpaceDRC進行了試驗。SpaceDRC是一個面向變量訪問序模式的中斷數(shù)據(jù)競爭檢測工具，是本文前期的研究工作。該工具能夠?qū)Σ糠謹(jǐn)?shù)據(jù)訪問沖突問題進行有效識別，但受所采用技術(shù)的限制，仍然存在誤報和漏報，還處在不斷地優(yōu)化中。

SpaceDRC運行于一臺型號為HP Compaq dc7900的計算機上，CPU為Intel Core2 Quad Q9650(3.00GHz，四核)，內(nèi)存為4GB，操作系統(tǒng)為Microsoft Windows 7。針對RaceBench的分析，SpaceDRC共報告23數(shù)據(jù)訪問沖突，涉及96種場景，分析耗時69 s。經(jīng)分析，工具報告結(jié)果中包含21處真實缺陷、2處誤報和3處漏報。

其中2處誤報原因為：SpaceDRC未考慮中斷的觸發(fā)時機，所涉及的并發(fā)場景在真實環(huán)境中無法復(fù)現(xiàn)。

對漏報情況的詳細分析如下：

1)case5中，在任務(wù)中對case5_x，case5_y和case5_z三個全局變量進行讀，在中斷中取地址傳引用給writeVariable()函數(shù)中，再通過指針解引用對3個變量進行寫操作，如圖3(a)所示。SpaceDRC未能識別出通過指針解引用進行共享數(shù)據(jù)訪問導(dǎo)致的沖突。

2)case12中預(yù)埋了兩種類型的沖突，包括指針解引用方式和聯(lián)合體成員別名方式，如圖3(b)所示。

對于前者，在低優(yōu)先級中斷中通過指向g1_case12的指針tmp解引用(*tmp=1)進行寫操作，在高優(yōu)先級中斷中直接對變量進行寫操作，兩者實際上存在沖突，但SpaceDRC未報告。

對于后者，在低優(yōu)先級中斷中對聯(lián)合體packet_case12的第1個成員header進行賦值，在高級中斷中對其第2個成員進行賦值，根據(jù)聯(lián)合體的語義定義，其第1個成員和第2個成員指向同一個內(nèi)存數(shù)據(jù)，因此上述操作是潛在的數(shù)據(jù)訪問沖突，但SpaceDRC未報告。

根據(jù)以上試驗結(jié)果可以得出對SpaceDRC的評估結(jié)論：

1)SpaceDRC的檢測能力覆蓋了各類缺陷模式、并發(fā)關(guān)系和控制流場景；

2)SpaceDRC能夠支持3級中斷和5個以內(nèi)任務(wù)的檢測；

3)SpaceDRC不支持指針解引用數(shù)據(jù)訪問方式和聯(lián)合體數(shù)據(jù)類型，根據(jù)第1.2.3節(jié)對共享數(shù)據(jù)訪問方式的統(tǒng)計分析，指針解引用和聯(lián)合體別名方式僅占到15%?；诮y(tǒng)計學(xué)規(guī)律可得出SpaceDRC對數(shù)據(jù)訪問沖突問題的檢出率為84%。

因此，RaceBench能夠有效評估數(shù)據(jù)訪問沖突檢測工具的檢出率、可伸縮性等各項指標(biāo)，并為SpaceDRC的進一步改進提供了方向。

4 結(jié)束語

本文對航天嵌入式軟件真實數(shù)據(jù)訪問沖突案例進行了系統(tǒng)分析，提出了影響數(shù)據(jù)訪問沖突檢測的6類要素，為中斷數(shù)據(jù)訪問沖突基準(zhǔn)測試集以及檢測方法的研究提供了基礎(chǔ)?；谶@些要素，設(shè)計開發(fā)了已知首個中斷數(shù)據(jù)訪問沖突問題基準(zhǔn)測試集RaceBench。RaceBench來源于真實案例，體現(xiàn)了中斷數(shù)據(jù)訪問沖突各個方面的要素，滿足了一個基準(zhǔn)測試集的代表性、多樣性、公平性和適應(yīng)性特征。試驗表明，RaceBench能夠有效評估相應(yīng)工具的技術(shù)指標(biāo)。本文構(gòu)建的基準(zhǔn)測試集對工具選型具有現(xiàn)實意義，也為中斷數(shù)據(jù)競爭研究提供指導(dǎo)。一個完善的缺陷基準(zhǔn)測試集構(gòu)建是一個長期的過程，未來RaceBench將繼續(xù)擴展新的缺陷特征和場景，提供更完備的評估能力。

References)

[1] LEVESON N G，TURNER C. An investigation of the Therac-25 accidents[J]. IEEE Computer，1993，16(7)：18-41.

[2] US-Canada Power System Outage Task Force. Final report on the August 14，2003 blackout in the United States and Canada：Causes and Recommendations[EB/OL]. 2004-04-01. http：∥energy.gov/sites/prod/files/oeprod/DocumentsandMedia/BlackoutFinal-Web.pdf.

[3] 楊孟飛，顧斌，郭向英，等. 航天嵌入式軟件可信性保障技術(shù)及應(yīng)用研究[J]. 中國科學(xué)：技術(shù)科學(xué)，2015，45(2)：198-203.

YANG M F，GU B，GUO X Y，et al. Aerospace embedded software dependability guarantee technology and application[J]. Scientia Scinica Technologica，2015，45(2)：198-203(in Chinese).

[4] 段永顥，陳睿. 基于啟發(fā)式的靜態(tài)中斷數(shù)據(jù)競爭檢測方法[J]. 計算機工程與設(shè)計，2013，34(1)：140-145.

DUAN Y H，CHEN R. Heuristic static data race detection for interrupt-driven software[J]. Computer Engineering and Design，2013，34(1)：140-145(in Chinese).

[5] CHEN R，GUO X Y，DUAN Y H，et al. Static data race detection for interrupt-driven embedded software[C]∥ Proceedings of International Conference on Secure Integration and Reliability Improvement 2011，Jesu Island，South Korea，June 27-29，2011.Washington,D.C.:IEEE Reliability Society，2011.

[6] 陳睿，楊孟飛，郭向英. 基于變量訪問序模式的中斷數(shù)據(jù)競爭檢測方法[J].軟件學(xué)報，2016，27(3)：547-561.

CHEN R，YANG M F，GUO X Y. Interrupt data race detection based on shared variable access order pattern[J]. Journal of Software，2016，27(3)：547-561(in Chinese).

[7] REGEHR J，COOPRIDER N. Interrupt verification via thread verification[J]. Electron. Notes Theoretical Computer Science，2007，174(9)：139-150.

[8] 周筱羽，顧斌，趙建華，等.中斷驅(qū)動系統(tǒng)模型檢驗[J]. 軟件學(xué)報，2015，26(9)：2221-2230.

ZHOU X Y，GU B，ZHAO J H，et al. Model checking technique for interrupt-driven system[J]. Journal of Software，2015，26(9)：2221-2230(in Chinese).

[9] WU X G，WEN Y J，CHEN L Q，et al. Data race detection for interrupt-driven programs via bounded model checking[C]∥ Proc.Of IEEE 7th International Conference on Software Security and Reliability-Companion(SERE-C)，Washington，D.C.，USA，18-20 June,2013.

[10] 霍瑋，于洪濤，馮曉兵，等. 靜態(tài)檢測中斷驅(qū)動程序的數(shù)據(jù)競爭[J].計算機研究與發(fā)展，2011，48(12)：2290-2299.

HUO W，YU H T，F(xiàn)ENG X B，et al. Static data race detection of interrupt-driven programs[J].Journal of Computer Research and Development，2011，48(12)：2290-2299(in Chinese).

[11] 陳園軍，石浚菁，王林章，等.中斷驅(qū)動的嵌入式系統(tǒng)數(shù)據(jù)競爭檢測工具[J].計算機科學(xué)與探索，2015，9(8)：914-925.

CHEN Y J，SHI J J，WANG L Z，et al. Data race detection tool for interrupt-driven embedded system[J]. Journal of Frontiers of Computer Science and Technology，2015，9(8)：914-925(in Chinese).

[12] WU X G，CHEN L Q，MINE A，et al. Static analysis of run-time errors in interrupt-driven programs via sequentialization[J]. ACM Transactions on Embedded Computing Systems(TECS)，2016，15(4)：1-26.

[13] 于廣良，楊孟飛，徐建，等. 面向多級中斷系統(tǒng)的任務(wù)最差響應(yīng)時間分析[J]. 中國空間科學(xué)技術(shù)，2016，36(2)：28-36.

YU G L，YANG M F，XU J，et al. Worst case response time analysis of multi-level interrupt systems[J]. Chinese Space Science and Technology，2016，36(2)：28-35(in Chinese).

[14] Standard Performance Evaluation Corporation. SPEC benchmarks[EB/OL].2017-03-28.URL：http：∥www.spec.org.

[15] Transaction Processing Council. TPC benchmarks[EB/OL].2016-10-26. URL：http：∥www.tpc.org/.

[16] CIFUENTES C，HOERMANN C，KEYNES N，et al. BegBunch：benchmarking for C bug detection tools[C]. The 2nd International Workshop on Defects in Large Software Systems，Chicago，USA，July 19，2009.

[17] LU S，LI Z，QIN F，TAN L，et al. BugBench：a benchmark for evaluating bug detection tools[C]∥Proc. of Workshop on the Evaluation of Software Defect Detection Tools，June，2005.

[18] NIST. National Institute of Standards and Technology SAMATE Reference Dataset (SRD) project[EB/OL].2016-01-01. http：∥samate.nist.gov/SRD，January，2006.

(編輯：車曉玲)

Study on aerospace embedded software data race benchmark

CHEN Rui1，2，YANG Mengfei3，*

1.BeijingInstituteofControlEngineering，Beijing100190，China2.BeijingSunwiseInformationTechnologyCo.Ltd.，Beijing100190，China3.ChinaAcademyofSpaceTechnology，Beijing100094，China

No good benchmark suite was made to evaluate the detection methods or tools for the advent of interrupt data race. Based on the real aerospace embedded software data race bugs，six essential factors related to data race detection were proposed，and the data race benchmark suite named RaceBench for aerospace embedded software was designed. The RaceBench，which is close to real programs and is extensible，covers all six factors. The RaceBench was used to evaluate a data race detection tool named SpaceDRC. The result shows that RaceBench can evaluate the capabilities of the tool effectively.

data access conflict；benchmark；aerospace embedded software；data race；software testing

10.16708/j.cnki.1000-758X.2017.0052

2017-04-10；

2017-04-20；錄用日期：2017-05-18；網(wǎng)絡(luò)出版時間：2017-05-31 09:44:37

http:∥kns.cnki.net/kcms/detail/11.1859.V.20170531.0944.004.html

國家自然科學(xué)基金(91118007，61632005)

陳睿(1984-)，男，博士研究生，高級工程師，chenrui@sunwiseinfo.com，研究方向為嵌入式軟件測試

*通訊作者：楊孟飛(1962-)，男，研究員，yangmf@bice.org.cn，研究方向為空間飛行器系統(tǒng)設(shè)計、控制計算機系統(tǒng)及嵌入式軟件

陳睿，楊孟飛. 航天嵌入式軟件數(shù)據(jù)訪問沖突基準(zhǔn)測試集研究[J].中國空間科學(xué)技術(shù)，2017，37(3)：62-70.

CHENR,YANGMF.Studyonaerospaceembeddedsoftwaredataracebenchmark[J].ChineseSpaceScienceandTechnology，2017，37(3)：62-70(inChinese).

TP311

A

http:∥zgkj.cast.cn