Model-Checking Behavioral Specification of BPEL Applications

被引：42

作者：

Nakajima, Shin ^{[1
,2
]}

机构：

[1] Natl Inst Informat, Tokyo, Japan

[2] Japan Sci & Technol Agcy, SORST, Tokyo, Japan

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2006年 / 151卷 / 02期

关键词：

BPEL; Model-Checking; SPIN; Abstraction; DPE;

D O I：

10.1016/j.entcs.2005.07.038

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：89 / 105

页数：17

共 17 条

[1]

Curbera F., 2003, BUSINESS PROCESS EXE

[2]

Foster H., 2003, P ASE 2003 SEPT

[3]

Fu X, 2004, P 13 INT C WORLD WID, P621, DOI DOI 10.1145/988672.988756

[4]

GRAF S, **DROPPED REF**

[5]

Holzmann G. J, 2004, SPIN MODEL CHECKER

[6]

KOSHKINA M, 2003, CS200311 YORK U

[7]

LEYMANN F, 1999, PRODUCTION WORKFLOW

[8]

Nakajima S., 2003, Transactions of the Information Processing Society of Japan, V44, P942

[9] Verification of web service flows with model-checking techniques [J].

Nakajima, S .

FIRST INTERNATIONAL SYMPOSIUM ON CYBER WORLDS, PROCEEDINGS, 2002, :378-385

[10] On verifying Web service flows [J].

Nakajima, S .

2002 SYMPOSIUM ON APPLICATIONS AND THE INTERNET (SAINT) WORKSHOPS, PROCEEDINGS, 2002, :223-224

← 1 2 →