Web服務組合的形式化驗證與可視化方法研究
發(fā)布時間:2018-03-18 20:44
本文選題:Web服務組合 切入點:行為建模 出處:《武漢大學》2014年博士論文 論文類型:學位論文
【摘要】:Web服務可用來實現(xiàn)應用程序在互聯(lián)網上的互操作,它已成為一種極具發(fā)展?jié)摿Φ姆植际骄W絡應用集成技術。對組合服務的研究,不僅可以實現(xiàn)行業(yè)內服務的有效使用,也可以幫助行業(yè)服務擁有者將業(yè)務擴大化,提升業(yè)務價值。Web服務組合要實現(xiàn)的最終目的是希望能開發(fā)出高質量和滿足用戶需求的服務組合系統(tǒng)。而系統(tǒng)能否滿足用戶需求,本質上是由實際執(zhí)行的具體行為所決定的,也就是說,執(zhí)行行為的正確與否決定了系統(tǒng)能否滿足用戶需求。 本論文從理論研究和實踐結合兩個方面著手,研究探索了服務組合的形式化建模、驗證以及模型驅動的可視化技術。采用基于行為描述語言的建模方法,可以抽象化流程中的服務行為,這些行為是關系著不同的Web服務之間的通信和交互的,對建立的行為模型可以進一步進行相關特性的驗證,這對后續(xù)組合服務能否正確執(zhí)行并成功實現(xiàn)用戶既定的目標提供了理論依據(jù)。在此基礎之上進行的模型驅動的行為模型可視化的研究,可以實現(xiàn)讓不同知識背景的用戶更直觀準確的掌握行為模型中復雜的行為交互,以保證后續(xù)開發(fā)過程的高效性和表達的準確性。本論文的主要工作如下: (1)建立了基于BPEL4WS的形式化服務組合行為模型WSBM,該模型以行為描述語言BDL為基礎,給出了BPEL4WS到BDL的轉換與建模方法。使用行為描述語言BDL可以建立一個形式化的行為模型,通過對BPEL4WS描述的Web服務組合系統(tǒng)與BDL模型進行分析和比較,能夠將服務組合系統(tǒng)中的概念和元素與BDL模型中的概念和元素對應起來。由變換語義學的概念,這樣建立起來的形式化服務組合行為模型WSBM繼承了BDL的基本語法和語義。 (2)構造出了形式化服務組合行為模型WSBM的模擬執(zhí)行過程。在構造的過程中,從初始狀態(tài)出發(fā),通過追蹤復合行為表達式的變化,得出WSBM形式化模型在每個狀態(tài)下的遷移事件集合,并獲得他們之間的映射關系,最終得到模型的運行軌跡。并給出了模擬執(zhí)行模型的語義正確性證明,使用標記遷移系統(tǒng)作為其操作語義,描述了WSBM模型的狀態(tài)演化過程,構造了一個等價的執(zhí)行模型來描述行為模型的運行軌跡,對系統(tǒng)進行語義檢查。 (3)進行了Web服務組合形式化模型的特性分析驗證。由于Web服務的可復用的概率非常高,因此一個組合服務如果在未經過驗證以前就發(fā)布出去,一旦出現(xiàn)錯誤,付出的代價將會很大。因此在組合流程發(fā)布之前要對其進行驗證?梢圆捎眯问交Ec驗證的方法,通過模型的語法以及語義規(guī)則來表示和建立需求模型及其執(zhí)行模型,并通過對目標系統(tǒng)的特性分析,最終驗證目標系統(tǒng)所能滿足的相關特性。本文研究了Web服務組合的驗證問題,提出了服務組合匹配性驗證方法。該方法能夠在服務部署前發(fā)現(xiàn)組合邏輯上潛在的行為不匹配性,從而提高了服務組合的健壯性和用戶滿意度。并且通過一個實際案例驗證了本方法的正確性和有效性。 (4)以web服務組合的行為模型驅動的組合行為交互表達的可視化方法。 通過形式化建模和驗證,系統(tǒng)的相關特性已經得到了保證。然而要讓用戶通過閱讀和理解模型的語法甚至語義規(guī)則來了解需求模型仍然是一件困難的事情。一種較好的方法是采用可視化的技術,將模型形象地表達出來,使用戶能夠直觀地認識和理解需求模型。本文通過對具體Web Service實例的形式化模型,轉換為對其組合的可視化動畫形式。在建立了組合服務行為模型后,首先使用模型轉換的方法將行為模型轉換成狀態(tài)機,以作為需求動畫的模型。再根據(jù)需要選擇需求可視化描述的實體集,并選擇對應的圖形和圖片以直觀地表達所選擇的實體。然后,根據(jù)所選擇的實體集,利用狀態(tài)抽取的方法從模型中提取該演示范圍內與這些實體對應的狀態(tài)塊,并將每個狀態(tài)塊中的遷移與提供的動作原語進行關聯(lián),作為行為的可視化描述。當狀態(tài)機執(zhí)行時,驅動動畫引擎根據(jù)狀態(tài)塊中對應的遷移,調用相關聯(lián)的動作原語,控制與對象關聯(lián)的圖形運動,從而直觀地表現(xiàn)出模型所描述的行為過程。
[Abstract]:The interoperability of Web services can be used to implement the application on the Internet, it has become a distributed network application integration technology has great potential for development. Research on the combination of services, not only can realize the effective use of the service industry, service industry can also help the owner to expand business, enhance the ultimate purpose of business value of.Web service to implement the combination is to develop high quality and meet the needs of users of the service composition system. The system can meet the needs of users, is essentially determined by the actual implementation of the specific behavior, that is to say, the implementation of the validity of the system can meet the needs of users.
This paper from the two aspects of theoretical research and practice, research the formal modeling of service composition, visualization technology and model driven verification. The behavior modeling method based on language, can the service behavior abstraction process, these behaviors is the relationship between different Web services and interactive communication further, can verify the relevant characteristics of the behavior of the model, the subsequent composite service can correct implementation and successful implementation of user goals provide a theoretical basis for the visualization research of model driven behavior. On the basis of the model, can be achieved for the different background knowledge of users more intuitive and accurate grasp of complex interactive behavior the behavior of the model, in order to ensure the accuracy and efficiency of the subsequent expression of the development process. The main work of this paper is as follows:
(1) established a formal WSBM model service composition based on BPEL4WS, this model takes the behavior description language based on BDL, gives the conversion of BPEL4WS to BDL and the modeling method. Using the behavior description language BDL can establish a behavior model of form, through the analysis and comparison of Web service composition system on BPEL4WS scan the BDL model can be combined service concept and concept elements and element and BDL model in the system. By the corresponding concept transform semantics, formal WSBM model service composition so established inherited the basic syntax and semantics of BDL.
(2) to construct the simulation model of the formal implementation process of WSBM service composition. In the construction process, starting from the initial state, through the change tracking compound behavior expressions, the migration event WSBM formal model in each state set, and obtain the mapping relationship between them, finally get the trajectory model. And gives the semantic correctness of simulation execution model that uses the labeled transition system as its operational semantics, describes the WSBM model of the state evolution process, construct an equivalent execution model to describe the trajectory for the model, the semantic check on the system.
(3) analyzed characteristics of formal model for Web services composition. Because the Web service reuse probability is very high, so a combination of services if not verified before release, once the error occurs, the cost will be great. So in the combination process to verify its release before the method can be used. Modeling and formal verification, and establishes the demand model and the execution model represented by the model of grammar and semantic rules, and the characteristics of the target system analysis, characteristics of the target system can meet the final verification. This paper studies the verification of Web service composition, put forward the matching authentication service the combination method. The method can find the potential behavior of combinational logic does not match the service deployment, thus improving the robustness and service composition and through customer satisfaction. A practical case shows the correctness and effectiveness of this method.
(4) a visualization method driven by the behavior model of web service composition for the interactive expression of combination behavior.
Through the formal modeling and verification, the relevant characteristics of the system have been guaranteed. However, to let the user through the reading and understanding of grammar and semantic rules to model even understand demand model is still a difficult thing. A better method is the use of visualization technology, the model of image expression, allowing users to intuitively to know and understand the demand model. Through the formal model of specific Web Service instance, converted to its combination of visual form of animation. In the combination of service behavior model, model transformation method firstly uses the behavior model into a state machine, as demand animation model. Then according to the demand describe the set of entities, and select the corresponding graphics and pictures to visually express the selected entity. Then, according to the selected set of entities, the use of state selection The method of extraction from the model state block the demonstration range corresponding to these entities, and the migration of each state in the block were associated with the action primitives provided, described as behavior visualization. When the state machine implementation, driven animation engine based on the corresponding state migration in the block, call the relevant action primitives combined. Association control and object motion graphics, which intuitively exhibit behavioral process model described.
【學位授予單位】:武漢大學
【學位級別】:博士
【學位授予年份】:2014
【分類號】:TP393.09
【參考文獻】
相關期刊論文 前6條
1 李喜彤;范玉順;;Web服務過程建模及其邏輯正確性驗證[J];計算機集成制造系統(tǒng);2008年04期
2 郭玉彬;杜玉越;奚建清;;Web服務組合的有色網模型及運算性質[J];計算機學報;2006年07期
3 蔣哲遠;韓江洪;王釗;;動態(tài)的QoS感知Web服務選擇和組合優(yōu)化模型[J];計算機學報;2009年05期
4 楊濤,劉錦德;Web Services技術綜述——一種面向服務的分布式計算模式[J];計算機應用;2004年08期
5 岳昆,王曉玲,周傲英;Web服務核心支撐技術:研究綜述[J];軟件學報;2004年03期
6 陳彥萍;李增智;郭志勝;晉勤學;王創(chuàng);;Web服務組合中基于服務質量的服務選擇算法[J];西安交通大學學報;2006年08期
相關博士學位論文 前1條
1 李磊;面向服務計算的若干關鍵技術研究[D];中國科學技術大學;2008年
,本文編號:1631270
本文鏈接:http://www.sikaile.net/guanlilunwen/ydhl/1631270.html
最近更新
教材專著