基于TLA的OWL-S Web服務(wù)驗證與組合.pdf

1、隨著以Web服務(wù)為基礎(chǔ)的面向服務(wù)的體系結(jié)構(gòu)的發(fā)展,如何有效的聯(lián)合自治的、分布的、不同功能的Web服務(wù)構(gòu)建新的企業(yè)業(yè)務(wù)應(yīng)用成為新的熱點問題。利用Web服務(wù)組合技術(shù),企業(yè)業(yè)務(wù)應(yīng)用可以獲得極大的靈活性。然而,Web服務(wù)組合技術(shù)的研究剛剛起步,如何使Web服務(wù)真正進(jìn)入實用階段,使之實現(xiàn)跨組織,跨管理域的系統(tǒng)集成和自動交互,還面臨很多問題。有些已經(jīng)解決,另一些則研究尚不充分,比如Web服務(wù)如何組合,能否自動組合,組合的正確性驗證,以及如何利用模型

2、檢測技術(shù)來解決諸如服務(wù)組合狀態(tài)的終止性和可達(dá)性等問題。 針對上述不足,本文引入了一種時序邏輯TLA(Temporal Logic of Actions),用作Web服務(wù)的驗證與組合,主要包括：1)驗證已存在的OWL-S描述的服務(wù)組合流程；2)提出Web服務(wù)的TLA規(guī)范,并利用TLA的一階邏輯特性,實現(xiàn)服務(wù)組合流程的自動生成與驗證。本文首先提出了一種OWL-S流程的TLA模型,并開發(fā)自動轉(zhuǎn)化驗證OWL-S流程的工具,實現(xiàn)服務(wù)組合的