期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于SPIN的BPEL4WS建模与验证研究

Researches on the Modeling and Verification of BPE14WS Based on Spin
下载PDF
导出
摘要 Web服务组合研究领域的一个重要问题是如何形式化描述Web服务组合,验证服务组合的正确性,Web服务组合的形式化模型可以用来检查和验证Web服务组合以保证组合的正确性.文章使用模型检查工具SPIN对目前普遍使用的Web服务组合规范BPEL4WS(Business Process Execution Language for Web Services,Web服务业务流程执行语言)模型进行了验证,给出了BPEL4WS语法到Promela形式化模型的转换方法,最后通过一个实例对BPEL4WS表示的服务组合模型的安全性、活性和有界性等特性进行了验证分析,从而给出了基于SPIN的BPEL4WS表示的Web服务组合模型验证的方法. One of important issues in web service composition researching area is how to describe web service composition formally and verify the correctness. A formal model of web service composition can be used to check and verify web service composition so that the correctness of web service composition can be guaranteed. This paper gives the transform method from BPEL4WS to Promela and verifies the model based on SPIN. At last, this paper gives an example of web service composition and the model checking method through verifying the safeness, liveness and boundness of the model.
作者 孙军梅 周娇蓉
机构地区 杭州师范大学信息科学与工程学院
出处 《杭州师范大学学报（自然科学版）》 CAS 2010年第5期385-391,共7页 Journal of Hangzhou Normal University(Natural Science Edition)
关键词 WEB服务组合 模型检测 SPIN BPEL4WS web service composition model checking SPIN BPEL4WS
分类号 TP311 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献9

  • 1Holzmann G J.The spin model checker:primer and reference manual[M].Baston:Addison Wesley,2003.
  • 2Mcmillan K L.The SMV system for SMV version 2.5.4[CP].http://www.cs.cmu.edu/-modelcheck/smv/smvmanual.ps,October,2006.
  • 3Ankolekar A,Paolucci M,Sycara K.Spinning the OWL-S process model-towards the verification of the OWL-S process models[C]//In:Semantic Web Services:Preparing to Meet the World of Business Applications Workshop at ISWC,Hiroshima:2004.
  • 4Andrew Tony.Business Process Execution Language for Web Services Version 1.1.[CP].W3C Web Site,May 2003:1-136.
  • 5Fu Xiang,Bultan T,Su Jianwen.WSAT:a tool for formal analysis of web services[J].Lecture Notes in Computer Science,2004,3114:394-395.
  • 6Fu Xiang,Bultan T,Su Jianwen.Model checking interactions of composite Web services[R].Tech Report 2004-05,Computer Science Department,University of California at Santa Barbara,California:2004.
  • 7Nakajima S.Model-checking verification for reliable web service[C].In:Proc.OOPSLA'02 Workshop on Object-Oriented Web Services,Washington:2002.
  • 8廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证[J].计算机学报,2005,28(4):635-643. 被引量：107
  • 9门鹏,段振华.基于着色Petri网的BPEL建模与验证[J].西北大学学报（自然科学版）,2007,37(6):986-990. 被引量：8

二级参考文献24

  • 1孙健,陶晓峰.基于Petri网的Web服务BPEL4WS建模与分析[J].计算机工程,2004,30(22):14-16. 被引量：9
  • 2张力,赵宗涛,慕晓冬,邵军勇.一种分析作战指控并发信息流的Petri网模型[J].西北大学学报（自然科学版）,2006,36(1):33-35. 被引量：1
  • 3Koehler J., Srivastava B. Web service composition: Current solutions and open problems. In: Proceedings of the 13th International Conference on Automated Planning & Scheduling, Trento, Italy, 2003, 28～35
  • 4Milner R. Communication and Concurrency. Englewood Cliffs: Prentice -Hall, 1989
  • 5Fensel D. The semantic web and its languages. IEEE Intelligent Systems, 2000, 15(6): 67～73
  • 6Milner R. Communicating and Mobile Systems: The Pi-Calculus. Cambridge: Cambridge University Press, 1999
  • 7Milner R., Parrow J., Walker D. A calculus of mobile processes, part I/II. Journal of Information and Computation, 1992, 100(1): 1～77
  • 8Lin Hui-Min. Complete proof systems for observation congruences in finite control pi-calculus. In: Proceedings of the 25th International Colloquium on Automata, Languages and Programming, Aalborg, Denmark, 1998, 443～454
  • 9Jiao Wen-Pin, Zhou Ming-Hui, Wang Qian-Xiang. Formal framework for adaptive multi-agent Systems. In: Proceedings of IEEE/WIC International Conference on Intelligent Agent Technology, Halifax, Canada, 2003, 442～445
  • 10Markus Lumpe. A Pi-calculus based approach to software composition [Ph.D. dissertation]. Institute of Computer Science and Applied Mathematics, University of Bern, Switzerland, 1999

共引文献113

杭州师范大学学报（自然科学版）
2010年 第5期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部