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

被引：23

作者：

门鹏

段振华

机构：

[1] 西安电子科技大学计算理论与技术研究所

来源：

计算机研究与发展 | 2009年 / 46卷 / 08期

关键词：

着色Petri网; Web服务组合; 形式化验证; 模型检测; 时序逻辑;

D O I：

暂无

中图分类号：

TP393.09 [];

学科分类号：

摘要：

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

引用

页码：1294 / 1303

页数：10

共 4 条

[1]

AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].