用動作時序邏輯（TLA）進行Web服務描述和合成的研究.pdf

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

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

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