Formal Verification in Web Services Composition

被引：0

作者：

Todica, Valeriu ^{[1
]}

Vaida, Mircea-Florin ^{[1
]}

Cremene, Marcel ^{[1
]}

机构：

[1] Tech Univ Cluj Napoca, Baritiu St 26, Cluj Napoca 400027, Romania

来源：

2012 IEEE INTERNATIONAL CONFERENCE ON AUTOMATION, QUALITY AND TESTING, ROBOTICS, THETA 18TH EDITION | 2012年

关键词：

Web Services; Model Checking; Spin;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

The aim of this research is to propose a method for verifying business processes automatically generated through Web services composition. The method is based on model checking and uses Spin model checker, a tool for verifying the correctness of software models. Model checking is a powerful verification technique that can be applied to hardware or software systems in order to validate safety requirements such as the absence of deadlocks. The business process is transformed into a PRONIELA model that is simulated by Spin in order to be verified against the constraint requirements specified. The proposed method is incorporated into a generic and extensible framework for automatic Web services composition and execution.

引用

页码：195 / 200

页数：6

共 15 条

[1]

[Anonymous], 1975, ACM SIGPLAN NOTICES

[2]

[Anonymous], 2004, DAT SYS APP

[3]

Ben-Ari M., 2008, Principles of the Spin Model Checker

[4] The Semantic Web - A new form of Web content that is meaningful to computers will unleash a revolution of new possibilities [J].

Berners-Lee, T ;

Hendler, J ;

Lassila, O .

SCIENTIFIC AMERICAN, 2001, 284 (05) :34-+

[5]

Clarke EM, 1999, MODEL CHECKING, P1

[6] A framework for model checking Web service compositions based on BPEL4WS [J].

Dai, Guilan ;

Bai, Xiaoying ;

Zhao, Chongchong .

ICEBE 2007: IEEE INTERNATIONAL CONFERENCE ON E-BUSINESS ENGINEERING, PROCEEDINGS, 2007, :165-+

[7] Model-based verification of web service compositions [J].

Foster, H ;

Uchitel, S ;

Magee, J ;

Kramer, J .

18TH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2003, :152-161

[8]

Gao CM, 2006, GCC 2005: FIFTH INTERNATIONAL CONFERENCE ON GRID AND COOPERATIVE COMPUTING, PROCEEDINGS, P355

[9]

Hohpe G., 2012, Enterprise Integration Patterns: Designing, Building, and Deploying Messaging Solutions, V15

[10] The model checker SPIN [J].

Holzmann, GJ .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1997, 23 (05) :279-295

← 1 2 →