用動作時序邏輯（TLA）進(jìn)行Web服務(wù)描述和合成的研究.pdf

1、近年來,以Web服務(wù)為基礎(chǔ)的面向服務(wù)的體系結(jié)構(gòu)的迅速發(fā)展,為互聯(lián)網(wǎng)應(yīng)用提供了一種共享數(shù)據(jù)的有效手段。Web服務(wù)組合為企業(yè)業(yè)務(wù)應(yīng)用提供了極大的靈活性。然而,Web服務(wù)組合技術(shù)的研究剛剛起步,如何有效地解決Web服務(wù)在異構(gòu)應(yīng)用之間、松散耦合環(huán)境下的互操作、集成和協(xié)作等問題,就成為國內(nèi)外軟件技術(shù)研究的重要方向。 目前國內(nèi)外針對Web服務(wù)組合,已經(jīng)提出了很多Web服務(wù)的描述語言及組合方法。這些語言從不同方面對Web服務(wù)進(jìn)行建模和規(guī)范,但

2、在Web服務(wù)的行為表示上,仍缺乏一個清晰的語義和概念化的模型。本文分析了服務(wù)組合的相關(guān)解決方案,比較了它們滿足服務(wù)組合正確性、安全性、自動組合等需求的情況。針對這些方法在滿足組合需求問題上的不足,本文引入了一種基于模型檢驗機制的動作時序邏輯(Temporal Logic of Action,簡稱TLA)對Web服務(wù)的描述和組合問題進(jìn)行研究。 本文基于有限狀態(tài)自動機(Finite State Automata,簡稱FSA)理論,將

3、Web服務(wù)建模成一個有限狀態(tài)自動機,首先針對WSDL在服務(wù)行為描述方面的缺陷對WSDL進(jìn)行擴展,并提出了從擴展的WSDL語言到TLA語言的轉(zhuǎn)換算法,從而用TLA對服務(wù)的行為進(jìn)行形式化的描述和規(guī)范,為描述Web服務(wù)提供了一個新的方法和途徑。然后,本文討論了在動作時序邏輯中,服務(wù)組合時各組件服務(wù)的有限狀態(tài)自動機的組合方式,以及伴隨著服務(wù)組合,單個服務(wù)的TLA規(guī)范如何組合以形成復(fù)合服務(wù)的TLA規(guī)范的問題,并在此基礎(chǔ)上,提出了實現(xiàn)TLA規(guī)范正確