基于形式化規約的缺陷規則庫構建與檢測方法

佟超，王建新，齊建東

北京林業大學信息學院，北京100083

1 引言

程序缺陷分析是軟件質量保證的重要組成部分，它能夠在程序交付測試之前檢測出影響系統及其運行環境的一般缺陷、惡意代碼及后門程序，能發現編譯器不能捕獲的錯誤，很大程度上降低了程序的出錯率。但隨著軟件系統日趨復雜，一般缺陷分析方法已不能滿足用戶日益增長的需求，其中有兩方面的需求尤為突出。首先，一般缺陷分析方法都將缺陷規則內置在缺陷分析工具之中，用戶只能選擇工具已有的缺陷，不能自行定義缺陷規則；其次，傳統缺陷分析方法一般只指出了缺陷發生的最終位置[1]，無法確定實際缺陷與模式缺陷之間的詳細對應情況，開發人員仍需手動調試以確定導致缺陷的路徑，不能很好地幫助其對錯誤進行快速排查和修正。

本文結合形式化規約及模型檢測中的反例輸出技術提出了一種缺陷規則庫構建與源碼檢測方法。利用形式化規約中的模型規約對程序進行建模，用性質規約抽象化待檢測缺陷，即從一般控制流結構中提取出適用于缺陷分析的通用原子命題，結合分支時序邏輯CTL的量詞集合，構建缺陷規則庫元數據。用戶可按照分支時序邏輯CTL的語法規則選取原子命題構建積木式靜態缺陷集。規則庫引擎從缺陷集中拆分出元數據以設計表示靜態缺陷的CTL判定公式，形成相關原子命題，從源程序中抽取控制流信息并激活相關原子命題的標記模塊，并將控制流信息轉換為模型檢測可接受的K ripke結構。最后，結合NuSMV模型驗證器對轉換所得的有限狀態系統進行檢測，若存在某種缺陷，則返回帶有源程序行信息的反例路徑。

2 缺陷規則庫整體框架

作為一種形式化的自動驗證方法，模型檢測將“一個有限狀態系統是否滿足某種規范”抽象為“一個結構是否滿足某個命題邏輯公式”，若不滿足則返回導致該錯誤的反例[2]。其一般過程分為三步：對系統進行建模；對規約進行時態邏輯描述；利用模型檢測工具結合以上兩步實現驗證。模型檢測需要對有限狀態系統進行狀態檢索，經過對各類程序分析方法的研究[3]，本文采用程序控制流分析手段，展開基于形式化規約的缺陷規則庫構建。

圖1給出了規則庫模型的整體框架，從功能角度可將其流程概括為三個步驟，每個步驟涉及到框架中模塊間的通信和交互：

步驟1 用戶通過元數據自定義所需分析的缺陷規則，加入規則庫。

步驟2 導入待檢測程序，由規則庫引擎抽取其控制流結構，同時從規則集中取得待分析缺陷，經過命題動態匹配和模型轉換兩個模塊實現程序建模以及規則集中缺陷的實例化，得到模型驗證器可接受的有限狀態系統。

步驟3 通過NuSMV模型驗證器對有限狀態系統進行檢驗，通過檢測結果轉換與輸出模塊返回檢測結果及導致缺陷的反例路徑。

圖1 整體框架圖

步驟1與步驟2是本文的重點。其中，用戶通過自定義缺陷規則形成缺陷規則集，該功能的實現采用了積木式設計模式，并設計了相應的匹配機制和邏輯描述形式，使缺陷的抽象化更為靈活。規則庫引擎負責元數據匹配機制的動態喚醒和程序與實際缺陷的關系建模，同時完成了模型結構的轉換。

3 積木式缺陷規則庫模型

缺陷規則庫模型的構建基礎是對單一缺陷規則的抽象化描述。本文采用時態邏輯描述系統所要滿足的規范，在此基礎上對缺陷的行為邏輯進行分析，取得構成規則集的通用原子命題集和邏輯量詞集，為規則庫的積木式構建準備元數據。

3.1 缺陷的行為抽象

時態邏輯是一種包含有時間概念的邏輯，是在命題邏輯的基礎上加入了時態算子而形成的邏輯，其基本組成元素為：原子命題、邏輯連接詞、時態連接詞[4]。CTL即分支時序邏輯，是一種典型的時態邏輯，缺陷規則庫的構建需要用戶理解缺陷抽象為CTL公式的過程以實現缺陷自定義，通過分析M itre通用缺陷列表[5]（Common Weakness Enumeration，CWE），不難發現程序缺陷產生的原因與人為因素、編程語言以及缺陷本身都具備一定關聯，即缺陷的產生與缺陷本身具備一定的規律性，對靜態缺陷而言，該特點在缺陷的語法及語義特征上尤為明顯。根據該特征與CTL分支時序邏輯的相似性，同時考慮到缺陷間不可提取的非共性因素，本文定義了靜態缺陷的一般缺陷模式，使針對缺陷的CTL抽象過程更為清晰，同時為構造規則庫的元數據集提供研究基礎。

3.1.1 靜態缺陷的一般缺陷模式

通過對靜態缺陷語法及語義特征的分析，本文將靜態缺陷的一般缺陷模式定義如下：

定義1 基于語法及語義的靜態缺陷模式是一個三元組，M=(S，T，C)，其中S表示一個或多個狀態，T表示由狀態和狀態存在性構成的事件，C表示事件發生的范圍。

定義2 狀態存在性包括：不存在、存在、狀態組合邏輯（例如狀態間的與或關系）下的存在性。

定義3 缺陷有關事件發生的范圍可劃分為：全局范圍，在某事件之前，在某事件之后，在事件A與事件B之間，直到發生某事件。

以Java語言中的空指針異常為例，其缺陷的語義描述為“對一個不存在的對象調用其屬性或方法而導致的異常”，從該描述中可以提取出缺陷模式的基本表示S={s1，s2}，s1表示對象值為null，s2表示調用對象的屬性或方法；T={t1，t2}，t1表示“存在”s1，t2表示“存在”s2；C表示事件t1出現在事件t2之前。

3.1.2 缺陷模式與CTL

作為一種非線性的時態邏輯，CTL在命題邏輯的基礎上加入了時態算子，同時解決了線性時序邏輯中對所有路徑做全程量詞的限制。CTL的組成元素包括：原子命題、邏輯連接詞、時態連接詞及路徑量詞，其巴克斯范式如下：

其中，F指某個未來狀態，X表示下一個狀態，G指所有未來狀態，U指直到，A指所有路徑，E指存在一條路徑；?則指某個原子命題，它是CTL的基本單位[6]。舉例說明CTL的用法：以started表示開始狀態，ready表示就緒狀態。則語句“存在一個某未來狀態，使得開始狀態成立且就緒狀態不成立”的CTL描述為：

從CTL的基本描述可以分析得出其與缺陷模式M的對應關系：S映射為原子命題?，T映射為S與邏輯連接詞的組合關系，C映射為T與時態連接詞和路徑量詞的組合關系。根據這一對應關系結合CTL的邏輯規則，即可實現缺陷模式的CTL抽象[7]。以靜態缺陷分析中的文件輸入流關閉異常和空指針異常為例，本文通過以下兩步來抽象化缺陷。

步驟1 根據缺陷含義分析缺陷模式，獲取相關原子命題。兩種缺陷的具體含義為：

（1）文件輸入流關閉異常，指在開啟了輸入流后，沒有對其進行關閉而導致的異常。

（2）空指針異常，指對一個不存在的對象（其指針為null）調用其屬性或方法而導致的異常。

與以上兩種缺陷相關的原子命題，如表1所示。

表1 缺陷及相關原子命題表示

步驟2 根據缺陷模式，確定所要采用的邏輯連接詞、時態連接詞以及路徑量詞，得到最終的CTL公式表示形式如下所示。

文件輸入流關閉異常：

AG(malloc_fin_s→AF free_fin_s)

該公式的含義：對于任意路徑下的所有狀態，若某一狀態開啟了文件輸入流s，則任意路徑的所有未來狀態會存在針對s的文件流關閉操作。

空指針異常：

AG(assign_null_s→!(EFinvoked_s))

該公式的含義：對于任意路徑下的所有狀態，若某一狀態將對象s賦值為null，則不存在未來狀態中會調用s的屬性或方法的路徑。

以上兩個步驟可以成功地抽象出缺陷的規則化描述，并能分析出與該規則有關的原子命題和邏輯量詞。通過分析缺陷的一般模式，發現大部分原子命題都存在一定的復用性，若在分析過程中進行統一管理與匹配，將顯著提高靜態缺陷分析的可擴展性，這一發現正是積木式規則庫構建的出發點，也是規則庫中元數據集的原型。

3.2 積木式構建模式

規則庫中會內置缺陷規則的元數據，因為程序分析系統會涉及到大量的實時事件分析，若采用傳統的狀態機模式處理，會將元數據的事件關聯全部寫入基本處理邏輯之中，使得程序臃腫不堪，同時嚴重影響到規則庫引擎的響應與處理速度。因此，本文采取積木式構建模式改進這種不足。

積木式構建模式將事件分層，通過簡單事件來搭建復雜事件。其特點是通過有限種基本事件模型和有限種組合形式，構造復雜的事件。這使得在處理事件的過程中不用考慮事件間復雜的因果關系，符合人們處理事務時由簡單到復雜的行為習慣，使事件的處理更為清晰，更專注于事件的關聯與匹配。本文利用積木式構建模式的優點，將與規則有關的所有原子命題和邏輯量詞作為底層元數據，通過積木式方法由用戶自定義缺陷規則并加入到缺陷規則集中，供規則庫引擎調用。

以3.1節中的兩種靜態缺陷為例，其構成的簡易積木式規則庫模型如圖2所示，其中原子命題集、邏輯量詞集、缺陷規則集均以XM L形式描述。原子命題集存儲了表1中與缺陷有關的所有原子命題，邏輯量詞集存儲了缺陷有關的所有邏輯量詞，缺陷規則集中存儲了CTL形式的由以上兩種元素組成的缺陷規則。與此同時，在規則庫引擎中會設計原子命題的匹配模塊，實現原子命題的動態匹配。

圖2 積木式缺陷規則庫模型示例圖

需要注意的是，與規則集有關的原子命題是原子命題集的一部分，前者由用戶輸入，后者由系統內置。

規則庫引擎中的原子命題動態匹配模塊也是積木式模式中的重要組成部分，將在后文中詳述。

4 規則庫引擎

規則庫引擎是缺陷規則庫的核心部分，其功能是將導入的待分析程序建模為K ripke結構的有限狀態系統，在有限狀態系統上動態匹配并標記與規則集關聯的原子命題集，再將其轉換為模型驗證器可接受的數據結構。

4.1 控制流結構抽取與分析

該步驟關聯框架中的控制流結構抽取模塊和命題動態匹配模塊。規則庫引擎中源程序的目標模型是一種有限狀態系統，有限狀態系統的機制是通過狀態變量、輸入變量和常量來描述不同狀態下的不同變量；通過轉換關系來描述一個輸入如何導致系統從一個狀態轉換至多個狀態；通過條件來描述對系統各可用路徑的限制，它符合K ripke結構。

4.1.1 控制流結構與K ripke結構

設計控制流結構抽取模塊的原因在于源程序控制流結構與K ripke結構的相似性。程序的控制流圖可以用來表示程序的控制流信息，它是一個程序所有可能執行路徑的抽象表示，基本元素是節點和有向邊，其中節點代表的是無跳轉的代碼塊，有向邊是各代碼塊之間的跳轉關系，其數據結構為：

其中，V表示節點有限集，vs表示起始節點，vf表示終結節點，A代表節點間的有向邊集合。而K ripke結構是添加了原子命題（AP）概念的有限自動機的變種[8]，其結構如下：

其中，S是有限狀態集；I是初始狀態集，I?S；R是表示狀態間轉換的二元關系，R?S×S；L是標記方法，L:S→2AP，圖3是一個簡單的K ripke結構范例。

該K ripke結構可描述為：

由此可見，將源程序轉換為K ripke結構只需經過兩個步驟，首先是從源程序抽取出控制流結構，然后通過遍歷控制流節點，對原子命題集中的原子命題進行動態匹配，若某個節點滿足某一命題，則在該節點標記該命題為真。

4.1.2 利用Soot抽取及分析控制流結構

直接通過字節碼取得控制流會遇到表達式指令不夠清晰，表達式樹構造過于復雜[9]等情況，本文以Java程序分析為例，選擇Soot代替手工分析字節碼來抽取和分析控制流。Soot是開源的Java字節碼分析與轉換工具[10]，既可以作為單獨的類優化與檢查工具來使用，也可以作為Java字節碼的優化與轉換框架，其最新版本可支持嵌入集成開發環境，使得程序的分析更為易用和高效。本文在獲得控制流結構的同時還需對控制流節點進行分析，因此需要觸及到Soot的表現形式并深入到類結構。

首先，要抽取出控制流結構，需要認識Soot的中間表示——IR。Soot提供了四種用于代碼分析的中間表現形式，它們分別是：Baf、Grimp、Jimple、Shim ple[11]。每種IR都針對不同的分析做了不同程度的抽象，其中，Jimple是Soot的最主要IR，也是本文抽取和分析控制流信息時的主要操作對象。

由于待分析程序結構的多樣化，控制流的抽取也需針對不同場景[12]，Soot構建了五種場景結構：Scene、SootClass、SootM ethod、SootField及Body，分別表示待檢測程序本身、某個待檢測類、類中的某個方法、類中的某個成員、函數體。Body與不同的IR相對應，本文分析采用了Jimple作為IR，故使用Jim pleBody作為方法的主要載體，以方法為單位，抽取程序的控制流信息。

目前人們多通過Soot的命令行工具和Eclipse插件來查看程序的控制流結構[13]，這不利于在抽取過程中對控制流節點進行分析，因此本文采用了繼承Soot的Transformer類并重寫其InternalTransform方法來解決該問題，流程如下：

（1）根據取得的JmpleBody，通過getMethod方式取得method。

（2）以Body為參數，通過BriefUnitGraph構建Unit-Graph，得到控制流圖的基本結構。

（3）遍歷UnitGraph，對每個節點使用getSuccsof遍歷分支節點。

由此即可實現控制流結構的抽取及遍歷，為下一步原子命題的動態匹配提供基礎。

4.2 動態匹配原子命題

原子命題的動態匹配是控制流結構轉換的輔助模塊，它是在遍歷程序控制流節點的過程中，對與規則集相關的原子命題按照一定的匹配規則進行動態匹配。下面將從匹配規則和動態匹配機制兩方面介紹該模塊。

4.2.1 原子命題匹配規則

圖3 K ripke結構

本文詳細分析了Jimple之后，發現可以通過Jim ple的聲明（Statement）實現原子命題的匹配，因為Jimple是類型化的基于聲明的IR，與Java字節碼中約200個指令數相比，Jimple只需掌握15種Statement就能更加方便、標準地描述程序。在遍歷控制流節點過程中，針對每個節點，取得其Statement類型，以此為基礎取得命題匹配條件以及標記命題所需的其他參數，完成原子命題的匹配。

對不同的原子命題而言，其匹配條件也各有不同，前文已經提到，完善功能的系統中會內置與一般缺陷或某一類缺陷有關的所有原子命題，構成原子命題集。因此，需要為原子命題集中的每種命題定義匹配規則。以圖2中的原子命題集為例，其對應的匹配條件如表2。

表2 原子命題的Jim ple匹配條件

文中，原子命題的匹配與缺陷類型是分開的，在原子命題集體積較小時，原子命題的匹配機制并不會對規則庫引擎的處理速度造成很大影響，但隨著原子命題集涵蓋范圍逐漸變廣，則需要定義更為高效的動態匹配機制。

4.2.2 改進的原子命題匹配機制

常見的元素匹配機制是通過分支判定語句if-else進行逐層比對，直至進入判定結果為真的分支，該做法存在三方面的隱患：

（1）當待判定元素過多時，將會相應產生更多的判定語句，這可能會導致某些元素要經過很長的時間才能進入其判定分支，影響處理速度。

（2）若判定分支中的處理語句過于復雜，當判定元素過多時，會造成判定程序體積過大。

（3）判定程序與各原子命題的匹配方法耦合性過高，無法有效地管理每種元素的判定規則。

為解決該匹配機制造成的隱患，本文結合IOC思想設計了一種新的匹配方式，基于接口依賴注入的原子命題動態匹配機制。

IOC即控制反轉，其中心思想是通過面向對象法則來解耦程序，也稱依賴注入[14]，它通過外部實體調控系統內所有對象，在對象創建時返回該對象所依賴的引用。本文實現該機制的方法與規則庫的積木式模式相輔相成，為規則庫原子命題集中的每個原子命題定義匹配對象APmodelImp，且所有對象都實現通用接口Base-APmodel及其方法checkAP（），作為對應的原子命題匹配方法。在主程序中只需遍歷原子命題集，根據命題集中的匹配對象名反射出對象的引用，賦值給通用接口，由通用接口調用匹配方法，具體實現見程序1。

程序1原子命題動態標記算法偽代碼

輸入：程序控制流信息，原子命題集

輸出：標記原子命題的控制流

Begin

for控制流節點node do

for原子命題集元素ap do

根據ap的名稱反射出ap對應的匹配類APModelImp；

將APModelImp實例化所得引用賦給BaseAPModel；

i

f BaseAPModel.checkAP（）為真then

創建原子命題標記對象APObject；

關聯node與APObject；

將APObject加入標記對象集合APLlist；

end if

end for

end for

end

4.3 模型轉換

規則庫引擎中模型轉換模塊的最終目標，是將前兩個功能模塊所得的K ripke結構轉換為NuSMV模型驗證器所接受的SMV語言[15]的同時保留程序的控制流節點信息及行信息，構造缺陷集中各缺陷的實例，實現對缺陷和缺陷檢測結果的管理。

由此可見，該模塊首先要定義符合規則庫模型的SMV語言結構，同時需要設計大量數據結構與相應的轉換算法。

規則庫引擎將本文分析缺陷所需的SMV結構定義為以下四部分，以缺陷實例的構造為入口，設計了對應的數據結構，見表3。這四部分的構造方式如下：

（1）遍歷輸出NodeLink中的所有控制流節點S；

表3 數據結構

（2）取NodeLink頭節點作為初始節點I，遍歷并輸出NodeLink中每個節點的后繼節點，得到狀態轉換關系R；

（3）遍歷APList得到原子命題集合L；

（4）遍歷BugList，取出每個BugObject中的AssertionString，獲得CTL形式的斷言集合A。

以上數據結構均通過在動態匹配模塊中遍歷控制流節點，分析元數據中的原子命題集與規則集實現其構造。

5 原型系統與實驗結果

依據圖2中的積木式規則庫模型，實現了原型系統以驗證本文提出的構造方法的可行性與有效性。首先是規則集的構建，如圖4，用戶根據元數據來自定義缺陷，同時指定缺陷名稱，加入規則集，圖中三個列表分別代表從XM L文件轉換而來的原子命題集、邏輯量詞集和缺陷規則集。列表頂部為編輯區域，用于規則的添加和更新。缺陷規則列表中顯示了規則名稱和規則的邏輯公式，可以通過點擊“edit”或“del”按鈕實現規則的編輯和刪除；點擊“添加規則”按鈕，實現規則的添加。

圖4 原型系統-規則庫管理

添加規則成功后，即可進入原型系統的檢測界面，如圖5，左側是被檢測的源程序，首先根據缺陷集和元數據集對源程序進行建模，得到SMV結構的有限狀態系統，建模結果如程序2（由于建模結果較長，只截取其中代表性的部分）。建模結果的VAR標簽下輸出源程序的全部控制流節點，ASSIGN標簽下輸出控制流節點的轉換關系，DEFINE標簽下輸出已標記的原子命題同時指出原子命題標記的控制流節點。

程序2建模結果

MODULE main

VAR

state：{stat0，stat1，…，stat15}；

ASSIGN

圖5 原型系統-輸入流關閉異常的反例路徑

init（state）：=stat0；

next（state）：=case

state=stat0：{stat1}；

state=stat1：{stat2}；

state=stat2：{stat3}；

state=stat3：{stat4，stat6}；

state=stat4：{stat5}；

...

state=stat14：{stat15}；

TRUE：state；

esac；

DEFINE

param_r0：=state in{stat0}；

assign_null_n0：=state in{stat1}；

invoked_r0：=state in{stat2}；

invoked_n0：=state in{stat6}；

malloc_fin_r1：=state in{stat7}；

free_fin_r1：=state in{stat10}；

if_null_r0：=FALSE；

圖5中右側為檢測結果，源程序共檢測出三個缺陷，分別為空指針異常NullException，文件輸入流關閉異常InputException以及入參判空異常Param IfNullException。點擊缺陷條目，在“Counter Example”區域會顯示反例路徑，同時代碼區域會標記反例行信息。反例路徑中的每個節點以按鈕方式顯示，以節點名加行號作為按鈕名稱，通過點擊節點按鈕，可以定位到代碼中該節點對應的行，從而實現反例重現。從反例路徑可以很容易得出導致輸入流未關閉異常的原因：在行12處開啟了輸入流后，跳轉至catch塊繼續執行至結束，因而導致輸入流未關閉。

空指針異常的反例路徑如圖6所示。可以得出導致缺陷的原因是在行5處將變量賦值為null，當args.length小于或等于0時，程序運行到行9，造成空指針異常。

圖6 原型系統-空指針異常的反例路徑

入參判空異常的反例路徑如圖7，其含義是指“因方法入參變量在引用前未進行判空而可能引發的空指針異常”，其CTL公式的表示形式為：

AG(param&EF invoked-＞A[!invoked U if_null])其中原子命題param表示方法的輸入參數，invoked指引用對象的屬性或方法，if_null表示判斷對象是否為空值。該CTL描述的語義是“對任意路徑下的所有狀態，若某一個狀態定義了方法的入參變量且未來存在一個狀態對該變量進行了引用，則直到對變量判空之前不會對該變量進行引用”。由圖7可以得出，方法入參args在第6行引用其length屬性之前沒有進行判空，若傳入的args為空則會導致空指針異常。

圖7 原型系統-入參判空異常的反例路徑

為進一步驗證方法的適用性，以開源軟件JBoss中的部分代碼作為檢測范例。從圖8中可以發現，原型系統檢測出一條空指針異常。導致缺陷的原因是：在行20處將對象response置為null后，在行27調用了其方法，由此引發空指針異常。

圖8 原型系統-JBoss代碼檢測結果

實驗結果表明，可以利用元數據集合中的原子命題將缺陷成功抽象為CTL表示，實現積木式缺陷規則集的構建；待檢測程序經過模型抽取、標記與轉換過后能夠成功檢測出存在的缺陷，實現反例路徑跟蹤。

同時，在分析實驗結果的過程中也發現，與其他基于靜態分析技術的源碼檢測工具類似，本文提出的方法不能處理動態代碼關聯的原子命題，因此不可避免地會出現檢測結果的漏報與誤報。此外，檢測的準確性還依賴于控制流圖的準確構建及狀態到原子命題的映射。可通過使用高效且準確的控制流抽取方法以及清晰的控制流節點的中間表示形式從外部來降低這兩種依賴性帶來的隱患；細化原子命題匹配規則及缺陷的邏輯描述，減少靜態分析方法可控范圍內的漏報與誤報。

6 結束語

從形式化規約的角度出發，構建積木式缺陷規則庫，在研究過程中實現了規則集的自動構建；源程序到有限狀態系統的動態建模；結合規則集和NuSMV模型檢測器進行模型檢查，返回帶有源程序行信息的缺陷路徑，實現原型系統驗證了本文方法的有效性。

在當前的基礎上，仍需進一步研究的問題是：對不同原子命題的匹配規則進行分析，提取共性部分，為存在共性的原子命題制定通用轉換規則，提高匹配效率及匹配準確性；擴充原子命題集，以擴大缺陷檢測的覆蓋率，進一步提升軟件的可用性。

[1]A rtzi S，Kiezun A，Dolby J，et al.Finding bugs in Web applications using dynamic test generation and explicitstate model checking[J].IEEE Transactions on Software Engineering，2010，36（4）：474-494.

[2]Ball T，Levin V，Rajamani S K.A decade of software model checking with SLAM[J].Communications of the ACM，2011，54（7）：68-76.

[3]Yoo J，Jee E，Cha S.Formal modeling and verification of safety-critical software[J].Software，2009，26（3）：42-49.

[4]Choppy C，K lai K，Zidani H.Formal verification of UML state diagrams：a petri net based approach[J].ACM SIGSOFT Software Engineering Notes，2011，36（1）：1-8.

[5]Sl?tten V，K raemer F A，Herrmann P.Towards automatic generation of formal specifications to validate and verify reliable distributed systems：a method exemplified by an industrial case study[J].ACM SIGPLAN Notices，2012，47（3）：147-156.

[6]Cordeiro L，Fischer B，Marques-Silva J.SMT-based bounded model checking for embedded ANSI-C software[J].IEEE Transactions on Software Engineering，2012，38（4）：957-974.

[7]Ljungkrantz O，Akesson K，Fabian M，et al.Formal specification and verification of industrial control logic components[J].IEEE Transactions on Automation Science and Engineering，2010，7（3）：538-548.

[8]Fioravanti F，Pettorossi A，Proietti M，et al.Generalization strategies for the verification of infinite state systems[J].TPLP，2013，13（2）：175-199.

[9]Liu P，Zhang C.Pert：the application-aware tailoring of java object persistence[J].IEEE Transactions on Software Engineering，2012，38（4）：909-922.

[10]FitzRoy-Dale N，Kuz I，Heiser G.Architecture optimisation with currawong[J].ACM SIGCOMM Computer Communication Review，2011，41（1）：115-119.

[11]Zhou C，Frankl P.JDAMA：Java database application mutation analyser[J].Software Testing，Verification and Reliability，2011，21（3）：241-263.

[12]Eichberg M，Sewe A.Encoding the Java virtual machine’s instruction set[J].Electronic Notes in Theoretical Computer Science，2011，264（4）：35-50.

[13]Girard A，Pola G，Tabuada P.Approximately bisimilar symbolic models for incrementally stable switched systems[J].IEEE Transactions on Automatic Control，2010，55（1）：116-126.

[14]Chang C，Lu C.Pattern-based framework for modularized software development and evolution robustness[J].Information and Software Technology，2011，53（4）：307-316.

[15]A rcaini P，Gargantini A，Riccobene E.A model advisor for NuSMV specifications[J].Innovations in Systems and Software Engineering，2011，7（2）：97-107.