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

摘要：

Web服务组合的形式化描述和验证是一个重要的研究问题.为了更好地完成验证工作,提出了扩展着色Petri网的模型检测方法.首先,在着色Petri网原有的基于CTL的局部模型检测算法基础上,给出了获取模型检测证据/反例的算法,并在着色Petri网模型检测工具--CPN Tools--中使用ML(meta language)语言实现了这些算法,然后将扩展后的CPN模型检测工具应用在Web服务组合的验证问题中.该方法不仅可以验证Web服务组合是否存在逻辑错误,还能告诉用户发生错误的原因,为Web服务组合的验证提供了技术上的保障.实验表明对着色Petri网的模型检测工具的扩展是正确、有效的.

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

所属期刊栏目：46

分类号：TP393;TP301(计算技术、计算机技术)

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

在线出版日期：2009-09-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：1294-1303