Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
423197 | Electronic Notes in Theoretical Computer Science | 2006 | 17 Pages |
Abstract
To provide a framework to compose lots of specialised services flexibly, BPEL is proposed to describe Web service flows. Since the Web service flow description is basically a distributed collaboration, writing correct programs in BPEL is not easy. Verifying BPEL program prior to its execution is essential. This paper proposes a method to extract the behavioral specification from a BPEL appliation program and to analyze it by using the SPIN model checker. With the adequate abstraction method and support for DPE, the method can analyze all the four example cases in the BPEL standard document.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics