Epistemic Model Checking Approach for Web Service Compositions
Fengchai Wang · Journal of Chinese Computer Systems · 2011
Due to the dynamics of Web services and their coordination,the openness and variability of Internet,and the loosely coupled developing approach of Web services,the development and execution process of Web service compositions become uncertain,which imperils the trustworthy properties,such as correctness and reliability and so on.In this paper,to realize automatic modeling for Web service compositions,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 loan approval service via MCWS.The experimental results show the validity of MCWS.