控制系統多重中斷并發程序測試動態工具設計

梁 昊，艾云峰，陳麗容，沈懷榮，趙永超

（1.裝備學院 研究生管理大隊，北京101416；2.中國航天科工集團第二研究院706所，北京100854；3.中國科學院大學 工程管理與信息技術學院，北京100049；4.裝備學院 航天裝備系，北京101416；5.國防大學 作戰與指揮訓練教研部，北京100091）

0 引 言

當前多重中斷程序在自動控制系統軟件中得到了廣泛的應用，但是由于多重中斷程序在執行過程中并發中斷交疊路徑的復雜性、不確定性、難以預期性，給軟件的設計與測試工作帶來了大量困難。當前在多重中斷錯誤檢測工具設計方面主要采用靜態分析和動態驗證兩種方案。

靜態分析測試工具的基本思想是不編譯運行程序，將程序抽象成模型，對模型中的共享對象讀寫操作進行檢查，如GOBLINT［1］和國防科技大學設計的MIDAC［2］檢測工具。MIDAC采用了函數摘要的技術來縮減靜態分析過程中需要遍歷的狀態空間。然而此類工具依然存在狀態空間爆炸和誤報較高的問題。在文檔［3，4］所描述的測試工具中提出了類線程的測試方法，其主要原理是將中斷服務函數改寫為“語義”等價的多線程程序，然后對多線程程序進行靜態測試，但該工具需要操作系統的內核支持。

動態驗證測試工具是在給定測試數據驅動下動態的執行被測試程序進行驗證。它避免了可執行程序代碼 （包括編譯、運行時庫等）與模型之間的不一致問題。動態驗證與靜態分析比較的優點是不會產生誤報；同時是可避免復雜的建模、語義差異和約束求解。其中典型的工具有：VeriSoft XT［5］，它可以檢測基于網絡系統的，包含大量I／O 操作的可執行并發程序。文獻 ［6］提出的多重中斷程序測試框架亦是一種動態測試工具，它的主要設計思想是對中斷進行兩兩測試，通過不斷提高觸發頻率來加速并發錯誤的出現。但是該工具只能針對兩個中斷進行測試，且需要人為干預，很難保證測試的覆蓋率。

本文在參考了國內外已有技術的基礎上，設計了基于動態驗證方案的多重中斷程序錯誤檢測工具，該工具可對不同硬件平臺、多種操作系統以及不基于操作系統的多重中斷程序并發錯誤進行檢測。本文首先介紹了面向控制系統的多重中斷程序測試工具的總體設計框架，之后分別詳細敘述了程序分析器、中斷分析器、控制執行器、中斷發生器的詳細設計方案；最后通過實驗對比證明了本測試工具的準確性和時效性。

1 測試工具總體設計概述

多重中斷程序動態測試工具構架主要包含4 個部分：程序分析器、程序插裝器、控制執行器、中斷發生器。其總體設計構架如圖1所示。

源程序首先經過程序分析器的分析之后得到多重中斷并發程序的模型，在此基礎上使用程序插裝器進一步對程序中的共享變量、中斷服務函數進行標記、插裝。在編譯的過程中，配合本文所設計的相應軟硬件平臺的C 語言測試庫文件，得到可被控制執行的目標程序，將目標程序燒寫入目標機，建立目標機和控制執行器的通信鏈路，啟動中斷發生器，目標機進入實時動態執行階段，控制執行器根據目標機反饋的執行狀態，通過動態測試算法實時地控制中斷發生器產生特定的中斷，直到所有的并發程序路徑被搜索完畢后測試結束，控制執行報告可能存在的并發錯誤。

1.1 程序分析器設計

程序分析器采用CIL （C intermediate language）［7］開源工具對被測是程序進行分析，創建被測試程序的標記遷移系統模型。其主要工作可以分為：①對并發程序進行分析，標記出程序中的共享變量，得到的共享變量及其相關操作，在程序中插入臨時變量記錄共享變量讀寫前后的取值，從而抽象出程序狀態空間；②將程序中的復雜語句轉換為：if、else、goto、while、賦值等5種簡單語句，抽象出程序遷移空間。由此可以獲得并發程序的標記遷移系統模型。

標記遷移系統 （labeled transition systems，LTS）［8］，其模型的具體描述如下：

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

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

1.2 程序插裝器設計

程序插裝器通過使用了CIL 工具的API［7］，完成對共享變量相關操作的插裝以及對中斷服務函數的插裝。針對共享變量的插裝操作主要包括：標記共享變量；注冊共享變量與中斷服務函數；識別對共享變量的相關操作等，具體描述見表1。

在中斷服務函數插裝方面，本文通過對表2的不同硬件平臺的中斷服務函數關鍵字的搜索，從原程序中找到中斷服務函數，并進行插裝。

1.3 控制執行器

控制執行器的主要作用是：接收由插裝、編譯后的被測試程序發送來的共享變量、中斷服務函數注冊信息，并根據以上信息控制中斷發生器產生中斷，在目標程序執行的過程中，對于目標程序執行路徑的狀態空間使用動態偏序化簡算法縮減進行化簡，提高執行效率。并依次遍歷縮減后的所有交疊路徑，覆蓋全部的狀態空間，同時根據不同路徑的交疊執行情況，判斷并發交疊中是否包含數據競爭、死鎖等并發錯誤。

表2 中斷服務函數關鍵字識別

1.3.1 多重中斷程序模型

通過表2在程序初始執行的過程中按照中斷服務函數被檢索到的次序對中斷服務函數進行注冊，并分配一個唯一的標識fid。假設一個多重中斷程序包含n個函數 （1個main函數，n－1個中斷服務函數），Fid ＝［1，2，…n］表示并發程序函數空間中函數的唯一標識的集合。本文在標記遷移系統的基礎上將函數的LTS擴展為一個五元組：每一個函數的標記遷移系統模型記作Mfid＝（Sfid，initfid，TPfid，R，IFlagefid），其中IFlage 表示允許中斷發生的標識，P表示函數的優先級，P 值越高該函數具有的優先級就越高，main函數的優先級最低。由此可以得到程序的并發模型為：M｜｜＝（S｜｜，init｜｜，T｜｜，R｜｜，IFlage｜｜）＝｜｜｜｜…｜｜＝＜S1×S2×…×Sn，（init1，init2，…，initn），

1.3.2 狀態空間化簡

本文在控制執行器的算法設計中使用了并發多線程程序化簡算法——動態偏序化簡 （dynamic partial－order reduction，DPOR）［9－11］的狀態空間化簡思想。

定義2 對于一個全局狀態Si＝（，…），當且僅當其上的遷移t在全局狀態Si上的一個局部狀態上是可執行的，此時不屬于Si的局部狀態有＝，則遷移t在全局狀態上才是可執行的，記作t∈Si.enable。

由于動態偏序化簡算法主要是用來化簡多線程程序的狀態空間，因此在多重中斷程序狀態空間的化簡方面無法直接使用。同時傳統的DPOR 算法無法對包含無限循環的程序進行化簡［11］，而控制系統并發程序往往會使用無限循環的設計方式。

針對以上的問題，本文設計了圖2中所描述的多重中斷程序動態偏序化簡算法。

本文在傳統的DPOR 算法中加入了一個hash表H 用來記錄檢索過的狀態，同時引入了被稱作可見操作依賴關系圖的處理機制，可見關系依賴圖記作G。詳細的描述如下，令M ＝（S，s0，T，R）為一個并發程序的模型。可見操作依賴關系圖G ＝＜V，E ＞為模型M 中的有向圖，它包含了遍歷狀態空間中所有可見操作之間的發生前關系。對于G 中的每一個節點v∈V 是一個可見操作，即v∈V：-t∈T：tg＝v。對于在動態搜索中執行的每一個遷移序列算法都會在圖中加入一個方向邊（tg，t′g），這樣在第一次動態執行完成之后，算法會首先搜索可見關系依賴圖并執行回溯，進一步提高了狀態空間搜索效率。

圖2的算法設計中，本文采用基于深度優先的搜索方式來對程序的狀態空間進行搜索。本文使用pre（s，t）來表示到達狀態s之前的那個遷移，fid（t）表示該遷移所在的函數表示。PRI 的作用是記錄函數的優先級。S 為待搜索的狀態堆棧，s.enabled 為每一個狀態s 的可執行遷移集合，s.backtrack 為回溯集合表示需要搜索的狀態s 的中斷集合。s.done表示被檢測過的狀態s的中斷集合。s.sleep 表示在狀態s上可以執行但沒有必要執行的遷移的集合。狀態s上s.sleep 的初始值為存在獨立關系的遷移集合，之后算法會對s.sleep 不斷更新，將已經檢索過的遷移加入到s.sleep中，同時在s.enabled 集合中減去s.sleep，這樣做不僅可以減少狀態s 上需要遍歷的遷移數量，更重要的是隨著s.enabled 集合的不斷縮小，在所有遷移都被檢索之后s.enabled ＝，解決了在無限循環中出現的遷移空間的無限增長問題。

圖2 基于多重中斷的偏序化簡算法描述

在圖2第19、24、26、27、37行中，加入對函數優先級的比較，實現高優先級的中斷服務函數可以打低優先級的中斷服務函數和普通函數的執行，可進一步縮減動態執行中的目標程序狀態空間 （如果函數fid（s）優先級高于函數fid（t）優先級，就不再求取狀態s上遷移t的回溯點）。

與傳統的DPOR 算法不同之處在于算法第12行包含了對中斷允許標志位的判斷，如果在開中斷的情況下，算法才會執行回溯集合中的中斷，反之關中斷的情況下，算法不執行該中斷，

函數UPDATEBACKTRACESETS （S，s）作用是動態計算回溯集合，與經典的DPOR 算法相同，其具體描述如圖3所示。

關于DPOR 算法的詳細理論與數學證明參考文獻 ［9］。

1.3.3 對并發錯誤檢測

并發錯誤檢測算法的設計如圖4所示，算法的第2行至第14行是檢測多重中斷程序中變量讀寫時是否存在原子性違背錯誤；第15、16行是檢測程序中高優先級中斷打斷低優先級中斷時，程序是否存在數據競爭的情況。

圖3 回溯算法描述

圖4 多重中斷程序并發錯誤檢測算法描述

1.3.4 共享變量的讀寫機制

前文中已經介紹了針對多重中的DPOR 偏序化簡算法，如圖2算法中第12行，此時控制執行器將控制目標機中執行fid（t）＝q的中斷服務程序，即控制執行器通知中斷發生器觸發fid（t）＝q的中斷服務程序，由于該過程的延時，也無法保證在目標機中的被測試程序的fid（s）中斷服務函數能夠從當前狀態s處執行到既定的后續狀態s′，因此本文在此設計一個阻塞機制來等待新中斷產生的處理延時。

圖5中所描述的共享變量讀寫流程圖也就是表1中插裝函數Instrument ＿obj＿write（＆X）以及Instrument ＿obj＿read（＆X）所完成的功能。

1.4 中斷發生器設計

由于中斷主要是由硬件觸發的，為了觸發目標機上中斷服務程序的運行，本文專門設計一個中斷信號發生器。

1.4.1 中斷發生器硬件設計

設計中斷信號發生器時，通過分析典型的被測程序的分析，為保證其通用性，本文所設計的中斷信號發生器的包含了圖6所示的硬件接口。

圖5 共享變量讀寫機制

圖6 中斷發生器硬件設計方案

1.4.2 中斷觸發機制設計

控制執行器會在圖2算法中第12行處，觸發fid（t）＝q的中斷，從而強制程序進入下一個狀態s′。但被測試程序中不僅僅包含外部中斷服務函數，還有相當數量的內部中斷服務函數例如定時器中斷、計數器中斷。對于外部中斷本文采用了主動的觸發的方式，但是對于內存中斷，無法進行主動觸發。為此在內部中斷的測試中我們采用了等待內部中斷滿足條件自身觸發的方式來執行測試。測試中如果下一個要執行的中斷服務函數fid（t）＝q 恰好是一個內部中斷函數，此時控制執行器同樣會通知中斷發生器，但是由于中斷服務函數類型為內部中斷，中斷發生器無法觸發相關中斷，共享標量的讀寫會被阻塞，直到內部中斷觸發條件滿足并在內部中斷函數執行結束后通知控制執行器，該中斷函數執行結束。

這樣做的好處是可以不用在中斷函數分析器中區分內部中斷和外部中斷 （不同的硬件平臺中斷服務函數的編寫差別很大，如果區分內部中斷和外部中斷必須在中斷分析的時候進行人工干預，無法自動完成分析過程）。當然通過這樣的方法執行動態測試，如果一旦內部中斷的要求滿足條件需要的時鐘周期過多，這樣難免會影響動態測試的執行效率，這里本文通過改變內部中斷的觸發條件來提高執行效率，例如縮短定時器中斷的觸發周期、減少計數中斷的計數長度。

2 實驗搭建與結果分析

2.1 實驗平臺的搭建

測試系統軟硬件平臺見表3。

表3 測試系統軟硬件平臺

由于多重中斷程序在可控制的動態執行過程中，需要系統有很強的實時性，因此本文使用了高速串行接口HSSI負責控制執行器和中斷發生器的通信。考慮到測試平臺的通用性，控制執行器和目標的通信接口選擇了RS232的串行通信界口。接口設計方案如圖7所示。

圖7 多重終端測試工具接口設計

2.2 實驗結果分析

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

表4 實驗結果1

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

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

表5 實驗結果2

3 結束語

本文根據控制系統中多重中斷并發程序的相關特點，針對數據競爭、原子性違背的并發程序驗證工具。該測試工具的核心算法來自于針對多線程程序測試的DPOR 算法，本文根據多線程和多重中斷程序的不同特點對算法進行了修改，最終實現了對于包含多重中斷控制系統并發程序的狀態空間化簡。目前在數據競爭的檢測方面，可以報告出可能存在的數據競爭，但是還無法區分良性的數據競爭還是惡性的數據競爭，最終結果還需要人為判斷。

［1］Hatcli J，Robby，Dwyer M B.Verifying atomicity speci－fications for concurrent object－oriented software using model－checking ［G］.LNCS 2937：Proceedings of the 5th International Conference on Verification，Model Checking and Abstract Interpretation.Berlin：Heidelberg：Springer－Verlag，2004：175－190.

［2］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 （in Chinese）. ［吳學光，文艷軍，王戟，等.多重中斷數據競爭及原子性違背檢測［J］.計算機科學與探索，2011，12 （3）：1086－1093.］

［3］John Regehr，Nathan Cooprider.Interrutp verifition via thread verification ［J］.Electronic Notes in Theoretical Computer Science，2007，174 （9）：139－150.

［4］Wanja Hofer，Daniel Lohmann，Fabian Scheler，et al.Sloth：Threads as interrupts ［C］／／30th IEEE Real－Time Systems Symposium，2009.

［5］Christoph Baumann，Bernhard Beckert，Holger Blasum，et al.Better avionics software reliability by code verification－A glance at code verification methodology in the Verisoft XT project［C］／／In Embedded World Conference，2009.

［6］FU Xiufeng，CHEN Lirong.Frameork for testing multiple interrupts program ［J］.Computer Engineering and Design，2012，33 （2）：617－623 （in Chinese）. ［傅修峰，陳麗容.多重中斷程序測試框架 ［J］.計算機工程與設計，2012，33（2）：617－623.］

［7］Zachary Anderson.A CIL tutorial－using CIL for language extensions and program analysis ［M］.Systems Group Department of Computer Science，2013.

［8］LIANG Zhongxing，LUO Guiming，KUANG Hongbin.On－thefly deadlock detection with partial－order reduction based on CEGAR［J］.Computer Engineering，2009，35 （19）：65－68 （in Chinese）.［梁中興，羅貴明，曠宏斌.基于CEGAR 偏序化簡得并行程序死鎖檢測［J］.計算機工程，2009，35 （19）：65－68.］

［9］Cormac Flanagan，Patrice Godefroid.Dynamic partial－order reduction for model checking software ［C］／／Proceedings of POPL.Long Beach，California，USA：ACM Press，2005：110－121.

［10］Yi Xiaodong，Wang Ji，Yang Xuejun.Stateful dynamic partial－order reduction ［C］／／8th International Conference on Formal Engineering Methods，2008：149－167.

［11］Christel Baier，Katoen Joost－Pieter.Principles of Model Checking ［M］.London：The MIT Press，2008：595－663.