陳立前， 吳國(guó)福， 姜加紅

1. 國(guó)防科技大學(xué)計(jì)算機(jī)學(xué)院， 湖南 長(zhǎng)沙 410073 2. 國(guó)防科技大學(xué)空天科學(xué)學(xué)院， 湖南 長(zhǎng)沙 410073 3. 北京跟蹤與通信技術(shù)研究所， 北京 海淀 100095

0 引 言

隨著我國(guó)衛(wèi)星、大運(yùn)載火箭、載人航天、探月計(jì)劃的發(fā)展，航天嵌入式軟件的規(guī)模和復(fù)雜程度日益增大，系統(tǒng)并發(fā)性不斷增強(qiáng)，軟件系統(tǒng)變得日趨龐大和難以駕馭，軟件系統(tǒng)中潛在的缺陷也越來(lái)越難以檢測(cè)、定位和控制[1].軟件故障已成為航天系統(tǒng)失敗的重要因素[2].源代碼級(jí)程序錯(cuò)誤仍是航天嵌入式軟件中最突出的問(wèn)題之一，數(shù)組越界、算術(shù)溢出、被零除、空指針解引用、數(shù)據(jù)競(jìng)爭(zhēng)等問(wèn)題仍經(jīng)常發(fā)生.

靜態(tài)分析是一種在編譯時(shí)通過(guò)分析程序源代碼來(lái)推斷程序運(yùn)行時(shí)性質(zhì)的程序分析技術(shù)，是檢測(cè)代碼缺陷、提高代碼安全性與可靠性的一種重要技術(shù).盡管程序分析是一類不可判定問(wèn)題，然而通過(guò)適當(dāng)?shù)某橄螅o態(tài)分析能夠構(gòu)造程序行為的某種近似，并得出有意義的分析結(jié)果.程序靜態(tài)分析的目標(biāo)是在程序運(yùn)行前盡可能多地發(fā)現(xiàn)其中隱含的錯(cuò)誤，以提高程序的可靠性和安全性.對(duì)于一些常見的源代碼級(jí)程序錯(cuò)誤，雖已有較成熟商業(yè)化靜態(tài)分析工具(如Coverity、Klocwork、Parasoft等)支持其檢測(cè)，但是這些工具主要基于語(yǔ)法規(guī)則、缺陷模式等開展分析，程序語(yǔ)義信息利用不夠，且對(duì)于航天嵌入式軟件中常見的中斷并發(fā)機(jī)制、浮點(diǎn)運(yùn)算、面向可靠性的容錯(cuò)設(shè)計(jì)等代碼特征和要素考慮不夠，因此這些工具還不能很好地適用于航天嵌入式軟件的分析.

為此，本文首先將分析航天嵌入式軟件代碼特征及常見錯(cuò)誤.在此基礎(chǔ)上，介紹適合于航天嵌入式軟件錯(cuò)誤檢測(cè)的靜態(tài)分析技術(shù)，包括抽象解釋、符號(hào)執(zhí)行、數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)等.這些靜態(tài)分析技術(shù)都通過(guò)不同方式自動(dòng)分析并利用了程序的語(yǔ)義信息.

1 航天嵌入式軟件代碼特征及常見錯(cuò)誤

航天嵌入式軟件對(duì)可靠性要求非常高，軟件開發(fā)過(guò)程有嚴(yán)格的評(píng)審環(huán)節(jié)，軟件設(shè)計(jì)考慮容錯(cuò)與冗余設(shè)計(jì)，軟件編碼實(shí)現(xiàn)遵循嚴(yán)格的安全編程規(guī)范.遵循嚴(yán)格的編程規(guī)范，使用程序語(yǔ)言的安全子集編程，從某些方面規(guī)避了程序錯(cuò)誤的引入，也簡(jiǎn)化了程序分析的難度，如無(wú)需考慮遞歸函數(shù)、非結(jié)構(gòu)化程序結(jié)構(gòu)(goto語(yǔ)句)等.但是，航天嵌入式軟件中也有一些特征和要素，也給程序分析帶來(lái)了挑戰(zhàn).

航天嵌入式軟件在本質(zhì)上都是基于物理模型的，需要實(shí)現(xiàn)導(dǎo)航、姿軌控等模塊，因此不可避免地會(huì)包含大量數(shù)值計(jì)算，涉及許多整型、浮點(diǎn)型變量及其上的運(yùn)算，從而容易導(dǎo)致除以零、整數(shù)溢出、浮點(diǎn)溢出等運(yùn)行時(shí)錯(cuò)誤[1].在涉及姿態(tài)軌道控制的功能實(shí)現(xiàn)方面，航天軟件會(huì)大量使用浮點(diǎn)運(yùn)算.這些計(jì)算模塊的源數(shù)據(jù)來(lái)自敏感器模數(shù)(AD)轉(zhuǎn)換后的數(shù)據(jù)，如果不對(duì)數(shù)據(jù)的有效性進(jìn)行檢查，數(shù)據(jù)處理過(guò)程中可能出現(xiàn)非法浮點(diǎn)數(shù)等問(wèn)題，導(dǎo)致整個(gè)系統(tǒng)數(shù)據(jù)錯(cuò)誤.同時(shí)，由于浮點(diǎn)數(shù)的有限二進(jìn)質(zhì)制表示，在處理極小數(shù)時(shí)，可能產(chǎn)生除以零的問(wèn)題，導(dǎo)致無(wú)法得到正確結(jié)果.浮點(diǎn)的誤差累積可能對(duì)結(jié)果的計(jì)算精度造成較大影響.

為了更好封裝數(shù)據(jù)，航天嵌入式軟件會(huì)大量使用數(shù)組、結(jié)構(gòu)體、聯(lián)合體等數(shù)據(jù)結(jié)構(gòu)，從而容易出現(xiàn)初始化不完全、數(shù)組越界等數(shù)據(jù)使用問(wèn)題.航天嵌入式軟件大部分使用C語(yǔ)言編程，程序代碼中會(huì)大量使用指針，經(jīng)常會(huì)使用指針訪問(wèn)內(nèi)存絕對(duì)地址、數(shù)組、結(jié)構(gòu)體或傳遞函數(shù)參數(shù)等.指針的使用增加了編程實(shí)現(xiàn)的靈活性，但C語(yǔ)言中指針不受約束，指針訪問(wèn)可能超出所定義內(nèi)存區(qū)域范圍，造成越界訪問(wèn)，導(dǎo)致不相干數(shù)據(jù)被破壞、函數(shù)調(diào)用堆棧被覆蓋等嚴(yán)重問(wèn)題.

航天嵌入式軟件功能復(fù)雜，往往采用多任務(wù)(多進(jìn)程)設(shè)計(jì)，并且其執(zhí)行會(huì)受外部中斷源的影響.多任務(wù)調(diào)度、中斷處理帶來(lái)的并發(fā)可能導(dǎo)致數(shù)據(jù)競(jìng)爭(zhēng)、數(shù)據(jù)訪問(wèn)原子性違反等問(wèn)題.數(shù)據(jù)競(jìng)爭(zhēng)問(wèn)題僅在特定外部環(huán)境和輸入下才會(huì)出現(xiàn)，難以測(cè)試、調(diào)試和復(fù)現(xiàn)，問(wèn)題遺漏率較高，是航天嵌入式軟件可信性保障中最迫切需要解決的問(wèn)題之一.

航天嵌入式軟件中可能包含符合設(shè)計(jì)的無(wú)限循環(huán)(如用于事件處理、采集數(shù)據(jù)等).但是，不符合預(yù)期設(shè)計(jì)的無(wú)限循環(huán)可能給系統(tǒng)帶來(lái)嚴(yán)重的后果.代碼設(shè)計(jì)邏輯不當(dāng)會(huì)導(dǎo)致在某些條件下對(duì)循環(huán)變量進(jìn)行更改，導(dǎo)致無(wú)法滿足循環(huán)退出條件.程序進(jìn)入無(wú)限循環(huán)后，可能導(dǎo)致系統(tǒng)崩潰或者長(zhǎng)時(shí)間占用CPU無(wú)法為其他模塊服務(wù).

航天嵌入式軟件中往往融入三模冗余等容錯(cuò)技術(shù)來(lái)提高系統(tǒng)的可靠性.比如，為了防止外空間高能粒子對(duì)RAM數(shù)據(jù)造成的翻轉(zhuǎn)破壞，對(duì)關(guān)鍵數(shù)據(jù)采用三取二的方式，即數(shù)據(jù)保存三份副本，使用時(shí)采用三取二的表決方式得到正確的值.數(shù)據(jù)保存三份副本，新數(shù)據(jù)產(chǎn)生時(shí)需要同步更新三份數(shù)據(jù)，可能由于人為疏忽造成數(shù)據(jù)更新不同步，帶來(lái)關(guān)鍵數(shù)據(jù)錯(cuò)誤等問(wèn)題.因此，需要從代碼層面檢查同時(shí)更新了三份數(shù)據(jù)以及表決程序本身代碼實(shí)現(xiàn)的正確性.此外，看門狗程序、數(shù)據(jù)緩沖模塊(乒乓存儲(chǔ)、環(huán)形緩存等)、數(shù)字濾波器等航天嵌入式軟件中常見模塊的正確性，也需要保證.

2 面向航天嵌入式軟件的抽象解釋技術(shù)

抽象解釋是一種對(duì)程序語(yǔ)義進(jìn)行可靠近似的通用理論，可用于構(gòu)造和逼近程序不動(dòng)點(diǎn)，為靜態(tài)分析提供了一個(gè)通用的框架[3].基于抽象解釋的靜態(tài)程序分析框架一般包括編譯前端、不動(dòng)點(diǎn)求解器和抽象域庫(kù)三個(gè)模塊.編譯前端主要負(fù)責(zé)將源程序建模成遷移系統(tǒng)，不動(dòng)點(diǎn)求解器通過(guò)迭代的方式調(diào)用抽象域的操作來(lái)計(jì)算程序不變式，而抽象域庫(kù)一方面為靜態(tài)分析過(guò)程中需處理的值、表達(dá)式、約束等元素提供統(tǒng)一的數(shù)據(jù)類型，另一方面為區(qū)間抽象域、八邊形抽象域、多面體抽象域等抽象域的域操作提供了通用的接口.

上世紀(jì)九十年代末，基于抽象解釋的靜態(tài)分析工具已被用來(lái)識(shí)別導(dǎo)致阿麗亞娜5號(hào)火箭失效的程序錯(cuò)誤和類似錯(cuò)誤[4].近年來(lái)，基于抽象解釋的靜態(tài)分析工具在工業(yè)界大規(guī)模嵌入式軟件尤其是航空航天嵌入式軟件的分析與驗(yàn)證中得到了成功應(yīng)用[5-6].

PolySpace是最早采用抽象解釋的商業(yè)化靜態(tài)分析工具之一.目前，其產(chǎn)品Polyspace Code Prover，支持形式化地證明軟件中不存在嚴(yán)重的運(yùn)行時(shí)錯(cuò)誤(如不存在溢出、除以零、數(shù)組訪問(wèn)越界等運(yùn)行時(shí)錯(cuò)誤)；其產(chǎn)品Polyspace Bug Finder，能夠檢查編碼規(guī)則、安全標(biāo)準(zhǔn)、代碼質(zhì)量指標(biāo)，并能發(fā)現(xiàn)嵌入式軟件代碼中的運(yùn)行時(shí)錯(cuò)誤、并發(fā)問(wèn)題、安全漏洞等缺陷[7].最近，Alenia Aermacchi公司開發(fā)了符合DO-178B A級(jí)認(rèn)證的 M-346教練機(jī)飛行控制系統(tǒng)自動(dòng)駕駛儀軟件.在該自動(dòng)駕駛儀軟件的開發(fā)和認(rèn)證過(guò)程中，該公司使用了Polyspace靜態(tài)分析工具來(lái)檢查代碼中是否存在運(yùn)行時(shí)錯(cuò)誤，確保符合 MISRA C編碼標(biāo)準(zhǔn)，并為DO-178B A 級(jí)認(rèn)證的取證提供了證據(jù)[8].

Cousot等[5]基于抽象解釋開發(fā)了程序靜態(tài)分析工具ASTREE，并以航空航天嵌入式安全關(guān)鍵軟件系統(tǒng)作為主要研究對(duì)象，分析和驗(yàn)證這些軟件系統(tǒng)的一些關(guān)鍵性質(zhì)，并自動(dòng)檢測(cè)其中的運(yùn)行時(shí)錯(cuò)誤[6].這些錯(cuò)誤包括數(shù)組越界、算術(shù)溢出、除以零等.ASTREE被成功應(yīng)用于空客A340(約13.2萬(wàn)行C 代碼)、A380(約35 萬(wàn)行C代碼)等系列飛機(jī)的飛行控制軟件的分析，并實(shí)現(xiàn)了“零誤報(bào)”[9].在航天領(lǐng)域，ASTREE證明了歐空局“儒勒·凡爾納”號(hào)自動(dòng)貨運(yùn)飛船ATV (Automated Transfer Vehicle) 的自動(dòng)對(duì)接軟件(約19萬(wàn)行C代碼)不含運(yùn)行時(shí)錯(cuò)誤[10].最近，作為ASTREE的并發(fā)擴(kuò)展版本，Miné等[11]基于抽象解釋開發(fā)了面向并發(fā)程序分析的商業(yè)化靜態(tài)分析工具AstreeA，并實(shí)際應(yīng)用于空客飛行系統(tǒng)軟件的分析，被分析程序的最大規(guī)模達(dá)到百萬(wàn)行C代碼.

NASA開發(fā)了基于抽象解釋的C程序運(yùn)行時(shí)錯(cuò)誤檢查工具C Global Surveyor(CGS)[12]，并成功地應(yīng)用于Mars Path-Finder(13.5萬(wàn)行代碼)、Deep Space One(28萬(wàn)行代碼)、Mars Exploration Rover(65萬(wàn)行代碼)等NASA的火星探測(cè)項(xiàng)目的軟件質(zhì)量保證.CGS重點(diǎn)檢查C程序的三種運(yùn)行時(shí)錯(cuò)誤：訪問(wèn)未初始化變量、訪問(wèn)空指針、數(shù)組越界訪問(wèn).經(jīng)過(guò)針對(duì)NASA軟件的優(yōu)化，其誤報(bào)率被控制在10%左右.同時(shí)CGS利用多處理器平臺(tái)支持對(duì)程序的并行分析，從而進(jìn)一步提高了其可擴(kuò)展性.

另外，Goubault等[13]基于抽象解釋開發(fā)了用來(lái)分析浮點(diǎn)程序中舍入誤差的傳播情況并發(fā)現(xiàn)舍入誤差的階及其源頭的靜態(tài)分析工具Fluctuat，并在ATV自動(dòng)貨運(yùn)飛船的監(jiān)控與安全保障單元(MSU)軟件等工業(yè)界航空航天控制軟件的分析與驗(yàn)證中也得到了成功應(yīng)用[10].

3 面向航天嵌入式軟件的符號(hào)執(zhí)行技術(shù)

符號(hào)執(zhí)行技術(shù)使用符號(hào)化的值(而非具體值)作為輸入，來(lái)(抽象)執(zhí)行程序.這樣，每次(抽象)執(zhí)行就可以覆蓋具有相同執(zhí)行路徑的多個(gè)輸入，分析器可以搜集每次執(zhí)行對(duì)應(yīng)的路徑約束，然后通過(guò)約束求解器求解得到可觸發(fā)該路徑的具體輸入值.總體而言，相比抽象解釋符號(hào)執(zhí)行可以避免誤報(bào).符號(hào)執(zhí)行發(fā)現(xiàn)的錯(cuò)誤對(duì)應(yīng)一條真實(shí)可行的路徑，從而可以生成觸發(fā)該錯(cuò)誤的測(cè)試用例.符號(hào)執(zhí)行技術(shù)最初在上世紀(jì)70年代提出，但是當(dāng)時(shí)的硬件和算法能力尚不夠，所以應(yīng)用受限.近年來(lái)，隨著SAT和SMT求解技術(shù)的快速發(fā)展、相關(guān)判定算法的研究進(jìn)展以及現(xiàn)代計(jì)算機(jī)運(yùn)算速度的提升，符號(hào)執(zhí)行在越來(lái)越多的實(shí)際場(chǎng)景中變得適用可行，成為近十余年的研究熱點(diǎn)之一.基于符號(hào)執(zhí)行技術(shù)構(gòu)建的分析工具和測(cè)試工具也逐漸被工業(yè)界所采納并使用.目前，比較著名的符號(hào)執(zhí)行工具有KLEE、SAGE、Pex、SPF、DART、CUTE、S2E、Cloud9等.

符號(hào)執(zhí)行技術(shù)對(duì)程序的路徑空間進(jìn)行遍歷，是一種路徑敏感的分析技術(shù)，因此分析精度高.但是，當(dāng)被分析程序具有較大規(guī)模時(shí)，符號(hào)執(zhí)行面臨路徑空間爆炸問(wèn)題.為了提高符號(hào)執(zhí)行的可擴(kuò)展性和效率，近年來(lái)，研究人員開展了大量研究，并提出了多種優(yōu)化技術(shù).其中，將符號(hào)執(zhí)行與具體執(zhí)行相結(jié)合(稱為concolic execution)的思想的提出，對(duì)推動(dòng)符號(hào)執(zhí)行的發(fā)展起了重要作用.Godefroid、Sen等人提出了動(dòng)態(tài)符號(hào)執(zhí)行(dynamic symbolic execution)技術(shù)，將具體執(zhí)行(如隨機(jī)測(cè)試)和靜態(tài)符號(hào)執(zhí)行方法結(jié)合起來(lái)，使用具體執(zhí)行中的信息輔助符號(hào)執(zhí)行，增加覆蓋率，并能減少符號(hào)執(zhí)行的約束求解開銷.動(dòng)態(tài)符號(hào)執(zhí)行有效緩解了第三方庫(kù)源碼不可見、復(fù)雜路徑條件(如非線性表達(dá)式、超越函數(shù)等)超出約束求解器能力范圍等靜態(tài)符號(hào)執(zhí)行面臨的挑戰(zhàn)性問(wèn)題.

Java PathFinder(JPF)是美國(guó)NASA開發(fā)的面向Java字節(jié)碼程序的分析和驗(yàn)證工具[14].該工具最早是基于模型檢驗(yàn)思想設(shè)計(jì)的，用于檢測(cè)并發(fā)程序中的數(shù)據(jù)競(jìng)爭(zhēng)、死鎖等問(wèn)題.早期的JPF，將Java代碼翻譯為Promela代碼，然后使用模型檢驗(yàn)工具SPIN來(lái)檢驗(yàn)性質(zhì)，并應(yīng)用于航空領(lǐng)域?qū)崟r(shí)操作系統(tǒng)DEOS的驗(yàn)證中[15].后來(lái)，該工具逐漸引入靜態(tài)分析的思想，采用基于符號(hào)執(zhí)行的方法對(duì)軟件進(jìn)行分析和驗(yàn)證[16].JPF是NASA航天器控制軟件驗(yàn)證的重要工具，如勇氣號(hào)、機(jī)遇號(hào)火星探測(cè)器的控制軟件都采用JPF進(jìn)行了分析和驗(yàn)證.

4 面向航天嵌入式軟件的數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)技術(shù)

隨著航天軟件并發(fā)性不斷增強(qiáng)，數(shù)據(jù)訪問(wèn)沖突問(wèn)題已成為航天嵌入式軟件質(zhì)量保障中最迫切需要解決的問(wèn)題之一[17].數(shù)據(jù)訪問(wèn)沖突是指多個(gè)并發(fā)執(zhí)行流(如任務(wù)、中斷、線程)對(duì)同一數(shù)據(jù)單元進(jìn)行同時(shí)讀寫、且其中至少有一個(gè)操作是寫操作.由于數(shù)據(jù)訪問(wèn)沖突中涉及的兩次訪問(wèn)之間的次序不可確定，程序可能會(huì)因此產(chǎn)生異常行為，嚴(yán)重時(shí)甚至?xí)?dǎo)致軟件或系統(tǒng)失效.這類問(wèn)題的產(chǎn)生是由于航天器的不同器件之間、多個(gè)并發(fā)運(yùn)行的軟件之間存在復(fù)雜的數(shù)據(jù)交互，如果同步、互斥機(jī)制安排不當(dāng)，很容易產(chǎn)生數(shù)據(jù)競(jìng)爭(zhēng)、原子性破壞等數(shù)據(jù)訪問(wèn)沖突問(wèn)題，從而導(dǎo)致軟件和系統(tǒng)故障.已往的航天嵌入式軟件研制經(jīng)驗(yàn)表明，數(shù)據(jù)競(jìng)爭(zhēng)問(wèn)題僅在特定外部環(huán)境和輸入下才會(huì)出現(xiàn)，難以測(cè)試、調(diào)試和復(fù)現(xiàn)，問(wèn)題遺漏率較高.同時(shí)，因?yàn)檫@類問(wèn)題涉及到并發(fā)軟件之間的復(fù)雜交疊和時(shí)序關(guān)系，所以其檢測(cè)比較困難.基于模型檢驗(yàn)和符號(hào)執(zhí)行的Java PathFinder(JPF)、基于抽象解釋的靜態(tài)分析工具AstreeA都支持多線程程序的數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè).

航天嵌入式軟件的典型并發(fā)特征是中斷驅(qū)動(dòng).由于中斷導(dǎo)致的數(shù)據(jù)競(jìng)爭(zhēng)問(wèn)題，曾經(jīng)導(dǎo)致多起系統(tǒng)故障，比如某衛(wèi)星帆板驅(qū)動(dòng)線路盒轉(zhuǎn)角跳變導(dǎo)致控制偏差[18].據(jù)中國(guó)空間技術(shù)研究院軟件產(chǎn)品保證中心統(tǒng)計(jì)，在航天器總裝測(cè)試(AIT.)階段發(fā)現(xiàn)的軟件質(zhì)量問(wèn)題中，約80%都與中斷密切相關(guān)[18]，這已經(jīng)成為影響我國(guó)航天任務(wù)完成的技術(shù)障礙.因此，研究針對(duì)中斷并發(fā)、中斷與任務(wù)共存相關(guān)數(shù)據(jù)競(jìng)爭(zhēng)分析方法和工具具有重要現(xiàn)實(shí)意義.中斷驅(qū)動(dòng)型軟件包含常規(guī)任務(wù)、中斷處理函數(shù)等成分，是一種特殊的并發(fā)軟件.一方面，中斷驅(qū)動(dòng)型軟件的分析面臨一般并發(fā)程序的共性問(wèn)題，即因?yàn)闋顟B(tài)的并發(fā)組合導(dǎo)致的整體狀態(tài)空間爆炸問(wèn)題；另一方面，與一般的多線程程序不同，因?yàn)橹袛嘤|發(fā)的不確定性和中斷控制的動(dòng)態(tài)性，中斷驅(qū)動(dòng)型程序的執(zhí)行過(guò)程，需要進(jìn)行特殊的語(yǔ)義解釋.

除了航天領(lǐng)域，汽車電子領(lǐng)域的軟件也常常包含中斷.Schwarz等[19]提出了一種針對(duì)中斷驅(qū)動(dòng)型程序的數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)方法，其主要針對(duì)汽車電子領(lǐng)域使用天花板協(xié)議(priority ceiling protocal)的中斷程序.其主要思想是在抽象解釋框架下，使用任務(wù)與中斷間的全局不變式，并基于該不變式計(jì)算共享變量的資源鎖，然后通過(guò)資源鎖來(lái)判定程序中是否存在數(shù)據(jù)競(jìng)爭(zhēng)，并開發(fā)了工具Goblint[20].目前，Goblint已成功應(yīng)用于OSEK程序、Linux設(shè)備驅(qū)動(dòng)程序等程序的數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)和鎖錯(cuò)誤檢測(cè).

5 國(guó)內(nèi)航天嵌入式軟件靜態(tài)分析工具研究

近年來(lái)，國(guó)內(nèi)學(xué)術(shù)界和工業(yè)界在將靜態(tài)分析技術(shù)與工具應(yīng)用于航天嵌入式軟件的質(zhì)量保證方面開展了不少研究.尤其，國(guó)內(nèi)航天軟件評(píng)測(cè)部門采用靜態(tài)分析技術(shù)也開發(fā)了一些面向航天軟件的靜態(tài)分析工具，并在實(shí)際航天軟件進(jìn)行了應(yīng)用，為航天軟件質(zhì)量保證提供了有力支撐.北京軒宇信息技術(shù)有限公司研發(fā)的C/C++靜態(tài)缺陷檢測(cè)工具Sunwise SpecChecker支持安全編碼標(biāo)準(zhǔn)符合性檢查、運(yùn)行時(shí)缺陷檢測(cè)和代碼質(zhì)量度量等，采用跨函數(shù)、跨中斷的抽象解釋技術(shù)對(duì)程序進(jìn)行高效的并發(fā)語(yǔ)義分析，除了支持如空指針、未初始化變量、數(shù)組越界、除零錯(cuò)、整數(shù)溢出等運(yùn)行時(shí)錯(cuò)誤的檢測(cè)，還支持中斷數(shù)據(jù)訪問(wèn)沖突缺陷的檢測(cè).該公司研制的針對(duì)C語(yǔ)言程序的單元與集成測(cè)試平臺(tái)Sunwise AUnit，采用了動(dòng)態(tài)符號(hào)執(zhí)行和約束求解技術(shù)來(lái)加速C程序測(cè)試用例的快速生成，提高了測(cè)試效率.這些工具已經(jīng)在中國(guó)空間技術(shù)研究院全面應(yīng)用，促進(jìn)了型號(hào)軟件質(zhì)量，并推廣至航空、電力等多個(gè)領(lǐng)域[21].王崑聲等[22]針對(duì)航天嵌入式軟件提出了一種基于屬性模型的運(yùn)行時(shí)錯(cuò)誤靜態(tài)分析方法，并開發(fā)了相應(yīng)的工具，在航天嵌入式軟件上開展了實(shí)驗(yàn).

在航天嵌入式軟件數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)方面，吳學(xué)光等[17]針對(duì)多重中斷航天嵌入式C程序開展了數(shù)據(jù)競(jìng)爭(zhēng)及原子性檢測(cè)相關(guān)研究，并開發(fā)了多重中斷環(huán)境下數(shù)據(jù)競(jìng)爭(zhēng)和原子性檢查工具M(jìn)IDAC.該工具支持共享變量分析、數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)、原子性違反檢測(cè)等.進(jìn)一步，WU等[23]在有界模型檢驗(yàn)框架下提出了一種面向多任務(wù)、多中斷嵌入式軟件的數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)方法，將可能產(chǎn)生數(shù)據(jù)競(jìng)爭(zhēng)的路徑條件編碼為SAT/SMT公式，然后通過(guò)判斷公式的不可滿足性來(lái)消除數(shù)據(jù)競(jìng)爭(zhēng)誤報(bào).進(jìn)一步，WU等[24]提出了基于順序化的中斷驅(qū)動(dòng)型程序的數(shù)值性質(zhì)分析方法，將中斷驅(qū)動(dòng)型程序順序化為帶非確定性的順序程序，然后使用面向順序程序的數(shù)值性質(zhì)分析方法來(lái)分析順序化中斷驅(qū)動(dòng)型程序，以檢查中斷驅(qū)動(dòng)型程序中的數(shù)值相關(guān)運(yùn)行時(shí)錯(cuò)誤，并在真實(shí)航天軟件上開展了實(shí)驗(yàn).陳睿等[18]以航天嵌入式軟件數(shù)據(jù)競(jìng)爭(zhēng)案例庫(kù)為基礎(chǔ)，經(jīng)過(guò)系統(tǒng)分析，提出了刻畫有害中斷數(shù)據(jù)競(jìng)爭(zhēng)的7種缺陷模式，并針對(duì)其中最常見且最難解決的單變量訪問(wèn)序模式，提出一種支持過(guò)程間分析、中斷并發(fā)分析的高效檢測(cè)方法，設(shè)計(jì)并實(shí)現(xiàn)了相應(yīng)的檢測(cè)工具SpaceDRC，在多個(gè)航天重點(diǎn)型號(hào)中進(jìn)行了應(yīng)用.進(jìn)一步，陳睿等[25]設(shè)計(jì)開發(fā)了航天嵌入式軟件中斷數(shù)據(jù)訪問(wèn)沖突基準(zhǔn)測(cè)試集程序RaceBench，對(duì)SpaceDRC工具進(jìn)行了評(píng)估.

表1 典型靜態(tài)分析技術(shù)及其在航天嵌入式軟件中的適用方面與可改進(jìn)方面Tab.1 Static analysis techniques and its applications to aerospace embedded software

6 結(jié) 論

本文首先分析了航天嵌入式軟件的代碼特征及常見錯(cuò)誤.在此基礎(chǔ)上，介紹了適合于航天嵌入式軟件錯(cuò)誤檢測(cè)的靜態(tài)分析技術(shù)，包括抽象解釋、符號(hào)執(zhí)行、數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)等.然后，介紹了國(guó)內(nèi)近年來(lái)在面向航天嵌入式軟件的靜態(tài)分析技術(shù)與工具方面的研究進(jìn)展.表1給出了本文主要介紹的抽象解釋、符號(hào)執(zhí)行兩種典型靜態(tài)分析技術(shù)及其優(yōu)缺點(diǎn)，以及在航天嵌入式軟件中的適用方面與可改進(jìn)方面.限于篇幅,本文只是簡(jiǎn)述了面向航天嵌入式軟件的一部分靜態(tài)分析技術(shù)及其進(jìn)展[26].

雖然近年來(lái)國(guó)內(nèi)在面向航天嵌入式軟件的靜態(tài)分析技術(shù)與工具方面取得了不少進(jìn)展，未來(lái)需要進(jìn)一步研究和開發(fā)適合于航天嵌入式軟件特征、支持領(lǐng)域關(guān)鍵模塊(如數(shù)據(jù)緩沖區(qū)等)、面向更多類型性質(zhì)與缺陷、面向航天嵌入式軟件未來(lái)發(fā)展方向(如多核等)的靜態(tài)分析技術(shù)與工具，為載人航天、探月工程和衛(wèi)星等國(guó)家重大科技專項(xiàng)中的軟件質(zhì)量保障提供支撐.