Ws-bpel Modeling Based On The ¦Ð-calculus And Implementation

Business process design and verification is a major feature of all workflow products. In order to detect deadlock, lack of synchronization and other issues, most workflow products need to provide analysis and modeling functions based on formalization. WS-BPEL (Web Services Business Process Execution Language) describes business process semi-formally, which is hard to detect and verify and is also without support of corresponding formal tools. It causes difficulty in ensuring the accuracy of Web service composition and tracking the business process at an abstract level.The thesis, combined with an 863 project undertaken by the lab, researches on the correctness of business process internal logic and explores a way to model and verify business process described in WS-BPEL using process algebra pi-calculus as a formal tool.1. The thesis puts forward the architecture of BPMV(Business Process Modeling and Verification) architecture, the problem to be solved and the steps to be followed, also analyses the modeling method based on Petri net, automata theory, process algebra.2. The thesis analyzes related research using pi-calculus modeling WS-BPEL at home and abroad, sums up the reason of the pi-calculus suitable for modeling the WS-BPEL, then the paper models the activities of WS-BPEL. On the basis, we present algorithm description for pi-calculus-based modeling of WS-BPEL.3. The thesis analyzes the property, such as deadlock, alivelock, bisimulation, which may exist in business process, deduces the property by pi-calculus and verifies the property by MWB.4. Based on eclipse development environment and SWT plug-in, Design and implement the prototype tool of B2P.