International Journal of Wireless and Microwave Technologies (IJWMT)
IJWMT Vol. 2, No. 6, 8 Dec. 2012
Cover page and Table of Contents: PDF (size: 204KB)
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
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.