1、如今 Web服務廣泛分布于互聯(lián)網中,它們通過彼此之間的交互實現(xiàn)對問題的協(xié)作求解。然而,在交互過程中,一些非預期、“不正?！钡男畔⒔换r有發(fā)生,嚴重影響了系統(tǒng)的質量及健壯性,有可能使用戶得不到正確結果。因此,模型檢測 Web服務組合的時態(tài)認知性質,保障 Web服務的正確運行就成為了模型檢測領域的熱門研究方向。目前,國內外針對 Web服務組合的形式化驗證正處于起步階段,整個驗證過程的自動化程度很低,各個技術環(huán)節(jié)都需要大量的人工操作。為了提高

2、 Web服務流程驗證的自動化程度,本文提出將Web服務組合的BPEL流程自動轉化為模型檢測工具MCTK輸入代碼的一系列轉換算法。最后利用這些算法在MCTK環(huán)境下對VTA協(xié)議和STS協(xié)議進行了形式化驗證,并自動構建了貸款服務協(xié)議的狀態(tài)轉換圖。取得的研究成果有:
　　(1)針對Web服務描述語言BPEL,給出相關活動語義。引入遷移七元組概念,基于活動語義,建立BPEL活動與能夠反映系統(tǒng)狀態(tài)遷移關系的遷移七元組的一一對應,為實現(xiàn)流程的自

3、動化驗證打下基礎;
　　(2)分別提出將BPEL控制流、數(shù)據(jù)流轉化為遷移七元組集合的轉換算法B2T和F2T。這些算法自動將BPEL流程轉化為遷移七元組集合,實現(xiàn)了將組合業(yè)務流程自動轉化為多分支狀態(tài)轉換圖的功能;
　　(3)提出根據(jù)遷移七元組集合自動生成MCTK代碼的轉換算法T2M。為了實現(xiàn)控制流的全自動檢測,T2M算法根據(jù)遷移七元組集合中各元組的相互關系,結合MCTK語言自身特點,自動生成用來描述流程的MCTK代碼,避免了繁