期刊名称：International Journal of Wireless and Microwave Technologies(IJWMT)
印刷版ISSN：2076-1449
电子版ISSN：2076-9539
出版年度：2012
卷号：2
期号：6
页码：66-73
出版社：MECS Publisher
摘要：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.
关键词：Model checking; Web services; BPEL; epistemic logic; multi-agent systems; strategy
