類復(fù)制變異和JPF技術(shù)的Eclipse模型檢測方法

廖慧芬，詹 芹

LIAO Hui-fen，ZHAN Qin

（九江學(xué)院 信息科學(xué)與技術(shù)學(xué)院，九江 330005）

1 JPF工作原理和體系結(jié)構(gòu)

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

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

2 JPF的關(guān)鍵技術(shù)

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

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

圖1 系統(tǒng)狀態(tài)轉(zhuǎn)移圖

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

圖2 對稱規(guī)約后的狀態(tài)轉(zhuǎn)移圖圖

圖3 偏序規(guī)約后的狀態(tài)轉(zhuǎn)移圖

3 基于JPF的Eclipse模型檢測平臺實現(xiàn)

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

3.1 分析插件要實現(xiàn)的功能，標(biāo)識需要進行添加的擴展點

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

3.2 根據(jù)擴展點的規(guī)范來實現(xiàn)這些擴展

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

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

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

圖4 配置面板

3.3 編輯plugin.xml文件

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

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

3.4 插件測試、打包與發(fā)布

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

插件項目在打包時，僅將src源文件對應(yīng)的編譯文件打成一個jar包。其它文件如xml、圖像文件等都需要手工復(fù)制到打包目錄下?？墒褂肊clipse導(dǎo)出功能，或Ant來打包插件。

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

4 實例應(yīng)用分析

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

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

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

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