Formal Modeling And Compatibility Analysis Of Web Service Composition

With the research, development and application of Web Service technology, some scholars start to look for various valid techniques for the validation of web service composition, hence they begin to make use of the formal method to model and analyse web service composition. At present, the domestic and foreign researchers use tools like process alebras, petrinet, spin for formal specification and verification of web service composition program. However, they have certain deficiencies, and fundamentally stay in the stage of exploration and theoretical research.Based on the research into present web service formalization confirmation methods, this paper analyses their characteristics and the deficiencies, probes into the analysis of BPEL4WS specification, which is widely used for web service composition, and develops a modeling rule for transforming BPEL4WS to pi calculus. Through the intensive research into type system, this paper proposes a practical and feasible method for the analysis of web service composition compatibility, based on typed pi calculus.The content of this paper mainly consists of 3 parts:in the first part, we make a study of the modeling BPEL4WS with formal method. We present the grammar and manipulating semantic of expanding the picalculus with sequence operator and make use of the the concurrent communication structure to represent the normative "link" structure of BPEL4WS. Based on the analysis of the Dead-Path-Elimination(DPE) pattern of the BPEL4WS,we propose a method to solve this DPE problem by the use of pi calculus. Thus we systematically complete the mapping from web service compositon language BPEL4WS standard to the expanded pi calculus. The second part makes a study of the type system. We distinguish the input and output ability of the channels, extend the bisimulation relation on types to that channel types, and then give the proof of related property and axioms. We set up the relation between the bisimulation on types and the subtyping, redefine the type contexts, define typing rules for welltyped processes, and finally define a corresponding rule for pi calculus added with type system. In the third part, we use typed pi calculus to model web service composition system descripted by BPEL4WS. Based on typed pi calculus, we propose a algorithm to check the composition compatibility of web service. At last we apply the algorithm to a complete examination of a bank loan approval system and approve that the algorithm is possibility.