| With the rapid development of Internet techniques, Web services are becoming more and more widely used. Web services are self-contained, self-describing modular applications that can be published, located and invoked across the Web. Web services provide the convenience for integrating applications, but as the capability of an individual Web service is limited, it's necessary to create new functionalities by composing existing Web services together to fulfill the practical requirements. Web services composition realizes the full potential of Web services. With the abroad application of Web services, Web services composition has triggered a considerable number of research efforts both in academia and in industry. Web services composition has become an important research.Web services composition is the ability to create a new value-added service by incorporating some existing web services together. Web services composition is usually an error-prone task, and repairing errors at services operation time is usually costly. Web services participated in composition are often with complex operations, and these operations must be invoked according to the precisely defined scheduling rules, so it's necessary to define the choreography rules for the operations. But some existing Web services composition languages only describe how to compose many elementary services into a composite service in syntax, but lack formal semantic, so it is difficult to analyze and verify these models built by these languages. These languages have not provided the techniques for choreographing complex operations either, and are unable to model concurrency and communication, so they are not suitable to define the choreography rules for Web services. Formal model can solve these problems. Creating formal model for Web services composition process can use formal techniques to analyze and verify the services composition process in order to ensure the correctness and reliability of the composition. Formal model also can define services choreography rules. This approach enables designers to test and repair design errors even before actual running of the service, or allow designers to detect erroneous properties and formally verify whether the service process design does have certain desired properties.Colored Petri Nets model (CPN) is a high-level Petri net and a graphical oriented language for design, specification, simulation and verification of systems. CPN is especially suitable for modeling systems where concurrency, synchronization, and communication are key characteristics. The primary reason for the success of CPN is CPN has a graphical representation, a well-defined semantics allowing formal analysis, and supporting software tools such as CPN Tools. A Web service behavior is basically a partially ordered set of operations. Therefore, it is straightforward to model Web services into CPN. In addition, as CPN can model concurrency, synchronization and communication, it can be used to define services choreography rules.Firstly, this paper proposes a CPN-based model for Web services composition, which is capable to specify choreography rules and Web services composition. By creating CPN model for services composition process, designers can use the formal semantic and analysis techniques of CPN to detect and repair the design errors as early as possible at design stage, thus ensure the correctness of the composition. Choreography rules define the invoking rules of WSDL operations and describe the external behaviors. Defining services choreography rules can ensure the services to be invoked correctly and allow the composition involving services with complex operations.Based on the Web services composition model, this paper presents choreography rules derivation algorithm. The basic idea of the derivation algorithm is simplifying the WSCNet service composition model, while preserving its externally observable interaction behavior. Choreography rules derivation algorithm is based on CPN full occurrence graph construction. With the use of this algorithm, choreography rules can be derivated automatically from the CPN-based model for Web services composition, and the choreography rules will be published with its WSDL interface to UDDI registry. The Web services composition is exposed as a new Web service for other users, and other users can use this new service conveniently, which will improve the reuse of the service.Then, this paper gives the translation between BPEL4WS and CPN model. In BPEL4WS, both the Web service composition and the choreography rules are specified as workflows consisting of activities. To represent BPEL4WS using CPN, basically we represent activities with CPN transitions. The control flow relations between activities specified in BPEL4WS are captured by CPN token firing rules. This paper considers the mostly used workflow patterns in BPEL4WS and discuss how to represent them using CPN model.This paper presents the steps of creating Web services composition using the Web services composition model. There are five steps: 1. discover component services and acquire their service descriptions including both WSDL interface and choreography rules; 2. describe the composite Service; 3. construct the Web service composition from CPN to BPEL4WS; 4. derive choreography rules of the composite service; 5. deploy and advertise the composite service.In order to ensure the correctness of the Web services composition model, it's necessary to analyze and verify the model. This paper gives the approach for analyzing and verifying the model, and designs an analysis and verification tools JCPN, which is realized in Java and more convenient than CPN tools. JCPN enables CPN model to be utilized more widely. JCPN can be used to detect deadlocks automatically and has also been applied intensively in the specification, design and analysis of service-oriented distributed systems. This paper designs several examples to test the functionalities of JCPN.Finally, a Web services composition system is implemented, which integrates JCPN, its main capabilities includes: (1) Specification of a service compositions and choreography rules visually using the composition model. (2) Incorporation of a Web service with complex operations into a larger composition. (3) Verification of the correctness of compositions. (4) Automatic generation of the skeleton BPEL4WS code from corresponding composition model. (5) Automatic derivation of service choreography rules from the service composition model. (6) Service discovery and publication involving choreography rules. (7) Loading an existing BPEL4WS files and automatically generates the composition model for automatic verification and visualization.Generally speaking, this paper proposes a CPN-based model for Web services composition, which can specify Web services composition and choreography rules. Using the formal semantic and analysis techniques of CPN can ensure the correctness of the composition. At the same time, choreography rules derivation algorithm is presented, which improves the reuse of new services. JCPN is designed to analyze and verify the composition model, and it is more convenient than CPN tools. Finally, a Web services composition system is realized, which can create Web services composition, detect the design errors, analyze and verify the correctness of compositions and derivate the choreography rules of composite services.As future work, the CPN-based model for Web services composition will be improved, and a services composition language-independent Web services composition model will be considered. |