Research On Modeling&Model Checking&Testing Of Web Services Based On Timed Colored Petri Nets

Web service is a kind of application which is self-contained, self-description andmodularization. It got various advantages from Distributed Computing, Grid Compute,XML and other technologies. It has solved some problems on heterogeneous distributedcompute, code and data reuse. It is interoperation, independent of platforms, and looselycoupled. It has played an important role in a variety of domains including electricbusiness and enterprise application integration. Especially, Web service compositiontechnology has got great focus in academia and industry over the world, due to itsimplementation of service reusing and service increment.Web service composition is a task prone to errors, because its candidate servicestake complex interactions within it. Web Service Business Process Execution Language(WS-BPEL, BPEL) implements the composition and integration of web services. BPELbuilds on IBM’s WSFL and Microsoft’s XLANG and combines the features of bothlanguages, which lead to some inconsistencies and semantic ambiguities. Like mostlanguages, the semantics of BPEL is defined in English prose. Although oftenmasterpieces of apparent clarity, such descriptions usually suffer from inconsistency,ambiguity and incompleteness. The WSBPEL TC recognized the need for a formalismto define the semantics of BPEL.With complex features, such as compensation, correlation,DPE(Dead-Path-Elimination，DPE) and concurrence, Process coded in BPEL is errorprone.The main research work of this thesis is modeling, verification, and test Webservice composition process coded in BPEL.Some approaches have applied to BPEL process model, such as Petri nets, SPINtool, process algebras, abstract state machines and automata, et al. This theise presentsan approach to model Web services composition based on transformation from BPEL toTimed colored Petri net (TCP-net). Each BPEL’s activity is modeled using a TCP-net.A BPEL process is regard as an activity which embedded some activities hierarchically.This hierarchical relation is mapped into TCP-net’s hierarchy.The normal Petri net was applied to model BPEL process in some literatures. Theexperience shows the model is usually on a large scale and result in state explosion.Modeling BPEL process by hierarchical TCP-net can relieve some problems on scaleand state explosion. An algorithm to unfold a hierarchical CP-net into equivalence un-hierarchicalCP-net is presented in this thesis. Any hierarchical CP-net has an equivalenceun-hierarchical CP-net with respect to their behaviors. But the equivalenceun-hierarchical CP-net exposes more details of the model. Also, the formal definition ofhierarchical CP-net proposed by K. Jensen is improved in this thesis..The formal verification of Web services came into research field in recent years,but it has obtained great attention. An approach is proposed in this thesis for modelchecking. The BPEL’s basic properties are verified by checking corresponding CP-net’sbasic properties. Dynamic properties are represented in a CTL-like temporal logic calledASK-CTL. The logic is an extension of CTL which is branch time logic. Such thedynamic properties are verified in this form. In order to solve the state space explosion,predicate abstract and lazy abstract are discussed in this thesis. The CP-nets state spacegeneration and the predicate abstract of the state space are integrated together. Duringthe state space generation, a reduced state space by predicate abstract are calculatedavoiding state space explosion. Lazy abstract applied to CEGAR approach to verifysafety property of BPEL process, which the first two steps of“abstract-verify-counterexample” optimized. This approach can be applied to large scaleprogram.Web services provide loose coupled models with flexibility and usability fordistributed compute. BPEL is a self-formal language with complex features and errorprone. Before a Web service released, verification and testing is require to confirm itsconsistence to the design model. The concept of execute program units is introduced forCP-nets models. Based on execute program units, a new test case generation method isgiven, in which concurrence and DPE features considered properly, as well as otherfeatures.