| Web服务的形式化验证 |
| |
| 引用本文： | 骆翔宇,陈艳. Web服务的形式化验证[J]. 计算机工程, 2010, 36(5): 257-259 |
| |
| 作者姓名： | 骆翔宇 陈艳 |
| |
| 作者单位： | 桂林电子科技大学计算机与控制学院,桂林,541004 |
| |
| 基金项目： | 国家自然科学基金资助项目(60763004);;中国博士后科学基金资助项目(20090450389);;广西青年科学基金资助项目(桂科青0728090) |
| |
| 摘 要： | 将Web服务组合建模为多智能体系统，采用时态知识逻辑模型检测工具MCTK刻画贷款协议Web服务实例，并验证相关的时态知识规范。在同一实验环境下，采用另一种时态知识逻辑模型检测工具MCMAS进行建模，并验证该实例。实验结果表明，基于MCTK的Web服务模型检测方法比基于MCMAS的方法更有效。
|
| 关 键 词： | 模型检测 时态知识逻辑 多智能体系统 Web服务 |
| 修稿时间： | |
Formal Verification for Web Service |
| |
| LUO Xiang-yu,CHEN Yan. Formal Verification for Web Service[J]. Computer Engineering, 2010, 36(5): 257-259 |
| |
| Authors: | LUO Xiang-yu CHEN Yan |
| |
| Affiliation: | (School of Computer and Control, Guilin University of Electronic Technology, Guilin 541004) |
| |
| Abstract: | 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. |
| |
| Keywords: | model checking temporal logics of knowledge multi-agent system Web service |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载免费的PDF全文 |
