Formal Verification for Web Service
Chen Yan · Jisuanji gongcheng · 2010
A Web service composition is modeled as a multi-agent system.The MCTK,a symbolic model checker for temporal logic of knowledge,is used to model a Web service example of loan approval and verify some related temporal epistemic specifications.Within the same experimental environment,the example is also modeled and verified via MCMAS,which is another model checker for temporal logic of knowledge.Experimental results show the presented model checking approach for Web services based on MCTK is more efficient than the approach based on MCMAS.