梁 昊 艾云峰 沈懷榮 趙永超

1.裝備學(xué)院研究生管理大隊(duì)，北京 101416 2.中國科學(xué)院大學(xué)工程管理與信息技術(shù)學(xué)院, 北京100049 3.裝備學(xué)院航天裝備系，北京 101416 4.國防大學(xué)作戰(zhàn)與指揮訓(xùn)練教研部, 北京 100091

?

航天軟件中多重中斷程序的動(dòng)態(tài)檢測方法研究

梁 昊1艾云峰2沈懷榮3趙永超4

1.裝備學(xué)院研究生管理大隊(duì)，北京 101416 2.中國科學(xué)院大學(xué)工程管理與信息技術(shù)學(xué)院, 北京100049 3.裝備學(xué)院航天裝備系，北京 101416 4.國防大學(xué)作戰(zhàn)與指揮訓(xùn)練教研部, 北京 100091

隨著控制系統(tǒng)軟硬件平臺(tái)的設(shè)計(jì)復(fù)雜度不斷增加，特別是飛行控制系統(tǒng)中集成的傳感器不斷增多，中斷數(shù)量也隨之不斷增加。本文根據(jù)飛控系統(tǒng)的具體特點(diǎn)，使用標(biāo)記遷移系統(tǒng)對(duì)多重中斷并發(fā)程序進(jìn)行建模，提出了原子性違背和數(shù)據(jù)競爭的形式化描述，運(yùn)用動(dòng)態(tài)偏序化簡算法對(duì)程序的狀態(tài)空間進(jìn)行化簡，并設(shè)計(jì)實(shí)現(xiàn)了多重中斷控制系統(tǒng)程序的動(dòng)態(tài)檢測工具，實(shí)驗(yàn)結(jié)果表明該檢測算法可以在滿足對(duì)多重中斷并發(fā)程序錯(cuò)誤檢測的基礎(chǔ)上，大大的縮短檢測時(shí)間。

多重中斷；數(shù)據(jù)競爭；原子性違背；偏序化簡

當(dāng)前多重中斷程序在航空航天控制軟件，特別是在飛行控制軟件中得到了廣泛應(yīng)用。由于中斷嵌套的原因，多重中斷程序的執(zhí)行路徑存在大量交疊，使得程序的運(yùn)行過程具有強(qiáng)烈的復(fù)雜性、不確定性和難以預(yù)期性，這給航空航天控制軟件設(shè)計(jì)與測試工作帶來了大量的困難。研究者針對(duì)多重中斷程序的錯(cuò)誤檢測已經(jīng)展開了一系列的研究，提出了靜態(tài)分析和動(dòng)態(tài)驗(yàn)證2種主要的測試方法。

靜態(tài)分析的基本原理是不編譯運(yùn)行程序，將程序抽象成模型，對(duì)模型中共享對(duì)象的讀寫操作進(jìn)行檢查，如GOBLINT[1]和國防科技大學(xué)設(shè)計(jì)的MIDAC[2]檢測工具。靜態(tài)測試主要缺點(diǎn)在于無法避免“狀態(tài)空間爆炸”和誤報(bào)率較高的問題。

動(dòng)態(tài)驗(yàn)證方法的基本原理是利用給定測試數(shù)據(jù)，驅(qū)動(dòng)被測試程序執(zhí)行，并在執(zhí)行的過程中對(duì)程序進(jìn)行驗(yàn)證。該方法可有效的避免可執(zhí)行程序代碼(包括編譯、運(yùn)行連接庫等)與程序模型之間存在的不一致問題。與靜態(tài)分析相比較，動(dòng)態(tài)驗(yàn)證不會(huì)產(chǎn)生誤報(bào)，同時(shí)可避免復(fù)雜的建模、語義差異和約束求解。VeriSoft[3]是一個(gè)采用動(dòng)態(tài)驗(yàn)證方法的典型測試工具，它面向可執(zhí)行程序，能夠驗(yàn)證由C，C++，Tcl等語言編寫的可執(zhí)行代碼。計(jì)算機(jī)技術(shù)與應(yīng)用研究所提出的多重中斷程序測試框架[4]也是一種動(dòng)態(tài)測試工具，它的主要設(shè)計(jì)思想是對(duì)中斷進(jìn)行兩兩對(duì)比測試，通過不斷提高2個(gè)中斷的觸發(fā)頻率來加速并發(fā)錯(cuò)誤的出現(xiàn)。但是該方法只能針對(duì)2個(gè)外部中斷進(jìn)行獨(dú)立測試，且需要人為干預(yù)，無法保證測試的覆蓋率。

文獻(xiàn)[5-6]所采用的類線程測試方法為多重中斷的測試提出了新的思路，其主要原理是將中斷程序改寫為“語義”等價(jià)的多線程程序，然后使用Locksmith races以及cXprop race對(duì)多線程程序進(jìn)行測試。但該方法在對(duì)多重中斷程序進(jìn)行改寫后，需要操作系統(tǒng)的內(nèi)核支持，而控制軟件特別是飛行控制軟件多使用無操作系統(tǒng)的多重中斷設(shè)計(jì)方式，因此該方法在工程應(yīng)用方面存在無法彌補(bǔ)的弊端。

本文在參考了國內(nèi)外已有技術(shù)的基礎(chǔ)上，將用于多線程并發(fā)程序驗(yàn)證的基于Happens-Before關(guān)系的動(dòng)態(tài)偏序化簡思想在功能上進(jìn)行了延伸和拓展，使其可以處理不基于操作系統(tǒng)的多重中斷程序。首先描述了多重中斷程序的系統(tǒng)建模，并給出了原子性違背和數(shù)據(jù)競爭兩種并發(fā)錯(cuò)誤的形式化描述；然后介紹了動(dòng)態(tài)偏序化簡算法，之后對(duì)該算法進(jìn)行改進(jìn)，使之可以對(duì)多重中斷程序進(jìn)行測試，并介紹了該算法中的并發(fā)錯(cuò)誤檢測模塊；最后通過實(shí)驗(yàn)對(duì)比證明了所提出的動(dòng)態(tài)驗(yàn)證方法在實(shí)際程序測試方面的準(zhǔn)確性和有效性。

1 多重中斷程序建模與并發(fā)錯(cuò)誤定義

1.1 多重中斷程序建模

本文使用了標(biāo)記遷移系統(tǒng)對(duì)多重中斷并發(fā)程序進(jìn)行建模，標(biāo)記遷移系統(tǒng)(Labeled Transition Systems, LTS)[7]的具體描述如下：

定義1 LTS(標(biāo)記遷移系統(tǒng))是一個(gè)四元組M=(S,init,T,R),其中：S表示并發(fā)程序的狀態(tài)集合；init表示初始狀態(tài)(也可表示為s0)，并且有init∈S；T表示遷移集合；R表示遷移關(guān)系集合。

在控制軟件中，往往包含1個(gè)主函數(shù)main和若干中斷服務(wù)函數(shù)interrupts。本文將由main函數(shù)和其調(diào)用的普通函數(shù)記作一個(gè)整體，將中斷服務(wù)函數(shù)的標(biāo)記集合為IR，則多重中斷程序的整體標(biāo)識(shí)集合為：Fid={main}∪IR，fid∈Fid,該標(biāo)識(shí)對(duì)應(yīng)于每一個(gè)具體的函數(shù)(中斷服務(wù)函數(shù)或者main函數(shù))。

不同中斷服務(wù)函數(shù)對(duì)于全局共享對(duì)象的讀寫操作，稱之為可見操作，對(duì)于不同中斷服務(wù)函數(shù)中本地對(duì)象的讀寫操作，稱之為不可見操作。由于不可見操作對(duì)共享變量沒有影響，因此下文中只對(duì)可見操作進(jìn)行討論。

1.2 多重中斷程序中并發(fā)錯(cuò)誤定義

在描述多重中斷程序并發(fā)錯(cuò)誤之前必須首先介紹2個(gè)相關(guān)概念。

定義4R∈T×T是獨(dú)立關(guān)系，當(dāng)且僅當(dāng)對(duì)于每一個(gè)∈R，如果它們是相互獨(dú)立的，則必須滿足下面2個(gè)關(guān)系：

獨(dú)立關(guān)系的定義反映了遷移t1,t2作用于同一個(gè)全局狀態(tài)中2個(gè)不同的局部狀態(tài)；或者t1,t2是作用于同一個(gè)局部變量上的2個(gè)讀操作，此時(shí)交換它們的執(zhí)行次序?qū)Τ绦虻倪\(yùn)行無影響。

1.2.1 原子性與原子性違背

原子性的定義[8]：一個(gè)事務(wù)中的所有操作，要么全部完成，要么全部不完成，不會(huì)結(jié)束或中斷在某一個(gè)環(huán)節(jié)，事物在執(zhí)行過程中發(fā)生錯(cuò)誤會(huì)被回滾到初始狀態(tài)。

多重中斷中C語言程序的原子性違背的形式化描述為：給定1個(gè)原子塊A，它的遷移序列為：TA={t1,t2,…,tn}，?i∈[1,n],ti∈TA，即ti處在原子塊A中，原子塊中所有寫操作的集合OPW(A)={op|op∈OP(A),and,op(A)=write}，原子塊中所有讀操作的集合OPR(A)={op|op∈OP(A),and,op(A)=read}，其中op的含義為操作；OP(A)為原子塊A中所有可見操作的集合。如果?t?TA，并且t與ti是非相互獨(dú)立且可同時(shí)執(zhí)行的遷移，若(OPR(A)∩opw(t))∪(opr(t)∩OPW(A))∪(OPW(A)∩opw(t))≠φ，則會(huì)引發(fā)原子性違背錯(cuò)誤。其中opw(t)，opr(t)分別表示op(t)=write，op(t)=read。

1.2.2 數(shù)據(jù)競爭

數(shù)據(jù)競爭的定義[9-10]：2個(gè)線程在沒有同步操作保護(hù)的前提下同時(shí)訪問一塊共享內(nèi)存，且至少其中有一個(gè)訪問為寫操作。

多重中斷中C語言程序數(shù)據(jù)競爭的形式化描述為：對(duì)于程序中的任意一個(gè)狀態(tài)s，在其上的所有寫操作的集合為：OPW(s)={op|op∈OP(s),and,op(s)=write}，所有讀操作的集合為：OPR(s)={op|op∈OP(s),and,op(s)=read}，如果存在2個(gè)遷移t和t′在狀態(tài)s上都是可執(zhí)行且非相互獨(dú)立的，若t和t′分別屬于2個(gè)優(yōu)先級(jí)不同的中斷函數(shù)，t和t′有一個(gè)操作在集合OPW(s)中，則狀態(tài)s存在數(shù)據(jù)競爭錯(cuò)誤。

數(shù)據(jù)競爭與原子性不同，原子性定義的描述必然是針對(duì)多個(gè)并發(fā)程序狀態(tài)而言的，即這個(gè)代碼段內(nèi)包含了一系列的狀態(tài)和遷移；而數(shù)據(jù)競爭主要針對(duì)一個(gè)狀態(tài)和這個(gè)狀態(tài)的可執(zhí)行遷移而言。

2 面向多重中斷程序的動(dòng)態(tài)驗(yàn)證算法設(shè)計(jì)

2.1 動(dòng)態(tài)偏序化簡

上文已經(jīng)提到，控制系統(tǒng)并發(fā)程序在動(dòng)態(tài)執(zhí)行的過程中狀態(tài)空間會(huì)變得極其巨大，甚至出現(xiàn)狀態(tài)空間爆炸的問題。為此本文將基于Happens-Before關(guān)系的多線程程序動(dòng)態(tài)偏序化簡(Dynamic Partial-Order Reduction，以下簡稱DPOR)[11-12]方法引入到多重中斷程序的狀態(tài)空間化簡中。

動(dòng)態(tài)偏序化簡的主要思想就是計(jì)算各個(gè)狀態(tài)的Persistent 集合。但傳統(tǒng)的DPOR算法在處理多重中斷程序中有2個(gè)缺陷：1)無法對(duì)包含無限循環(huán)的程序進(jìn)行化簡[11]，而控制系統(tǒng)的并發(fā)程序往往會(huì)普遍使用有無限循環(huán)的設(shè)計(jì)方式；2)DPOR算法無法對(duì)包含優(yōu)先級(jí)的中斷服務(wù)函數(shù)作出處理。

2.2 面向多重中斷的動(dòng)態(tài)偏序化簡算法

針對(duì)2.1節(jié)中提出的問題，本文在傳統(tǒng)的基于persistent集合的DPOR算法基礎(chǔ)上，引入了sleep集合的概念。一個(gè)狀態(tài)s的sleep集合表示在狀態(tài)s上可執(zhí)行但又沒有必要執(zhí)行的遷移的集合，記為s.sleep。引入sleep集合可以進(jìn)一步排除DPOR算法對(duì)相互獨(dú)立關(guān)系遷移的選取，同時(shí)將被檢索過的遷移加入sleep集合，可以避免DPOR算法反復(fù)搜索已經(jīng)執(zhí)行過的遷移，這點(diǎn)對(duì)含有循環(huán)的程序格外重要，它可以減少s.enabled集合中的遷移，從而避免由無限循環(huán)所帶來的程序狀態(tài)空間的無限制增長，如圖 1中的第32行所示。

圖1 DPOR算法描述

圖1的算法設(shè)計(jì)中，采用基于深度優(yōu)先的搜索方法來對(duì)程序的狀態(tài)空間進(jìn)行搜索。算法中使用集合FID來代表程序的函數(shù)空間，fid即為函數(shù)的唯一標(biāo)識(shí)，fid(s)返回動(dòng)態(tài)執(zhí)行過程中狀態(tài)s所處的當(dāng)前函數(shù)標(biāo)識(shí)，fid(t)返回遷移t所在的函數(shù)標(biāo)識(shí)。PRI的作用是記錄函數(shù)的優(yōu)先級(jí)，中斷服務(wù)函數(shù)的優(yōu)先級(jí)為其自身的優(yōu)先級(jí)，main函數(shù)的優(yōu)先級(jí)最低。通過在圖 1中第8，13，15行中，加入對(duì)函數(shù)優(yōu)先級(jí)的比較，實(shí)現(xiàn)了高優(yōu)先級(jí)的中斷服務(wù)函數(shù)可以打斷低優(yōu)先級(jí)的中斷服務(wù)函數(shù)和普通函數(shù)的執(zhí)行，這樣還可以進(jìn)一步縮減動(dòng)態(tài)執(zhí)行中的目標(biāo)程序狀態(tài)空間。

在DPOR算法中，控制執(zhí)行器記錄了包含全局對(duì)象的搜索堆棧S，s.backtrack為回溯集合表示需要搜索的狀態(tài)s的線程集合。s.done表示被檢測過的狀態(tài)s的線程集合，函數(shù)UPDATEBACKTRACESETS(S,t)的作用是動(dòng)態(tài)計(jì)算persistent集合，給定一個(gè)狀態(tài)s，狀態(tài)s的persistent集合不會(huì)在程序到達(dá)狀態(tài)s后立即被計(jì)算出來，而是在狀態(tài)s下使用深度優(yōu)先搜索的算法對(duì)persistent集合進(jìn)行計(jì)算。算法的具體描述如圖2所示。

圖2 UPDATEBACKTRACESETS算法描述

函數(shù)UPDATEBACKTRACESETS算法與經(jīng)典DPOR的回溯算法相同，只是在圖 2的第4行中，加入對(duì)于函數(shù)fid(td)的中斷允許標(biāo)志位的判斷，如果該中斷沒有被使能，則計(jì)算在狀態(tài)sd的回溯集合。關(guān)于DPOR的算法的詳細(xì)理論與數(shù)學(xué)證明請(qǐng)參考文獻(xiàn)[11]。

2.3 多重中斷程序并發(fā)錯(cuò)誤檢測算法

在圖 1所描述的算法中，函數(shù)DETECTERROR的作用是在狀態(tài)s處檢測是否存在原子性違背和數(shù)據(jù)競爭錯(cuò)誤，其算法實(shí)現(xiàn)如圖 3所示。

圖3 多重中斷程序并發(fā)錯(cuò)誤檢測算法

圖 3中第2～14行，按照文中對(duì)原子性違背形式化描述，設(shè)計(jì)了并發(fā)程序原子性違背錯(cuò)誤檢測方法，主要是檢測多重中斷程序中多變量讀寫時(shí)是否存在原子性違背錯(cuò)誤；第15，16行主要是檢測程序執(zhí)行過程中，高優(yōu)先級(jí)中斷打斷低優(yōu)先級(jí)中斷時(shí)，程序是否存在數(shù)據(jù)競爭的情況。

3 實(shí)驗(yàn)平臺(tái)和實(shí)驗(yàn)結(jié)果

3.1 實(shí)驗(yàn)平臺(tái)

多重中斷程序動(dòng)態(tài)測試工具構(gòu)架主要包含4個(gè)部分：程序分析器、中斷服務(wù)函數(shù)分析器、控制執(zhí)行器和中斷發(fā)生器。

圖4 多重中斷測試工具設(shè)計(jì)框架圖

中斷服務(wù)函數(shù)分析器的主要作用是識(shí)別程序的內(nèi)部和外部中斷，建立中斷觸發(fā)機(jī)制。控制執(zhí)行器的主要工作是接收由插裝、編譯后的被測試程序得到共享變量、函數(shù)注冊(cè)信息，并根據(jù)以上信息控制中斷發(fā)生器的中斷引號(hào)產(chǎn)生時(shí)間，在目標(biāo)程序執(zhí)行的過程中，使用DPOR算法對(duì)狀態(tài)空間進(jìn)行化簡，同時(shí)根據(jù)不同路徑的交疊執(zhí)行情況，判斷并發(fā)交疊中是否包含數(shù)據(jù)競爭、原子性違背錯(cuò)誤。中斷發(fā)生器的作用是在控制執(zhí)行器給定的信號(hào)驅(qū)使下，產(chǎn)生相應(yīng)的中斷，對(duì)于內(nèi)部中斷不進(jìn)行觸發(fā)，而是等待條件允許后，內(nèi)部中斷自身完成觸發(fā)執(zhí)行。目標(biāo)機(jī)的作用是接收中斷信號(hào)，動(dòng)態(tài)執(zhí)行被測試程序。

3.2 實(shí)驗(yàn)結(jié)果

表1 測試軟硬件平臺(tái)

被測試程序方面，選用了基于DSP的飛行控制程序，基于AVR單片機(jī)的四旋翼飛行器控制程序。為了通過實(shí)驗(yàn)驗(yàn)證控制系統(tǒng)并發(fā)程序錯(cuò)誤檢測算法的執(zhí)行效率，對(duì)目標(biāo)程序的中斷數(shù)量進(jìn)行了修改。具體的實(shí)驗(yàn)結(jié)果如表2所示。

表2 實(shí)驗(yàn)結(jié)果

在以上的表格中，用“/”表示程序無法在24 h(86400s)內(nèi)測試完成。從表 3可以看出，被測程序包含的中斷數(shù)、搜索遷移數(shù)和檢測時(shí)間等3個(gè)比較指標(biāo)，在使用了偏序化簡算法以后，執(zhí)行時(shí)間大大縮短，提高了檢測效率。

表3中由于多重中斷測試框架只能對(duì)中斷服務(wù)函數(shù)進(jìn)行兩兩比對(duì)測試，只能通過手動(dòng)來完成全部的測試，所以無法統(tǒng)計(jì)測試時(shí)間。在類線程的測試方法中，由于其需要操作系統(tǒng)內(nèi)核的支持，所以DSP平臺(tái)無法完成測試，在AVR平臺(tái)中，本文使用了TinyOS操作系統(tǒng)來完成類線程測試。通過實(shí)驗(yàn)結(jié)果的對(duì)比，可以看出相對(duì)類線程測試本文設(shè)計(jì)的檢測算法擁有更高的檢測效率，而且在AVR3的試驗(yàn)中不但找到數(shù)據(jù)競爭的存在，而且還發(fā)現(xiàn)了一個(gè)原子性違背錯(cuò)誤。

表3 實(shí)驗(yàn)結(jié)果

4 結(jié)束語

根據(jù)控制系統(tǒng)中多重中斷并發(fā)程序的相關(guān)特點(diǎn)，將基于線程的并發(fā)C語言程序狀態(tài)空間DPOR化簡算法應(yīng)用于多重中斷程序的狀態(tài)空間化簡，極大地縮短了測試執(zhí)行時(shí)間。根據(jù)原性子違背和數(shù)據(jù)競爭的經(jīng)典定義，在標(biāo)記遷移系統(tǒng)中給出了這兩種并發(fā)錯(cuò)誤的形式化描述，并完成對(duì)原子性違背和數(shù)據(jù)競爭檢測的算法設(shè)計(jì)，最終實(shí)現(xiàn)了對(duì)于包含多重中斷控制系統(tǒng)的并發(fā)錯(cuò)誤檢測。由于檢測算法基于Happens-Before關(guān)系，因此在數(shù)據(jù)競爭的檢測方面，可以報(bào)告出存在的數(shù)據(jù)競爭，但還無法區(qū)分是良性的數(shù)據(jù)競爭還是惡性的數(shù)據(jù)競爭。

[1] Hatcli J Robby, Dwyer M B. Verifying Atomicity Speci-fications for Concurrent Object-oriented Software Using Model-checking[C]//LNCS 2937: Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004), Venice, Italy, Jan 11-13, 2004. Berlin, Heidelberg: Springer-Verlag, 2004: 175-190.

[2] 吳學(xué)光，文艷軍，王戟,等.多重中斷數(shù)據(jù)競爭及原子性違背檢測[J].計(jì)算機(jī)科學(xué)與探索,2011,12(3):1086-1093.(Wu Xueguang, Wen Yanjun, Wang Ji, et al. Data Race and Atomicity Checking for C Programs with Multiple Interruptions[J]. Journal of Frontiers of Computer Science and Technology,2011,12(3):1086-1093.)

[3] Juergen Dingel. Computer-Assisted Assume/Guarantee Reasoning with VeriSoft[C]. In Proceedings of the 25th International Conference on Software Engineering(ICSE'03). Washington, DC, USA: IEEE Computer Society press,2009:138-148.

[4] 傅修峰，陳麗容.多重中斷程序測試框架[J].計(jì)算機(jī)工程與設(shè)計(jì),2012,2(2):617-623.(Fu Xiufeng, Chen Lirong. Frameork for Testing Multiple Interrupts Program[J]. Computer Engineering and Design, 2012,2(2):617-623.)

[5] John Regehr, Nathan Cooprider. Interrupt Verifition via Thread Verification[J]. Electronic Notes in Theoretical Computer Science, 2007,174(9): 139-150.

[6] Wanja Hofer, Daniel Lohmann, Fabian Scheler, et al. Sloth: Threads as Interrupts[C]. Proceedings of the 30th IEEE Real-Time Systems Symposium (RTSS ’09) Washington, DC, USA: IEEE Computer Society Press, 2009:215-228.

[7] Chaki S, Clarke E M, Ouaknine J, et al. Automated, Compositional and Iterative Deadlock Detection[C]. Proc. of the 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-design. Washington, DC, USA: IEEE Press, 2004: 201-210.

[8] Abraham Silberschatz, Peter Baer Galvin, Greg Gagne. Operating System Concepts (8th Edition)[M]. 2009 John Wiley & Sons, Inc:733-734.

[9] Netzer R H B. Race Condition Detection for Debugging Shared-Memory Parallel Programs[D].Madison, WI, USA: University of Wisconsin, 1991.

[10] Netzer R H B. What are Race Conditions? Some Issues and Formalizations[J]. ACM Letters on Programming Languages and Systems,1992,1(1):74-88.

[11] Cormac Flanagan , Patrice Godefroid. Dynamic Partial-order Reduction for Model Checking Software[C]. In Proceedings of POPL’05,Long Beach, California, USA: ACM press, 2005:110-121.

[12] Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems-An Approach to the State-Explosion Problem [M]. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1996:27-78.

DynamicTestingMethodforProgramwithMultipleInterruptsinAerospaceSoftware

LIANG Hao1AI Yunfeng2SHEN Huairong3ZHAO Yongchao4
1. Company of Postgraduate Management, the Academy of Equipment, Beijing 101416, China 2. College of Engineering & Information Technology, University of Chinese Academy of Sciences, Beijing 100049, China 3. Department of Space Equipment, the Academy of Equipment, Beijing 101416, China 4. National Defense University, Department of Battle Command and Training, Beijing 100091, China

Inrecentyears,withincreasingdegreeofdesigncomplexityoncontrolsystem,especiallyforflyingcontrolsystemintegratedwithincreasingnumberofsensors,thereisagrowingnumberofinterruptsincontrolsystem.TheLTSisusedasthesystemmodelinmultipleinterruptionsprogram,theformaldescriptionforatomicityviolationanddataraceispresented,theDPORalgorithmisusedtoreducethespaceofprogramstateandthedynamictestingtoolisdesignedforcontrolsystemunderthemultipleinterruptions.Atlast,theexperimentalresultsshowthatthistestingmethodcannotonlytestdugforthemultipleinterruptprogram,butalsocanlargelyreducethetestingtime.

Multipleinterrupt;Datarace;Atomicityviolation; DPOR

2014-03-11

梁昊(1981-)，男，北京人，博士研究生，主要研究方向?yàn)楸靼l(fā)射理論與技術(shù)；艾云峰(1979-)，男，濟(jì)南人，博士，副教授，碩士生導(dǎo)師，主要研究方向?yàn)榍度胧较到y(tǒng)實(shí)踐、實(shí)時(shí)嵌入式操作系統(tǒng)、智能交通、嵌入式系統(tǒng)建模與測試；沈懷榮(1954-)，男，安徽舒城人，博士，教授，博士生導(dǎo)師，主要研究方向?yàn)楸靼l(fā)射理論與技術(shù)；趙永超(1982-)，男，石家莊人，博士后，主要研究方向?yàn)檠b備論證作戰(zhàn)數(shù)據(jù)與作戰(zhàn)模擬。

TP311.5

： A

1006-3242(2014)05-0059-06