Welcome to the InfoSci Platform
Reference Hub5
A Bounded Model Checking Approach for the Verification of Web Services Composition

A Bounded Model Checking Approach for the Verification of Web Services Composition

Ehtesham Zahoor, Kashif Munir, Olivier Perrin, Claude Godart
Copyright: © 2013 |Volume: 10 |Issue: 4 |Pages: 20
ISSN: 1545-7362|EISSN: 1546-5004|EISBN13: 9781466635524|DOI: 10.4018/ijwsr.2013100103
Cite Article Cite Article

MLA

Zahoor, Ehtesham, et al. "A Bounded Model Checking Approach for the Verification of Web Services Composition." IJWSR vol.10, no.4 2013: pp.62-81. http://doi.org/10.4018/ijwsr.2013100103

APA

Zahoor, E., Munir, K., Perrin, O., & Godart, C. (2013). A Bounded Model Checking Approach for the Verification of Web Services Composition. International Journal of Web Services Research (IJWSR), 10(4), 62-81. http://doi.org/10.4018/ijwsr.2013100103

Chicago

Zahoor, Ehtesham, et al. "A Bounded Model Checking Approach for the Verification of Web Services Composition," International Journal of Web Services Research (IJWSR) 10, no.4: 62-81. http://doi.org/10.4018/ijwsr.2013100103

Export Reference

Mendeley
Favorite Full-Issue Download

Abstract

In this paper, we propose a bounded model-checking based approach for the verification of declarative Web services composition processes using satisfiability solving (SAT). The need for the bounded model-checking approach stems from the nature of declarative processes as they are defined by only specifying the constraints that mark the boundary of the solution to the composition process. The proposed approach relies on using Event Calculus (EC) as the modeling formalism with a sound and complete EC to SAT encoding process. The use of EC as the modeling also formalism allows for a highly expressive approach for both the specification of composition model and for the specification of verification properties. Furthermore, as the conflict clauses returned by the SAT solver can be significantly large for complex processes and verification requirements, we propose a filtering criterion and defined patterns for identifying the clauses of interest for process verification.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.