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

1、近年來(lái),以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é)作等問(wèn)題,就成為國(guó)內(nèi)外軟件技術(shù)研究的重要方向。 目前國(guó)內(nèi)外針對(duì)Web服務(wù)組合,已經(jīng)提出了很多Web服務(wù)的描述語(yǔ)言及組合方法。這些語(yǔ)言從不同方面對(duì)Web服務(wù)進(jìn)行建模和規(guī)范,但

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

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