An Epistemic Model Checking Approach to Web Service Compositions

Full Text (PDF, 204KB), PP.66-73

Views: 0 Downloads: 0

Author(s)

Xiangyu Luo 1,* Kun Wang 2 Fengchai Wang 2

1. Huaqiao University Xiamen 361021, China

2. Guilin University of Electronic Technology Guilin 541004, China

* Corresponding author.

DOI: https://doi.org/10.5815/ijwmt.2012.06.10

Received: 17 Aug. 2012 / Revised: 3 Oct. 2012 / Accepted: 6 Nov. 2012 / Published: 8 Dec. 2012

Index Terms

Model checking, Web services, BPEL, epistemic logic, multi-agent systems, strategy

Abstract

Due to the dynamics of Web services, the openness and variability of Internet, and the loosely-coupled developing approach of Web services, the development and execution process of Web service compositions becomes uncertain, which imperils the trustworthy properties. In this paper we abstract Web service compositions as multi-agent systems, propose a formal model BSTS for modeling BPEL, develop and implement two translation algorithms B2S and S2I, to translate BPEL into BSTS and translate BSTS into the input language ISPL of the model checker MCMAS for multi-agent systems, respectively. The proposed method supports not only temporal properties, but also epistemic and cooperation properties, which are supported only in multi-agent systems. We implemented the prototype tool, called MCWS, for the proposed method. We modeled and verified an example of Web service compositions. The experimental results show the validity of MCWS.

Cite This Paper

Xiangyu Luo,Kun Wang,Fengchai Wang,"An Epistemic Model Checking Approach to Web Service Compositions", IJWMT, vol.2, no.6, pp.66-73, 2012. DOI: 10.5815/ijwmt.2012.06.10

Reference

[1]OASIS Standard. Web Services Business Process Execution Language Version 2.0. http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html. 2007.

[2]Franco Raimondi. "Model checking multi-agent systems". Phd, University College London, 2006. pp. 112-127. Alessio Lomuscio, Hongyang Qu, Monika Solanki. " Towards verifying contract regulated service composition". ICWS'08. Beijing. 2008. pp.254-261.

[3]Alessio Lomuscio, Hongyang Qu, Marek sergot, Monika Solanki. "Verifying temporal and epistemic properties of web service composition". Lecture Notes in Computer Science, Vol. 4, Springer, 2007. pp. 456-461.

[4]Raman Kazhamiakin. "Formal analysis of web service composition". Phd, University of Trento. 2007. pp. 48-71.

[5]Andreas Wombacher, Peter Fankhauser, Erich Neuhold. "Transforming BPEL into annotated deterministic finite state automata for service discovery". ICWS'04. California. 2004, pp. 316-323.

[6]S.Nakajima. "Model-Checking Behavioral Specification of BPEL Applications". Electronic Notes in Theoretical Computer Science. 2006. pp. 89-105.

[7]Franck van Breugel and Mariya Koshkina. "Dead-path-elimination in BPEL4WS". ACSD'05. France. 2005. pp. 192-201.