類復制變異和JPF技術的Eclipse模型檢測方法

廖慧芬，詹 芹

LIAO Hui-fen，ZHAN Qin

（九江學院 信息科學與技術學院，九江 330005）

1 JPF工作原理和體系結構

JPF的基本工作原理是從被檢測對象中篩選出少量的狀態等價于原系統，然后交給JVM檢測，再對不符合系統性質的檢測結果，JPF可以用不同的方式顯示錯誤路徑及性質違例。JPF有三種不同的輸出方式：分別是JPF報告系統（Reporting System）、JPF日志和應用輸出。

JPF中的整個設計重點基本是JVM和Search對象，JVM的功能相當于狀態生成器，在執行過程中，首先JVM生成模型檢測使用的程序狀態，同時JVM中的三個重要的方法：Forward（）表示下一個狀態、Backtrack（）存儲回溯棧中的上一個狀態和RestoreState（）存儲一個任意狀態，控制程序狀態；Search的功能相當于是JVM的驅動，篩選出供JVM處理的狀態，告訴JPF虛擬機在狀態空間中是前進還是后退，同時具有性質驗證器的功能。

2 JPF的關鍵技術

在檢測過程中，JAVA程序狀態一般包括三部分，分別是對象的動態變量、類的靜態變量和每個線程的信息。由此可見，JAVA程序的狀態數量一般都是很大，在解決嚴重的狀態爆炸問題方面，JPF使用了啟發式路徑選擇生成器、on-the-fly偏序規約、主機VM執行、狀態抽象、靜態分析、對稱規約和符號執行等一系列的解決方案。

偏序規約（Partial Order Reduction）方法是利用行為的獨立性（Independence）來減少并行系統模型檢測中的狀態空間爆炸問題。因此，在算法中只需要考慮其中的一種狀態而忽略另一種狀態，狀態S通過這種方式可以轉換成比較小的另一個狀態S'，在執行狀態空間遍歷時，只需要選擇合適并具有代表性的狀態集代替全部狀態集，從而達到減少狀態數量。

圖1 系統狀態轉移圖

近年來，在模型檢測中經常用對稱（Symmetry）方法來避免狀態爆炸問題，對稱方法主要是利用了系統中的對稱結構來進行狀態精簡的。在JPF中，把對稱方法和偏序規約技術結合形成對稱規約技術，它的基本思想是，在模型檢測過程中對系統中需要進行性質驗證的狀態形成等價狀態，只需要檢測這些等價狀態中的一個就可以了。假設一個并行系統中，行為集A={xi,yi,zi,ni}，狀態集S={Ni,Ti,Ci}。形成的完整系統狀態轉移如圖1所示。注意到，圖1中存在明顯的對稱關系，使用對稱規約可以得到如圖2所示的新的狀態轉移圖。同時，行為y、z是獨立的，可以使用偏序規約對系統作進一步的狀態精簡，從而得到與原系統等價的狀態較少的狀態空間，如圖3所示。

圖2 對稱規約后的狀態轉移圖圖

圖3 偏序規約后的狀態轉移圖

3 基于JPF的Eclipse模型檢測平臺實現

JPF不僅可以實現對Java程序的模型檢測功能，它還提供了很強的程序擴展功能。本文使用JPF的Eclipse的PDE來進行JPF插件的開發，使用PDE提供工程向導，新建一個Eclipse Plug-in項目。

3.1 分析插件要實現的功能，標識需要進行添加的擴展點

plugin.xml是插件和Eclipse內核的接口，它提供的擴展點非常多，常見的擴展點有透視圖（perspectives）、視圖（views）、編輯器（editors）、首選項（preferencePages）、幫助（toc）和上下文幫助（context）。需要為每個class關聯一個配置文件（后綴為.cjp），通過讀取cjp文件的配置信息，使用JPF來檢測目標class文件。首先在工具欄中設計一個按鈕來啟動插件的配置對話框，用于配置和管理被檢測類的配置文件，然后還需要專門的面板來并顯示檢測的結果。

3.2 根據擴展點的規范來實現這些擴展

新建一個類MyJpfButtonAction，實現接口IWorkbenchWindowActionDelegate，然后在run（）方法中添加實現打開配置對話框的代碼。

然后，需要定義兩個視圖，一個用于管理配置需要驗證的文件，另一個用來顯示驗證的結果。作為view的擴展，它必須繼承ViewPart類，將它們分別命名為OutputView和TopicView。讓他們重載父類的createPartControl（）方法，來設計各自的面板內容。在OutputView中，設計一個列表來顯示線程選擇信息，當用戶點擊某個線程時，在右邊顯示線程檢測的詳細信息，為了實現此功能，讓OutputView類實現JFace的一個視圖UI接口ISelectionChangedListener。

添加一個右鍵菜單項，新建兩個類JavaClass LaunchAction和RunJpfAction，實現接口IObjectActionDelegate。在JavaClassLaunchAction的run（）方法中使用IProject和IFile來為class文件創建配置文件，并初始化配置文件的內容。在RunJpfAction的run（）方法中調用JPF來完成指定文件的檢測工作。

圖4 配置面板

3.3 編輯plugin.xml文件

PDE為插件清單文件plugin.xml提供了專門的插件清單編輯器。PDE中的插件編輯器為多頁編輯器，其中包括概述、依賴項、運行時、擴展、擴展點、編譯、MANIFEST.MF、plugin. xml和build.properties等，可在每個配置頁面中為其定制相關的屬性。為每一個擴展點添加一個＜extension＞節點，然后在子節點中配置擴展點的id、實現類的路徑、名稱、圖標、標簽文字等擴展點屬性。

調用JPF來執行檢測功能，需要設計一個專門的類來完成此項工作。新建一個類VerifyJob，繼承Eclipse的核心類Job，該類包含4個主要屬性：IFile變量來存儲配置文件信息，Config變量來自JPF的配置類，布爾型變量step指示是否單步執行，PrintStream變量用于輸出。根據默認的配置文件和用戶自定義的配置文件，生成JPF的Config對象，然后在VerifyJob的run（）方法中使用Config對象構造一個JPF對象，最后執行JPF的run（）方法。自定義一個監聽器，用于檢測并輸出JPF的檢測結果，然后通過調用JPF的addSearchListener（）和addVMListener（）方法，將該監聽器添加到當前的JPF對象中去。

3.4 插件測試、打包與發布

PDE提供了很方面的測試、調試手段。每添加一次代碼，就可以通過在插件項目上點擊鼠標右鍵，選擇”Run As Eclipse Application”來測試新插件的功能效果。當然，最終的測試，需要將打包發行后的插件安裝到Eclipse中來觀察插件的工作情況。

插件項目在打包時，僅將src源文件對應的編譯文件打成一個jar包。其它文件如xml、圖像文件等都需要手工復制到打包目錄下。可使用Eclipse導出功能，或Ant來打包插件。

Eclipse還可以通過新建一個Update Site項目的方法，將新的插件以網頁的形式發布出去。利用建立Update Site項目向導，最終會形成一個web目錄，該目錄下包含了你要發布的plugins和features文件夾，另外還有一個site.xml文件和一個index.html文件。site.xml中定義了改更新站點可以提供的插件的下載路徑，這樣用戶可以通過Eclipse的UpdateManager來在線安裝插件。

4 實例應用分析

為測試JPF的死鎖檢測功能，首先創建一個存在死鎖問題的Java類Deadlock，該類實現Runnable接口，在mian（）函數中啟動兩個Deadlock對象，并用synchronized控制對象本身的訪問。考慮這樣一種情況：1）線程T1在對象t1上同步，然后調用對象t2的foo方法，允許被搶先執行。2）另一個線程T2開始執行，在對性t2上同步。3）T2獲得t2，繼續執行，企圖獲得t1，調用t1的foo方法。但獲取失敗，因為T1占有t1。于是，T2阻塞，等待T1釋放t1。4）輪到T1繼續執行，T1試圖獲得t2，但不能成功，因為t2已經被T2占有了。至此，T1和T2都被阻塞，程序死鎖。配置JPF，實現死鎖檢測。

在運行Deadlock類后，由于配置了NotDeadlockedProperty屬性，JPF可以很快發現程序中的死鎖問題，并輸出導致死鎖的程序執行路徑。JPF的出現，為Java程序模型檢測注入了新的力量，它在許多方面都得到了實際應用，包括航天軟件的研制、實時系統驗證和網絡協議驗證[等。Eclipse是Java程序員比較常用的一種Java編輯工具，利用JPF在其基礎上開發一款Java模型檢測工具是非常有意義的，可以使得程序員在編寫程序的同時檢測程序代碼的邏輯正確性。

[1]楊明遠,羅貴明.一種大規模并行程序模型的檢測方法[J].計算機工程,2008,34,（13）：72-74.

[2]鐘誠,唐春艷.運用類復制變異和JPF技術生成類間測試用例[J].小型微型計算機系統,2009,30,（8）.