文献类型：期刊文章

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

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

出　　处：《计算机研究与发展》

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

年　　份：2009

卷　　号：46

期　　号：8

起止页码：1294-1303

语　　种：中文

收录情况：AJ、BDHX、BDHX2008、CSA-PROQEUST、CSCD、CSCD2011_2012、EI、IC、JST、RCCSE、SCOPUS、ZGKJHX、核心刊

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

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

分 类 号：TP393] TP301[计算机类]