航天軟件中多重中斷程序的動態檢測方法研究

梁 昊 艾云峰 沈懷榮 趙永超

1.裝備學院研究生管理大隊，北京 101416 2.中國科學院大學工程管理與信息技術學院, 北京100049 3.裝備學院航天裝備系，北京 101416 4.國防大學作戰與指揮訓練教研部, 北京 100091

?

航天軟件中多重中斷程序的動態檢測方法研究

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

1.裝備學院研究生管理大隊，北京 101416 2.中國科學院大學工程管理與信息技術學院, 北京100049 3.裝備學院航天裝備系，北京 101416 4.國防大學作戰與指揮訓練教研部, 北京 100091

隨著控制系統軟硬件平臺的設計復雜度不斷增加，特別是飛行控制系統中集成的傳感器不斷增多，中斷數量也隨之不斷增加。本文根據飛控系統的具體特點，使用標記遷移系統對多重中斷并發程序進行建模，提出了原子性違背和數據競爭的形式化描述，運用動態偏序化簡算法對程序的狀態空間進行化簡，并設計實現了多重中斷控制系統程序的動態檢測工具，實驗結果表明該檢測算法可以在滿足對多重中斷并發程序錯誤檢測的基礎上，大大的縮短檢測時間。

多重中斷；數據競爭；原子性違背；偏序化簡

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

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

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

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

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

1 多重中斷程序建模與并發錯誤定義

1.1 多重中斷程序建模

本文使用了標記遷移系統對多重中斷并發程序進行建模，標記遷移系統(Labeled Transition Systems, LTS)[7]的具體描述如下：

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

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

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

1.2 多重中斷程序中并發錯誤定義

在描述多重中斷程序并發錯誤之前必須首先介紹2個相關概念。

定義4R∈T×T是獨立關系，當且僅當對于每一個∈R，如果它們是相互獨立的，則必須滿足下面2個關系：

獨立關系的定義反映了遷移t1,t2作用于同一個全局狀態中2個不同的局部狀態；或者t1,t2是作用于同一個局部變量上的2個讀操作，此時交換它們的執行次序對程序的運行無影響。

1.2.1 原子性與原子性違背

原子性的定義[8]：一個事務中的所有操作，要么全部完成，要么全部不完成，不會結束或中斷在某一個環節，事物在執行過程中發生錯誤會被回滾到初始狀態。

多重中斷中C語言程序的原子性違背的形式化描述為：給定1個原子塊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是非相互獨立且可同時執行的遷移，若(OPR(A)∩opw(t))∪(opr(t)∩OPW(A))∪(OPW(A)∩opw(t))≠φ，則會引發原子性違背錯誤。其中opw(t)，opr(t)分別表示op(t)=write，op(t)=read。

1.2.2 數據競爭

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

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

數據競爭與原子性不同，原子性定義的描述必然是針對多個并發程序狀態而言的，即這個代碼段內包含了一系列的狀態和遷移；而數據競爭主要針對一個狀態和這個狀態的可執行遷移而言。

2 面向多重中斷程序的動態驗證算法設計

2.1 動態偏序化簡

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

動態偏序化簡的主要思想就是計算各個狀態的Persistent 集合。但傳統的DPOR算法在處理多重中斷程序中有2個缺陷：1)無法對包含無限循環的程序進行化簡[11]，而控制系統的并發程序往往會普遍使用有無限循環的設計方式；2)DPOR算法無法對包含優先級的中斷服務函數作出處理。

2.2 面向多重中斷的動態偏序化簡算法

針對2.1節中提出的問題，本文在傳統的基于persistent集合的DPOR算法基礎上，引入了sleep集合的概念。一個狀態s的sleep集合表示在狀態s上可執行但又沒有必要執行的遷移的集合，記為s.sleep。引入sleep集合可以進一步排除DPOR算法對相互獨立關系遷移的選取，同時將被檢索過的遷移加入sleep集合，可以避免DPOR算法反復搜索已經執行過的遷移，這點對含有循環的程序格外重要，它可以減少s.enabled集合中的遷移，從而避免由無限循環所帶來的程序狀態空間的無限制增長，如圖 1中的第32行所示。

圖1 DPOR算法描述

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

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

圖2 UPDATEBACKTRACESETS算法描述

函數UPDATEBACKTRACESETS算法與經典DPOR的回溯算法相同，只是在圖 2的第4行中，加入對于函數fid(td)的中斷允許標志位的判斷，如果該中斷沒有被使能，則計算在狀態sd的回溯集合。關于DPOR的算法的詳細理論與數學證明請參考文獻[11]。

2.3 多重中斷程序并發錯誤檢測算法

在圖 1所描述的算法中，函數DETECTERROR的作用是在狀態s處檢測是否存在原子性違背和數據競爭錯誤，其算法實現如圖 3所示。

圖3 多重中斷程序并發錯誤檢測算法

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

3 實驗平臺和實驗結果

3.1 實驗平臺

多重中斷程序動態測試工具構架主要包含4個部分：程序分析器、中斷服務函數分析器、控制執行器和中斷發生器。

圖4 多重中斷測試工具設計框架圖

中斷服務函數分析器的主要作用是識別程序的內部和外部中斷，建立中斷觸發機制。控制執行器的主要工作是接收由插裝、編譯后的被測試程序得到共享變量、函數注冊信息，并根據以上信息控制中斷發生器的中斷引號產生時間，在目標程序執行的過程中，使用DPOR算法對狀態空間進行化簡，同時根據不同路徑的交疊執行情況，判斷并發交疊中是否包含數據競爭、原子性違背錯誤。中斷發生器的作用是在控制執行器給定的信號驅使下，產生相應的中斷，對于內部中斷不進行觸發，而是等待條件允許后，內部中斷自身完成觸發執行。目標機的作用是接收中斷信號，動態執行被測試程序。

3.2 實驗結果

表1 測試軟硬件平臺

被測試程序方面，選用了基于DSP的飛行控制程序，基于AVR單片機的四旋翼飛行器控制程序。為了通過實驗驗證控制系統并發程序錯誤檢測算法的執行效率，對目標程序的中斷數量進行了修改。具體的實驗結果如表2所示。

表2 實驗結果

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

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

表3 實驗結果

4 結束語

根據控制系統中多重中斷并發程序的相關特點，將基于線程的并發C語言程序狀態空間DPOR化簡算法應用于多重中斷程序的狀態空間化簡，極大地縮短了測試執行時間。根據原性子違背和數據競爭的經典定義，在標記遷移系統中給出了這兩種并發錯誤的形式化描述，并完成對原子性違背和數據競爭檢測的算法設計，最終實現了對于包含多重中斷控制系統的并發錯誤檢測。由于檢測算法基于Happens-Before關系，因此在數據競爭的檢測方面，可以報告出存在的數據競爭，但還無法區分是良性的數據競爭還是惡性的數據競爭。

[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] 吳學光，文艷軍，王戟,等.多重中斷數據競爭及原子性違背檢測[J].計算機科學與探索,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].計算機工程與設計,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-)，男，北京人，博士研究生，主要研究方向為兵器發射理論與技術；艾云峰(1979-)，男，濟南人，博士，副教授，碩士生導師，主要研究方向為嵌入式系統實踐、實時嵌入式操作系統、智能交通、嵌入式系統建模與測試；沈懷榮(1954-)，男，安徽舒城人，博士，教授，博士生導師，主要研究方向為兵器發射理論與技術；趙永超(1982-)，男，石家莊人，博士后，主要研究方向為裝備論證作戰數據與作戰模擬。

TP311.5

： A

1006-3242(2014)05-0059-06