Web服务的形式化验证  

Formal Verification for Web Service

作　　者：骆翔宇[1] 陈艳[1] 

机构地区：[1]桂林电子科技大学计算机与控制学院,桂林541004

出　　处：《计算机工程》2010年第5期257-259,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(60763004);中国博士后科学基金资助项目(20090450389);广西青年科学基金资助项目(桂科青0728090)

摘　　要：将Web服务组合建模为多智能体系统,采用时态知识逻辑模型检测工具MCTK刻画贷款协议Web服务实例,并验证相关的时态知识规范。在同一实验环境下,采用另一种时态知识逻辑模型检测工具MCMAS进行建模,并验证该实例。实验结果表明,基于MCTK的Web服务模型检测方法比基于MCMAS的方法更有效。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.

关 键 词：模型检测 时态知识逻辑 多智能体系统 WEB服务 

分 类 号：N945[自然科学总论—系统科学]