Process Modeling And Verification Of Service Oriented Architecture

Service oriented architecture (SOA) is advanced business logic and computing concepts, service oriented development is an important supplement for object oriented development, process oriented development and database oriented development. Service oriented development methodology is being the latest technology solutions, which can express modular idea and promote the distribution of complex information systems functions. In the SOA solution, the establishment of business processes is not only the implemented process of enterprise information strategy, but also the pivotal process to enterprise information systems. Therefore, services composition languages as a starting research point to build a good SOA processes is worth studying.This paper uses a popular service orchestration language BPEL to achieve business process. It achieves top-down service-oriented architecture using the method of composing, orchestrating and coordinating Web services. Although BPEL language have strong expressive skill, the structural complexity of BPEL will make its semantics are not very clear, so in practical application, the accuracy of the BPEL process has placed enormous demands. In order to better understand the BPEL process, we need a formal modeling approach to model its process. This article uses a simple formal approach of process algebra (FSP) to describe the BPEL semantics and make some simple BPEL process mapped to LTS plan.This thesis makes the problem of concurrent processes sharing resources as a specific object of study, and the problem is modeled by BPEL process. Then, a model checking tool SPIN, which suit to parallel system and analysis of protocol conformance, complete the form model verification. Meanwhile, the paper realized conversion of BPEL processes to model checking input language Promela, and successful achieve verification; the same time, this thesis designs out Kripke structure and LTL model for the protocol of concurrent processes sharing resources. Separately,making Kripke structure mapped to Promela language in the model checking SPIN,and making LTL formula embedded into Promela language for achieving verification.Therefore,the paper discussed the orchestration can be simulated and verificated.Finally, this article summarizes the work done and the recommendations of follow-up work are given.