A Verification Approach for Web Service Compositions Based on Epistemic Model Checking
Luo Xiang · Chinese Journal of Computers · 2011
In recent years,the formal verification of Web service compositions is gradually becoming a hot research area.As a mainstream technique for formal verification,model checking is able to not only overcome the shortcoming of traditional software test techniques that they cannot generate the complete set of test cases,but also automatizes the verification process.In this paper,the authors propose and implement an epistemic model checking approach for the verification of Web service compositions by modeling them as multi-agent systems.After analyzing the BPEL control flow,the authors first propose a formal model for the BPEL activities and give the semantics of the implementation of the BPEL activities.By taking the so-call transition seven-tuple as the intermediate form,the authors further develop two automatic transform algorithms,one converts the BPEL process to the set of seven-tuples and the other converts this set of seven-tuples to the input language of MCTK(a model checker for multi-agent systems developed by the authors),such that can finally implement the verification by MCTK.The experimental results show that the proposed algorithms can effectively verify not only the temporal logical specifications,but also the temporal epistemic logical specifications,which are proper to multi-agent systems.