A Formal Method Support for Resource Modeling of Web Services Composition

Business process modeling is the key operation of Web services composition, and it is a new method for business process modeling by using communicating sequential process (CSP), current research only focuses on the functional requirements of Web services composition, but it ignores the non-functional requirements, although Timed CSP (TCSP) can analyze timing attributes of Web services composition, but it is not support for analyzing other non-functional attributes, especially resource consumption which web services composition focus on widely. Priced timed CSP (PTCSP) can solve this problem efficiently, which is extended price information on TCSP. Firstly, this paper gives the basic definition and semantics of PTCSP. Then a minimum-cost reachability algorithm is given to estimate the reachability of PTCSP and figures out the minimum cost. Finally, this paper gives an instance to explain how to apply PTCSP on business process resource modeling of Web services composition.