Verification of BPEL specifications using model checking

Abstract

Service Oriented Architecture(SOA) is based on creating services which can be distributed on a network by different business flows. Business Process Execution Language (BPEL) is a recent specification language to express web service applications and business flows in an easier way in SOA implementations. In order to verify the correctness of BPEL processes during design, a number of software verification methods can be applied to BPEL specified processes. In this paper, the translation of BPEL process specifications into PROMELA specification language and verification by model checking by SPIN tool are studied. By creating a model of any BPEL process, several verification steps can be applied during design time by the help of SPIN tool. A subset of BPEL activities consisting of assign, switch, sequence, empty, while, terminate, scope, flow, throw, invoke, reply, receive, pick, wait, fault handlers and compensation handlers are modeled to check and verify the processes specified by using these activities. With the tool created in this work, a given set of inputs consisting of BPEL source code(s), wsdl files(s) and BPEL descriptor file(s) are used to create a PROMELA model, then the model is verified by using the SPIN model checking tool for counter claims, assertions and unreachable codes.