欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
Web服务组合的形式化描述和验证是一个重要的研究问题．为了更好地完成验证工作，提出了扩展着色Petri网的模型检测方法．首先，在着色Petri网原有的基于CTL的局部模型检测算法基础上，给出了获取模型检测证据／反例的算法，并在着色Petri网模型检测工具——CPN Tools——中使用ML（meta language）语言实现了这些算法，然后将扩展后的CPN模型检测工具应用在Web服务组合的验证问题中．该方法不仅可以验证Web服务组合是否存在逻辑错误，还能告诉用户发生错误的原因，为Web服务组合的验证提供了技术上的保障．实验表明对着色Petri网的模型检测工具的扩展是正确、有效的．
英文摘要：
Formal description and verification of Web services composition are important research issues. To better complete the verification, an extended model checking method based on colored Petri nets is proposed. The latest version of the colored Petri net model checking tool can only determine the correctness of temporal logic formulas, and no further diagnosis information is available. Based on the local model checking algorithm of CTL （computational tree logic） in colored Petri nets, an algorithm for searching witness or counterexample Of the model checking result is investigated. The algorithm is implemented using ML（meta language） language, and fluently integrated in the colored Petri net model checking tool named CPN-tools. Then, the extended CPN model checking tool can be used in the verification of Web service composition. With this approach, CPN is used to describe the behaviors of Web service composition, and CTL logic formulas are used for specifying the requirements of target Web services. The method can not only check the logical errors in Web service composition, but also tell users the reasons for the errors. This extension provides the technical guarantees for the Web service composition validation based on the colored Petri nets. Experiments demonstrate that the extension is correct and effective.
同期刊论文项目
同项目期刊论文
期刊信息
位置：