| 基于着色Petri网的BPEL建模与验证 |
| |
| 引用本文： | 门鹏,段振华.基于着色Petri网的BPEL建模与验证[J].西北大学学报,2007,37(6):986-990. |
| |
| 作者姓名： | 门鹏 段振华 |
| |
| 作者单位： | 西安电子科技大学计算机学院 陕西西安710071 |
| |
| 基金项目： | 国家自然科学基金;教育部高等学校博士学科点专项科研基金 |
| |
| 摘 要： | 目的为了保证使用商业过程执行语言(BPEL)描述的Web服务组合的正确性。方法用着色Petri网(CP-nets)对BPEL流程进行建模、分析以及验证。结果定义了一套从BPEL到CP-nets的映射规则,该规则可以将BPEL流程转换成CP-nets,通过着色Petri网工具-CPN tools对该CP-nets进行自动分析以及验证,从而验证该BPEL流程的安全性、活性等性质。结论利用CP-nets这种形式化工具可以有效地发现BPEL流程中存在的设计错误。
|
| 关 键 词： | 着色Petri网 |
| 文章编号： | 1000-274X（2007）06-0986-05 |
| 收稿时间： | 2007-03-21 |
| 修稿时间： | 2007年3月21日 |
A colored Petri net based on approach for BPEL modeling and verification |
| |
| MEN Peng,DUAN Zhen-hua.A colored Petri net based on approach for BPEL modeling and verification[J].Journal of Northwest University(Natural Science Edition),2007,37(6):986-990. |
| |
| Authors: | MEN Peng DUAN Zhen-hua |
| |
| Abstract: | Aim To ensure the correctness of Web service composition described by BPEL.Methods The Colored Petri nets(CP-nets) are employed to modeling,analysis and verifying BPEL processes.Results A given BPEL process can be transformed into CP-nets with a set of translation rules.By implementing CPN tools,the properties of the given BPEL processes,such as security and liveness,can be verified.Conclusion By utilizing CP-nets,the design flaws of BPEL processes can be found effectively. |
| |
| Keywords: | BPEL Web services |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
