999精品在线视频,手机成人午夜在线视频,久久不卡国产精品无码,中日无码在线观看,成人av手机在线观看,日韩精品亚洲一区中文字幕,亚洲av无码人妻,四虎国产在线观看 ?

航天嵌入式軟件數據訪問沖突基準測試集研究

2017-07-03 16:03:51陳睿楊孟飛
中國空間科學技術 2017年3期
關鍵詞:程序

陳睿,楊孟飛

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

?

航天嵌入式軟件數據訪問沖突基準測試集研究

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

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

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

數據訪問沖突;基準測試集;航天嵌入式軟件;數據競爭;軟件測試

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

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

不同的數據訪問沖突檢測方法或工具在實際代碼中應用時,檢出率、誤報率、性能等技術指標存在較大差異。一方面,在工程實踐中選取合適的工具時需要一個統一的評價標準進行指導;另一方面,工具的研究設計者也希望了解自己的成果在工程實踐中的適用性及與其他競爭成果的優劣比較,為進一步改進研究提供指導。

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

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

1 中斷數據訪問沖突問題要素

本文對大量真實航天嵌入式軟件數據訪問沖突案例進行系統分析,綜合檢測技術、軟件特征、缺陷特征等多種因素,提煉出數據訪問沖突問題的關鍵要素,作為構建基準測試集的基礎。

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

1.1 案例分析方法概述

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

然后,進行缺陷特征信息采集,包括:1)確定與缺陷特征與統計分析相關的因素,包括軟件名、運行環境、并發體系結構、規模、問題,描述、代碼片段、共享數據類型、問題處理方式;2)設計相應的表格收集缺陷信息。缺陷特征信息的收集是一個迭代的過程,在此過程中,需要查看問題管理系統中的問題描述、定位代碼,比對獲取后續版本的修改策略。

最后,經過統計分析,得出特征結果。

1.2 數據訪問沖突問題要素

經案例分析得出,數據訪問沖突問題有軟件特征和缺陷特征兩方面的要素,如圖1所示。其中,軟件特征包括并發體系結構、開發語言及運行環境等;缺陷特征包括并發關系、數據訪問方式、共享數據的類型、控制流場景和缺陷模式。

1.2.1 要素1:軟件并發體系結構

數據訪問沖突是一種典型的并發缺陷,軟件的并發體系結構與缺陷檢測之間存在直接的關系。航天嵌入式軟件是典型的強實時系統,且存在多種并發方式。主要采用兩種并發體系結構:

(1)主循環+中斷結構(Round-Robin with Interrupts)

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

(2)實時多任務操作系統+中斷結構

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

(3)并發體系結構分布分析

根據案例分析數據統計,并發體系結構為RR-ISR的缺陷占82%,RTOS-ISR占18%。這種差異主要是由于航天嵌入式軟件本身采用的并發體系結構分布導致的。需要注意的是,RTOS-ISR結構的程序呈上升趨勢,為研究帶來新的問題。本文在構建基準測試集時考慮到了這種統計差異。

1.2.2 要素2:軟件形態及運行環境

軟件形態包括編程語言和軟件規模兩個方面。

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

軟件規模從數百行到上萬行不等,并發流個數與體系結構相關,中斷服務程序少于5個。

航天嵌入式軟件的硬件運行環境多樣,以SPARC、x86、MCS-51、DSP等體系結構的處理器為主。中斷并發機制與處理器架構相關,多為固定優先級非對稱搶占,各種處理器都有類似的中斷屏蔽機制實現中斷并發的互斥。

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

表1 數據訪問沖突缺陷處理器分布

1.2.3 要素3:共享數據類型及訪問方式

共享數據的類型是影響中斷數據訪問沖突檢測的關鍵因素。不同數據類型的共享數據在沖突方式上表現不同,例如結構體變量的沖突多發生在不同成員訪問的不一致性,數組變量的沖突發生在不同元素訪問中,因此對檢測工具的能力要求也不同。目前航天嵌入式軟件并發問題中表現出的沖突變量類型包括:

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

2)數組:共享數據的類型為數組。當按照一定順序依次訪問數組多個元素時,可能發生多個元素訪問不一致的情況。

3)結構體:共享數據采用結構體類型,同一個數據的不同成員之間可能由于沖突導致完整性被破壞。

4)聯合體:代碼中對聯合體不同成員的訪問應當作對同一數據單元的操作,但是很多檢測工具往往不能進行這種處理,因此是否支持聯合體是對工具評估的一項要素。

5)指針類型:指針變量本身發生沖突,可能導致被訪問的具體數據是不一致的。

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

1.2.4 要素4:控制流場景

無論動態或靜態檢測技術,控制流場景都可能影響分析的精度和效率。在航天嵌入式軟件中,控制流場景包括:

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

2)中斷嵌套:中斷嵌套可被看作一種特殊的函數嵌套,但與函數調用不同,內層中斷的觸發不是顯式的,具有不確定性。對中斷嵌套的支持意味著分析的復雜度會指數級增長。

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

1.2.5 要素5:并發關系

在不同并發體系結構下,數據訪問沖突涉及的并發關系對工具的檢測能力是一項挑戰。并發關系包括:

1)任務與中斷:任務中的數據訪問被中斷搶占而發生沖突。其中任務泛指主循環任務或實時操作系統中的任務;

2)中斷與中斷:指低優先級中斷被高優先級中斷搶占而發生沖突。

3)任務與任務:在實時操作系統下,多個任務之間未正確進行同步或互斥導致發生數據訪問沖突。

在不同并發關系下,數據訪問沖突發生的場景及缺陷特征表現不同,因此對檢測技術及工具的要求也不同。

1.2.6 要素6:缺陷模式

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

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

2)模式2:多個關聯變量訪問一致性被破壞。

3)模式3:多字節變量訪問原子性被破壞。

4)模式5:重復加鎖解鎖。

2 數據訪問沖突基準測試集 RaceBench

2.1 設計準則

基于第1節研究的要素集,本文按照以下原則設計開發了一個航天嵌入式軟件數據訪問沖突基準測試集RaceBench:

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

2)多樣性。要能夠覆蓋不同類型的程序及程序不同的特征,包括程序的體系結構、程序的語法特征、缺陷模式類型;RaceBench通過選取或設計相應的程序,覆蓋航天嵌入式軟件特征及數據訪問沖突缺陷特征的各個要素,保證基準測試集具有多樣性。

3)適應性。基準測試集要能夠適應不同的硬件平臺,具有平臺無關性;RaceBench將平臺無關的特征考慮到構建中,而與平臺相關的一些特性對檢測方法研究并不具有普適性,本文并未考慮。

4)公平性。基準測試集的設計不應傾向于某個特定的工具或方法,保證具有公平的評價能力。RaceBench的設計和選取完全來源于案例及其要素,不依賴于特定的方法和工具。

一個完善的基準測試集需要持續地開發豐富,RaceBench采用模塊化設計,便于對新要素覆蓋的擴展。未來我們計劃開源RaceBench,為其他研究中斷數據訪問沖突檢測方法的學者提供研究基礎。

2.2 RaceBench的設計與實現

RaceBench是一個運行在SpaceOS2上的應用程序,采用實時多任務操作系統+中斷結構,由主控調度程序及若干用例程序組成。其中,主控調度程序根據并發場景的設計調用各個用例程序,不同的用例程序覆蓋不同的數據訪問沖突要素集合。

目前RaceBench包含14個用例程序,所有用例程序都來源于代表性的航天嵌入式軟件案例,各個用例程序的覆蓋情況如表2所示。表格填充表示測試程序對該要素覆蓋。例如:用例1覆蓋了缺陷模式1中R-W-R的訪問序情況,涉及了一個基本類型的共享變量,沖突發生在任務與中斷中,程序通過變量讀寫的方式訪問共享數據,控制流場景中涉及了分支訪問。

從表2可以看出,RaceBench的用例程序對各個要素都進行了完整的覆蓋,具有多樣性的特征。在并發設計上,主控程序包括5個任務及4個中斷,優先級各不相同。任務為循環運行方式,每次循環完畢調用延時任務以實現任務的切換。4個中斷中3個為隨機觸發,1個為定時觸發。用例程序與各個任務和中斷的關系如表3所示。

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

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

表2 用例程序對各個要素的覆蓋

表3 用例程序與任務和中斷的關系

表4 RaceBench中各個任務的屬性

3 試驗評估

為了驗證RaceBench對數據訪問沖突檢測工具進行評估的能力,本文選取一個靜態中斷數據競爭檢測工具SpaceDRC進行了試驗。SpaceDRC是一個面向變量訪問序模式的中斷數據競爭檢測工具,是本文前期的研究工作。該工具能夠對部分數據訪問沖突問題進行有效識別,但受所采用技術的限制,仍然存在誤報和漏報,還處在不斷地優化中。

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

其中2處誤報原因為:SpaceDRC未考慮中斷的觸發時機,所涉及的并發場景在真實環境中無法復現。

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

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

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

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

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

根據以上試驗結果可以得出對SpaceDRC的評估結論:

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

2)SpaceDRC能夠支持3級中斷和5個以內任務的檢測;

3)SpaceDRC不支持指針解引用數據訪問方式和聯合體數據類型,根據第1.2.3節對共享數據訪問方式的統計分析,指針解引用和聯合體別名方式僅占到15%。基于統計學規律可得出SpaceDRC對數據訪問沖突問題的檢出率為84%。

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

4 結束語

本文對航天嵌入式軟件真實數據訪問沖突案例進行了系統分析,提出了影響數據訪問沖突檢測的6類要素,為中斷數據訪問沖突基準測試集以及檢測方法的研究提供了基礎。基于這些要素,設計開發了已知首個中斷數據訪問沖突問題基準測試集RaceBench。RaceBench來源于真實案例,體現了中斷數據訪問沖突各個方面的要素,滿足了一個基準測試集的代表性、多樣性、公平性和適應性特征。試驗表明,RaceBench能夠有效評估相應工具的技術指標。本文構建的基準測試集對工具選型具有現實意義,也為中斷數據競爭研究提供指導。一個完善的缺陷基準測試集構建是一個長期的過程,未來RaceBench將繼續擴展新的缺陷特征和場景,提供更完備的評估能力。

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] 楊孟飛,顧斌,郭向英,等. 航天嵌入式軟件可信性保障技術及應用研究[J]. 中國科學:技術科學,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] 段永顥,陳睿. 基于啟發式的靜態中斷數據競爭檢測方法[J]. 計算機工程與設計,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] 陳睿,楊孟飛,郭向英. 基于變量訪問序模式的中斷數據競爭檢測方法[J].軟件學報,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] 周筱羽,顧斌,趙建華,等.中斷驅動系統模型檢驗[J]. 軟件學報,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] 霍瑋,于洪濤,馮曉兵,等. 靜態檢測中斷驅動程序的數據競爭[J].計算機研究與發展,2011,48(12):2290-2299.

HUO W,YU H T,FENG 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] 陳園軍,石浚菁,王林章,等.中斷驅動的嵌入式系統數據競爭檢測工具[J].計算機科學與探索,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] 于廣良,楊孟飛,徐建,等. 面向多級中斷系統的任務最差響應時間分析[J]. 中國空間科學技術,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;網絡出版時間:2017-05-31 09:44:37

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

國家自然科學基金(91118007,61632005)

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

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

陳睿,楊孟飛. 航天嵌入式軟件數據訪問沖突基準測試集研究[J].中國空間科學技術,2017,37(3):62-70.

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

TP311

A

http:∥zgkj.cast.cn

猜你喜歡
程序
給Windows添加程序快速切換欄
電腦愛好者(2020年6期)2020-05-26 09:27:33
試論我國未決羈押程序的立法完善
人大建設(2019年12期)2019-05-21 02:55:44
失能的信仰——走向衰亡的民事訴訟程序
“程序猿”的生活什么樣
英國與歐盟正式啟動“離婚”程序程序
環球時報(2017-03-30)2017-03-30 06:44:45
基于VMM的程序行為異常檢測
偵查實驗批準程序初探
我國刑事速裁程序的構建
創衛暗訪程序有待改進
中國衛生(2015年3期)2015-11-19 02:53:32
恐怖犯罪刑事訴訟程序的完善
主站蜘蛛池模板: 亚洲欧美精品一中文字幕| 毛片基地美国正在播放亚洲 | 日本成人精品视频| 国产精品白浆在线播放| 亚洲国产AV无码综合原创| 国产成人亚洲欧美激情| 露脸一二三区国语对白| 欧美日韩中文国产va另类| 国产欧美日韩在线一区| 日本亚洲欧美在线| 国产精品美女在线| 日韩欧美国产另类| 91精品国产91久久久久久三级| 中日韩一区二区三区中文免费视频| 国产精鲁鲁网在线视频| 青青青国产视频| 中文字幕日韩丝袜一区| 国产九九精品视频| 国产精品99久久久| 日韩国产另类| 亚洲三级电影在线播放| 国产精女同一区二区三区久| 日韩美毛片| 国产va在线| 久久毛片网| 欧美亚洲另类在线观看| 伊人久久福利中文字幕| 最新国产精品第1页| 色悠久久综合| 大学生久久香蕉国产线观看| 国产成人1024精品下载| 国产精品久久久久鬼色| 一区二区三区四区日韩| 91免费国产在线观看尤物| 精品国产自在在线在线观看| 国产精品综合色区在线观看| 青青草原国产精品啪啪视频| 无码精品国产VA在线观看DVD| 九九精品在线观看| 日本高清有码人妻| 久久男人资源站| 欧美一区日韩一区中文字幕页| 亚洲欧美成aⅴ人在线观看 | 亚洲无码日韩一区| a亚洲天堂| 亚洲精品免费网站| 国产人成在线视频| 天天色天天综合| 日韩午夜福利在线观看| 91九色国产porny| 在线五月婷婷| 最新无码专区超级碰碰碰| 美女被躁出白浆视频播放| 欧美特黄一级大黄录像| 精品五夜婷香蕉国产线看观看| 欧美日韩国产系列在线观看| 久久无码av三级| 在线日韩日本国产亚洲| 日本不卡在线播放| 国产99欧美精品久久精品久久| 日本久久网站| 日韩av无码精品专区| 欧美日韩午夜| 国产精品jizz在线观看软件| 波多野结衣一区二区三区四区| 久久人搡人人玩人妻精品| 中国一级特黄大片在线观看| 国产免费a级片| a欧美在线| a色毛片免费视频| 免费A级毛片无码无遮挡| 亚洲中文字幕在线观看| 中文字幕在线一区二区在线| 91香蕉国产亚洲一二三区| 国产成人精品免费视频大全五级| 国产91av在线| 在线观看亚洲成人| 国产Av无码精品色午夜| 日韩欧美国产综合| 中文字幕不卡免费高清视频| 欧美视频免费一区二区三区| 最新国产精品第1页|