面向Web服務的業務流程執行語言WSBPEL(也稱為BPEL或BPEIAWS,下面簡稱為BPEL)是一種使用Web服務定義和執行業務流程的語言LlJ。由于存在并發、補償處理、死路徑刪除等復雜特征,BPEL流程容易出錯。另外,BPEL流程中可以通過調用的方式使用Web服務的一些有價值的資源;因此需要保證BPEL流程的正確性。測試是發現不正確行為的一種有效方法,使用驗證技術和工具探查不正確行為也是一種有益的方法。目前人們開發了一些不同的驗證技術和工具,常用的驗證技術多是基于被驗證對象模型基礎上的。基于有色Petri網,本文重點討論BPEL流程中(flow)活動建模方法以及死路徑刪除(dcad path-elmination,DPE)的處理方法。