Business Process modeling and verification is one of the main functions for all the workflow products. In order to detect the deadlock, the lack of synchronization and other issues in process modeling, the majority of workflow products needed to provide analysis and modeling functions based on formal methods. As the WS-BPEL (Web Services Business Process Execution Language) is a kind of non-formal language to describe business processes, testing and verification is not easy. What's more, there is no corresponding formal supporting tool, which makes it difficult to guarantee the correctness of Web services and to track the business processes in more abstract level. For this problem, this paper brought forward the three-tier architecture of business process modeling and verification, and realized the conversion algorithm of business processes to the π-calculus description.
展开▼
