Web服务组合的形式化验证与可视化方法研究

发布时间：2018-03-18 20:44

本文选题：Web服务组合　切入点：行为建模　出处：《武汉大学》2014年博士论文　论文类型：学位论文

【摘要】：Web服务可用来实现应用程序在互联网上的互操作,它已成为一种极具发展潜力的分布式网络应用集成技术。对组合服务的研究,不仅可以实现行业内服务的有效使用,也可以帮助行业服务拥有者将业务扩大化,提升业务价值。Web服务组合要实现的最终目的是希望能开发出高质量和满足用户需求的服务组合系统。而系统能否满足用户需求,本质上是由实际执行的具体行为所决定的,也就是说,执行行为的正确与否决定了系统能否满足用户需求。本论文从理论研究和实践结合两个方面着手,研究探索了服务组合的形式化建模、验证以及模型驱动的可视化技术。采用基于行为描述语言的建模方法,可以抽象化流程中的服务行为,这些行为是关系着不同的Web服务之间的通信和交互的,对建立的行为模型可以进一步进行相关特性的验证,这对后续组合服务能否正确执行并成功实现用户既定的目标提供了理论依据。在此基础之上进行的模型驱动的行为模型可视化的研究,可以实现让不同知识背景的用户更直观准确的掌握行为模型中复杂的行为交互,以保证后续开发过程的高效性和表达的准确性。本论文的主要工作如下： (1)建立了基于BPEL4WS的形式化服务组合行为模型WSBM,该模型以行为描述语言BDL为基础,给出了BPEL4WS到BDL的转换与建模方法。使用行为描述语言BDL可以建立一个形式化的行为模型,通过对BPEL4WS描述的Web服务组合系统与BDL模型进行分析和比较,能够将服务组合系统中的概念和元素与BDL模型中的概念和元素对应起来。由变换语义学的概念,这样建立起来的形式化服务组合行为模型WSBM继承了BDL的基本语法和语义。 (2)构造出了形式化服务组合行为模型WSBM的模拟执行过程。在构造的过程中,从初始状态出发,通过追踪复合行为表达式的变化,得出WSBM形式化模型在每个状态下的迁移事件集合,并获得他们之间的映射关系,最终得到模型的运行轨迹。并给出了模拟执行模型的语义正确性证明,使用标记迁移系统作为其操作语义,描述了WSBM模型的状态演化过程,构造了一个等价的执行模型来描述行为模型的运行轨迹,对系统进行语义检查。 (3)进行了Web服务组合形式化模型的特性分析验证。由于Web服务的可复用的概率非常高,因此一个组合服务如果在未经过验证以前就发布出去,一旦出现错误,付出的代价将会很大。因此在组合流程发布之前要对其进行验证。可以采用形式化建模与验证的方法,通过模型的语法以及语义规则来表示和建立需求模型及其执行模型,并通过对目标系统的特性分析,最终验证目标系统所能满足的相关特性。本文研究了Web服务组合的验证问题,提出了服务组合匹配性验证方法。该方法能够在服务部署前发现组合逻辑上潜在的行为不匹配性,从而提高了服务组合的健壮性和用户满意度。并且通过一个实际案例验证了本方法的正确性和有效性。 (4)以web服务组合的行为模型驱动的组合行为交互表达的可视化方法。通过形式化建模和验证,系统的相关特性已经得到了保证。然而要让用户通过阅读和理解模型的语法甚至语义规则来了解需求模型仍然是一件困难的事情。一种较好的方法是采用可视化的技术,将模型形象地表达出来,使用户能够直观地认识和理解需求模型。本文通过对具体Web Service实例的形式化模型,转换为对其组合的可视化动画形式。在建立了组合服务行为模型后,首先使用模型转换的方法将行为模型转换成状态机,以作为需求动画的模型。再根据需要选择需求可视化描述的实体集,并选择对应的图形和图片以直观地表达所选择的实体。然后,根据所选择的实体集,利用状态抽取的方法从模型中提取该演示范围内与这些实体对应的状态块,并将每个状态块中的迁移与提供的动作原语进行关联,作为行为的可视化描述。当状态机执行时,驱动动画引擎根据状态块中对应的迁移,调用相关联的动作原语,控制与对象关联的图形运动,从而直观地表现出模型所描述的行为过程。
[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

【参考文献】