检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
作 者:杨璐[1,2] 柳溪[1,2] 王林章[1,2] 陈鑫[1,2] 李宣东[1,2]
机构地区:[1]南京大学计算机软件新技术国家重点实验室,南京210093 [2]南京大学计算机科学与技术系,南京210093
出 处:《计算机学报》2009年第9期1759-1772,共14页Chinese Journal of Computers
基 金:国家自然科学基金项目(60673125;90818022);国家"八六三"高技术研究发展计划项目基金(2009AA01Z48);江苏省基础研究计划项目基金(BK2007714)资助~~
摘 要:采用UML顺序图构成基于场景的规约、WS-BPEL作为Web服务的描述语言,提出了一种面向基于场景规约对Web服务消息流进行分析与验证的方法:首先,对WS-BPEL消息流进行分析并将其自动抽象为基于Petri网的模型;同时,为了缩小状态空间、提高验证效率,在不影响消息交互顺序的前提下,对WS-BPEL源码和基于Petri网的模型分别进行化简,即面向基于场景规约将与验证无关的活动和元素删除;最后,通过遍历基于Petri网的模型以验证WS-BPEL消息流与基于场景的规约之间的一致性(消息交互顺序的存在/强制一致性).文中通过一个贯穿整个分析与验证过程的实例加以说明.该方法已经实现成为一个原型工具.This paper purposes a scenario-based analysis and verification approach for the Web Services message flow, in which UML Sequence Diagrams are used to specify scenario-based specifications and WS-BPEL is used to describe Web Services designs. Firstly the authors analyze a WS-BPEL specification and automatically extract its message flow model expressed by a Petri net. At the same time, according to a given scenario-based specification the authors do the simpli- fication for both the WS-BPEL source code and the Petri net model to reduce the state space for efficient verification, i.e. removing the activities and process elements which are not concerned with the verification against the scenario-based specification. Finally, the authors verify the con- sistency between the WS-BPEL message flow and the scenario-based specification (existential/ mandatory consistency of message sequence) by traversing the Petri net model. A case study is given throughout the analysis and verification process to illustrate the approach. And a prototype tool is implemented to support this approach.
分 类 号:TP311[自动化与计算机技术—计算机软件与理论]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:216.73.216.28