Mwb The Bpel-based ¦Ð-calculus, Automatic Conversion Tools

As an important means of communication, Web is rapidly developed with the accelerating process of globalization. People are paying more and more attention on the correctness of Web service description. BPEL (Business Process Execution Language), which is a kind of language utilized to describe Web services composition, it can composite, orchestrate and coordinate multiple Web services, and then combine them into a new composite service (which is called a business process). However, as the BPEL is a kind of non-formal language to describe business processes, it can not effectively describe the deadlock between the Web service process, the lack of synchronization and other problems. Therefore, formal methods must be adopted in modeling BPEL process to reduce such problems arising in Web services composition.This paper is based on the commitment of the state "863" key project, and then analyzed and referenced to the theories, research results and technologies ofπ-calculus and BPEL language. Moreover, this paper proposed a complete automatic modeling process from BPEL toπ-calculus expressions. Based on the automatic modeling theory, this paper implemented the automatic modeling and analyzing prototype tool. The main work of this paper is reflected in the following aspects:1. This paper analyzed the theories and methods that modeling BPEL with theπ-calculus, and then explained recently research in the relevant fields and summarized problems encountered in the process of automatic modeling.2. This paper combined the definition of identifiers for MWB (the Mobility WorkBench) and optimized the theory of manually modeling process. And this paper proposed the automatic modeling method from BPEL toπ-calculus expressions which is resolved with DOM (Document Object Model) trees, and made up the automatic modeling process.3. This paper analyzed problems encountered in the automatic modeling process such as data compatibility and structure legalization, and then proposed a method which solved problems through lexical analysis and syntax analysis. 4. Based on the related theory research, this paper designed and implemented the automatic model verification tool BPCT (BPEL to Pi Convert Tool).