An Epistemic Model Checking Approach to Web Service Compositions

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.