基于π-演算的BPEL4WS性质检验
|
摘要
随着Web服务的出现和推广,基于Web服务的动态服务组合技术也成为近年的研究热点。Web服务的业务流程执行语言(BPEL4WS)作为一种基于业务流程的服务组合方法,建模理论基础比较薄弱,组合正确性的保证较弱。因此流程的正确性、无死锁性等问题,在它正式被实施前必须得到形式上的模拟与检验。
基于形式化方法的研究工作,本文提出利用π-演算和μ-演算对BPEL4WS进行性质检验的方法。
建模方面,除了提出利用π-演算对BPEL4WS的建模方法外,考虑到手工建模的复杂度,在开发的检验工具中实现了π-演算对BPEL4WS建模的自动转换算法,用户可以利用本文的工具指定BPEL4WS文件自动生成其对应的π-演算模型。
性质描述方面,分析BPEL4WS可能出现的一些常规错误,并利用μ-演算给出了描述示例。
检验工具方面,开发了一个新的检验工具。实现上文提到的自动化建模,嵌入已有的检验工具MWB,对其检验算法加以改进,当模型不满足性质时可以输出有错的子模型片段,并首次尝试把出错路径反馈到BPEL4WS源文件中做出标识,基本实现了对BPEL4WS的自动化性质检验。
这样对于用户来说,从建模到检验几乎都是透明的,用户不用深入了解形式化方法的知识,就可以直接用本文开发的工具进行性质检验,并可以针对检验后标识的地方改进。本文的结果说明对BPEL4WS的自动
Along with the prosperity and acceptance of the Web services, the technique of dynamic service composition based on Web Services has been regarded as one of the hot research topics. The Business Process Execution Language for Web services (BPEL4WS) as to be a service composition method, which is based on business process, is weak in modeling, and the assurance of the validity is also weak. So the validity of the process and the property of non-deadlocks must be simulated and proved before being implemented formally.Based on the research of formal method, the method of checking the property of BPEL4WS, which make use of π -calculus and μ -calculus, has been put forward in this paper.In the aspect of modeling, in addition to put forward a method of modeling, in consideration of the complications of modeling by user, we have carried out the automatic conversion algorithm for modeling the BPEL4WS by π--calculus. Using the tool mentioned in this paper, the BPEL4WS file specified by user can create the π-calculus model automatically.In the aspect of describing property, we have analyzed some
errors which appear probably in BPEL4WS, and given the description example in u -calculus.In the aspect of tool, we have developed a new tool which carried out the automatic modeling mentioned in preceding context.This new tool, embedding the being tool ---- MWB and improvingthe algorithm, can return the erring snippet when the model can' t fulfill some given properties, and first try to remark the error path in the BPEL4WS source file, implementing the automatically check on the properties of BPEL4WS.It is almost transparent from modeling to checking for user. So, the user who doesn' t understand the formal method thoroughly can do the check using the tool and do the improvement aiming at the tagged place. The result of this paper has explained that it is feasible to check the property of BPEL4WS and tag the erring path automatically.
基于形式化方法的研究工作,本文提出利用π-演算和μ-演算对BPEL4WS进行性质检验的方法。
建模方面,除了提出利用π-演算对BPEL4WS的建模方法外,考虑到手工建模的复杂度,在开发的检验工具中实现了π-演算对BPEL4WS建模的自动转换算法,用户可以利用本文的工具指定BPEL4WS文件自动生成其对应的π-演算模型。
性质描述方面,分析BPEL4WS可能出现的一些常规错误,并利用μ-演算给出了描述示例。
检验工具方面,开发了一个新的检验工具。实现上文提到的自动化建模,嵌入已有的检验工具MWB,对其检验算法加以改进,当模型不满足性质时可以输出有错的子模型片段,并首次尝试把出错路径反馈到BPEL4WS源文件中做出标识,基本实现了对BPEL4WS的自动化性质检验。
这样对于用户来说,从建模到检验几乎都是透明的,用户不用深入了解形式化方法的知识,就可以直接用本文开发的工具进行性质检验,并可以针对检验后标识的地方改进。本文的结果说明对BPEL4WS的自动
Along with the prosperity and acceptance of the Web services, the technique of dynamic service composition based on Web Services has been regarded as one of the hot research topics. The Business Process Execution Language for Web services (BPEL4WS) as to be a service composition method, which is based on business process, is weak in modeling, and the assurance of the validity is also weak. So the validity of the process and the property of non-deadlocks must be simulated and proved before being implemented formally.Based on the research of formal method, the method of checking the property of BPEL4WS, which make use of π -calculus and μ -calculus, has been put forward in this paper.In the aspect of modeling, in addition to put forward a method of modeling, in consideration of the complications of modeling by user, we have carried out the automatic conversion algorithm for modeling the BPEL4WS by π--calculus. Using the tool mentioned in this paper, the BPEL4WS file specified by user can create the π-calculus model automatically.In the aspect of describing property, we have analyzed some
errors which appear probably in BPEL4WS, and given the description example in u -calculus.In the aspect of tool, we have developed a new tool which carried out the automatic modeling mentioned in preceding context.This new tool, embedding the being tool ---- MWB and improvingthe algorithm, can return the erring snippet when the model can' t fulfill some given properties, and first try to remark the error path in the BPEL4WS source file, implementing the automatically check on the properties of BPEL4WS.It is almost transparent from modeling to checking for user. So, the user who doesn' t understand the formal method thoroughly can do the check using the tool and do the improvement aiming at the tagged place. The result of this paper has explained that it is feasible to check the property of BPEL4WS and tag the erring path automatically.
引文
[1] 徐洋.面向服务设计的Web服务组合系统中动态选取机制的研究与实现:[硕士学位论文].东北大学信息科学与工程学院,2005年。
[2] Web服务的业务流程执行语言版本1.1 2003年5月5日 http://www.ibm.com/developerworks/library/ws-bpel/。
[3] Tadao Murata. Petri Net: Properties, Analysis and Applications. Proceedings of the IEEE, 1989, 77(4): 541-580。
[4] R. Milner. Communication and Concurrency. Prentice Hali, 1989。
[5] G. Piccinelli, S. L. Williams. Workflow: A language for composing web services. In W.M.P. van derAalst, A.H.M. ter Hofstede, and M. Weske, editors, Proceedings of the International Conference on Business Process Management, volume 2678 of Lecture Notes in Computer Science, pages 1-12, Eindhoven, June 2003. Springer-Verlag。
[6] W. M. P. van der Aalst and A. H. M. ter Hofstede. Workow patterns: on the expressive power of (Petrinet-based) workow languages. In K. Jensen, editor, Proceedings of the Fourth Workshop on the Practical Use of Coloured Petri Nets and CPN Tools, volume 560 of DAIMI PB series, pages 1-20, Aarhus, August 2002. University of iarhus。
[7] R. Cleaveland, J. Parrow, B. Steffen. The Concurrency Workbench: A semantics-based verification tool for verification of concurrent system. ACM Transactions on Programming languages and Systems, 1993, 5(1):36-72.
[8] M. Schroeder. Verification of business processes for a correspondence handling center using CCS. In A. I. Vermesan and F. Coenen, editors, Proceedings of European Symposium on Validation and Verification of Knowledge Based Systems and Components, pages 1—15, Oslo, June 1999. Kluwer.
[9] Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey,1991.
[10] Gerard J. Holzmann. The Model checker SPIN. IEEE Transactions on Software Engineering, 1997, 23(5):279-295.
[11] S. Nakajima. Verification of web services ows with model-checking techniques. In Proceedings of the First International Symposium on Cyber Worlds, pages 378-386, Tokyo, November 2002. IEEE Computer Society Press.
[12] C. Karamanolis, D. Giannakopoulou, J. Magee, and S. M. Wheater. Model checking of workow schemas. In Proceedings of the 4th International Enterprise Distributed Object Computing Conference, pages 170-179, Makuhari, Japan, September 2000. IEEE Computer Society Press.
[13] Milner R.. Communicating and Mobile Systems:The Pi-Calculus. Cambridge: Cambridge University Press, 1999。
[14] Milner R., Parrow J., Walker D.. A calculus of mobile processes, part Ⅰ/Ⅱ journal of Information and Computation, 1992, 100(1): 1-77。
[15] Bjorn Victor. The Mobility Workbench User's Guide Polyadic version 3.122. 1995.10 http://www.it.uu.se/profundis/mwb-dist/guide-3.122.ps.gz
[16] Bjorn Victor, Faron Moller. The Mobility Workbench - A Tool for the Pi-Calculus. 1994 http://user.it.uu.se/~victor/tr/docs-tr-94-45, htmt。
[17] K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Carneie-Mellon University, Department of Computer Sciences, Report CMU-CS-92-131, 1992。
[18] Glenn Bruns. Distributed Systems Analysis with CCS, 1997。
[19] 刘锋.安全协议模型检验技术研究与实现:[硕士学位论文].国防科学技术大学研究生院,2002年。
[20] E. A. Emerson E. M. Clarke and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transition on Programming Languages and Systems, April 1986.6, 8(2): 244-263。
[21] Joost-Pieter Katoen. Concepts, Algorithms, and Tools for Model Checking. 1999, http://scholar.google.com/url?sa:U&q=http://www.ift.ulaval.ca/~jodesharnais/Verification/avvs. ps. gz。
[22] 林惠民,张文辉。模型检测:理论、方法与应用.电子学报,2002年12月,第12A期。
[23] 杜旭涛.π-演算交互式验证工具的研究与实现:[硕士学位论文].国防科学技术大学研究生院,2002年。
[24] Colin Stirling. Modal and temporal logics for processes. In Logics for Concurrency, volume 1043 of LNCS. Springer, 1996。
[25] Colin Stirling. Modal and temporal properties of Processes. Springer, 2001。
[26] 傅建明,韩光鹏,朱福喜.两种死锁分析的逻辑方法.武汉大学学报(自然科学版)1999年6月,第45卷第3期。
[27] Riccardo Pucella. Notes on Programming Standard ML of New Jersey(version 110.0.6). 2001 http://www.cs.cornell.edu/riccardo/prog-smlnj/notes-011001. pdf。
[28] Fredrick. rhe Model Prover-a sequent-calculus based modal μ-calculus model checker tool for finite control π-calculus agents. 1998, http://www.it.uu.se/profundis/mwb-dist/x4.p.s.gz。
[29] Colin Stirling, David Walker. Local model checking in the modal mu-calculus. Dept. of Computer Science, University of Edinburgh Theoretical Computer Science, 1991。
[30] Zhang jia, Chung Jeir Yao, Chang C. K, Kim S.. WS-Net: A petri-net based specification model for web services. In: Proceedings of the 2nd IEEE International Conference on Web Services, San Diego, California, USA, 2004, 420-427。
[31] 廖军,谭浩,刘锦德.基于Pi-演算的web服务组合的描述和验证.计算机学报,2005年4月,第28卷第4期,635-643。
[32] Karamanolis C., Giannakopoulou D., Magee J., Wheater S. M.. Model checking of workflow schemas. In: Proceedings of the 4th International Enterprise Distributed Object Computing Conference, Makuhari, Japan, 2000, 170-179。
[33] Forster H., Uchitel S., Magee J., Kramer J.. Model based verification of web service compositions. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, Montreal, Canada, 2003, 152-161。
[34] Koshkina M., van Breugel F.. Modelling and verifying Web service orchestration by means of the concurrency workbench. ACM SIGSOFT SEN, 2004, 29(5): 1-10。
[35] Andrea Ferrara. Web Iervices: A Process Algebra Approach. In ICSOC' 04: Proceedings of the 2nd international conference on Service oriented computing, pages 242-251, New York,
?NY, USA, 2004. ACM Press。
[2] Web服务的业务流程执行语言版本1.1 2003年5月5日 http://www.ibm.com/developerworks/library/ws-bpel/。
[3] Tadao Murata. Petri Net: Properties, Analysis and Applications. Proceedings of the IEEE, 1989, 77(4): 541-580。
[4] R. Milner. Communication and Concurrency. Prentice Hali, 1989。
[5] G. Piccinelli, S. L. Williams. Workflow: A language for composing web services. In W.M.P. van derAalst, A.H.M. ter Hofstede, and M. Weske, editors, Proceedings of the International Conference on Business Process Management, volume 2678 of Lecture Notes in Computer Science, pages 1-12, Eindhoven, June 2003. Springer-Verlag。
[6] W. M. P. van der Aalst and A. H. M. ter Hofstede. Workow patterns: on the expressive power of (Petrinet-based) workow languages. In K. Jensen, editor, Proceedings of the Fourth Workshop on the Practical Use of Coloured Petri Nets and CPN Tools, volume 560 of DAIMI PB series, pages 1-20, Aarhus, August 2002. University of iarhus。
[7] R. Cleaveland, J. Parrow, B. Steffen. The Concurrency Workbench: A semantics-based verification tool for verification of concurrent system. ACM Transactions on Programming languages and Systems, 1993, 5(1):36-72.
[8] M. Schroeder. Verification of business processes for a correspondence handling center using CCS. In A. I. Vermesan and F. Coenen, editors, Proceedings of European Symposium on Validation and Verification of Knowledge Based Systems and Components, pages 1—15, Oslo, June 1999. Kluwer.
[9] Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey,1991.
[10] Gerard J. Holzmann. The Model checker SPIN. IEEE Transactions on Software Engineering, 1997, 23(5):279-295.
[11] S. Nakajima. Verification of web services ows with model-checking techniques. In Proceedings of the First International Symposium on Cyber Worlds, pages 378-386, Tokyo, November 2002. IEEE Computer Society Press.
[12] C. Karamanolis, D. Giannakopoulou, J. Magee, and S. M. Wheater. Model checking of workow schemas. In Proceedings of the 4th International Enterprise Distributed Object Computing Conference, pages 170-179, Makuhari, Japan, September 2000. IEEE Computer Society Press.
[13] Milner R.. Communicating and Mobile Systems:The Pi-Calculus. Cambridge: Cambridge University Press, 1999。
[14] Milner R., Parrow J., Walker D.. A calculus of mobile processes, part Ⅰ/Ⅱ journal of Information and Computation, 1992, 100(1): 1-77。
[15] Bjorn Victor. The Mobility Workbench User's Guide Polyadic version 3.122. 1995.10 http://www.it.uu.se/profundis/mwb-dist/guide-3.122.ps.gz
[16] Bjorn Victor, Faron Moller. The Mobility Workbench - A Tool for the Pi-Calculus. 1994 http://user.it.uu.se/~victor/tr/docs-tr-94-45, htmt。
[17] K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Carneie-Mellon University, Department of Computer Sciences, Report CMU-CS-92-131, 1992。
[18] Glenn Bruns. Distributed Systems Analysis with CCS, 1997。
[19] 刘锋.安全协议模型检验技术研究与实现:[硕士学位论文].国防科学技术大学研究生院,2002年。
[20] E. A. Emerson E. M. Clarke and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transition on Programming Languages and Systems, April 1986.6, 8(2): 244-263。
[21] Joost-Pieter Katoen. Concepts, Algorithms, and Tools for Model Checking. 1999, http://scholar.google.com/url?sa:U&q=http://www.ift.ulaval.ca/~jodesharnais/Verification/avvs. ps. gz。
[22] 林惠民,张文辉。模型检测:理论、方法与应用.电子学报,2002年12月,第12A期。
[23] 杜旭涛.π-演算交互式验证工具的研究与实现:[硕士学位论文].国防科学技术大学研究生院,2002年。
[24] Colin Stirling. Modal and temporal logics for processes. In Logics for Concurrency, volume 1043 of LNCS. Springer, 1996。
[25] Colin Stirling. Modal and temporal properties of Processes. Springer, 2001。
[26] 傅建明,韩光鹏,朱福喜.两种死锁分析的逻辑方法.武汉大学学报(自然科学版)1999年6月,第45卷第3期。
[27] Riccardo Pucella. Notes on Programming Standard ML of New Jersey(version 110.0.6). 2001 http://www.cs.cornell.edu/riccardo/prog-smlnj/notes-011001. pdf。
[28] Fredrick. rhe Model Prover-a sequent-calculus based modal μ-calculus model checker tool for finite control π-calculus agents. 1998, http://www.it.uu.se/profundis/mwb-dist/x4.p.s.gz。
[29] Colin Stirling, David Walker. Local model checking in the modal mu-calculus. Dept. of Computer Science, University of Edinburgh Theoretical Computer Science, 1991。
[30] Zhang jia, Chung Jeir Yao, Chang C. K, Kim S.. WS-Net: A petri-net based specification model for web services. In: Proceedings of the 2nd IEEE International Conference on Web Services, San Diego, California, USA, 2004, 420-427。
[31] 廖军,谭浩,刘锦德.基于Pi-演算的web服务组合的描述和验证.计算机学报,2005年4月,第28卷第4期,635-643。
[32] Karamanolis C., Giannakopoulou D., Magee J., Wheater S. M.. Model checking of workflow schemas. In: Proceedings of the 4th International Enterprise Distributed Object Computing Conference, Makuhari, Japan, 2000, 170-179。
[33] Forster H., Uchitel S., Magee J., Kramer J.. Model based verification of web service compositions. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, Montreal, Canada, 2003, 152-161。
[34] Koshkina M., van Breugel F.. Modelling and verifying Web service orchestration by means of the concurrency workbench. ACM SIGSOFT SEN, 2004, 29(5): 1-10。
[35] Andrea Ferrara. Web Iervices: A Process Algebra Approach. In ICSOC' 04: Proceedings of the 2nd international conference on Service oriented computing, pages 242-251, New York,
?NY, USA, 2004. ACM Press。
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |