着色Petri网模型检测工具的扩展及其在Web服务组合中的应用  

Extension of Model Checking Tool of Colored Petri Nets and Its Applications in Web Service Composition

作　　者：门鹏[1] 段振华[1] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,西安710071

出　　处：《计算机研究与发展》2009年第8期1294-1303,共10页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60433010;60873018);教育部高等学校博士学科点基金项目(200807010012)~~

摘　　要：Web服务组合的形式化描述和验证是一个重要的研究问题.为了更好地完成验证工作,提出了扩展着色Petri网的模型检测方法.首先,在着色Petri网原有的基于CTL的局部模型检测算法基础上,给出了获取模型检测证据/反例的算法,并在着色Petri网模型检测工具——CPNTools——中使用ML(metalanguage)语言实现了这些算法,然后将扩展后的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.

关 键 词：着色PETRI网 WEB服务组合 形式化验证 模型检测 时序逻辑 

分 类 号：TP393[自动化与计算机技术—计算机应用技术] TP301[自动化与计算机技术—计算机科学与技术]