BPEL流程的故障模式及其静态分析技术的研究
|
摘要
Web服务已经成为我们生活中的重要组成部分。面向服务计算的目的是通过组装独立的、松耦合的服务为构建软件提供基础。由于任何软件开发活动,包括开发组合服务,都需要执行应用的质量评估策略,尤其是验证和测试。服务组合是一个能够提供包括语言、规范等多种功能在内的SOA当前的一个发展趋势，它具有异构性、开放和分布式等鲜明特征。服务组合的出现和发展为未来的软件发展指出了演进的方向,同时也为工业界和学术界提出了新的任务和挑战。保证组合服务的正确性执行以及相关特性的验证问题显得尤为重要。
随着基于BPEL的组合服务在业界的日益普及,并逐渐成为企业应用集成的重要组成部分。各种组合流程经常表现的不尽人意,呈现出脆弱、难以置信的特征,甚至会给企业带来不可挽回的经济损失。对于像BPEL这种安全性要求极高的业务应用,也许一个很小的错误,就会造成重大的经济损失。因此,研究提高组合流程可信性技术成为十分重要的头等大事。
目前,服务组合技术还远未成熟,要想在大规模的商业中实现有效应用,还有许多关键技术和具体问题需要突破。任何企业和个人都无法保证所开发的业务流程一定没有问题,能够在开发的早期发现错误,便可以减少大量严重错误的发生几率,减少企业的经济损失。已经出现的模型检测技术和各种各样的动态测试技术,尽管能够对一定规模的流程进行验证,但这些方法在某种程度上都存在一定的局限性,比如流程规模(一般只适用于较小流程)和测试开销(测试费用昂贵)。而基于缺陷的软件测试技术,不需要运行被测系统,而且可以避免模型检查和组合路径的状态爆炸问题,通过对缺陷建模以及精确的检测算法,可以检测出流程中存在的相应缺陷,从而进一步提高对流程可靠性的可信度。在这种背景下,本文从组合流程中可能存在的缺陷方面入手,集中对服务组合语言BPEL中的缺陷及测试进行了深入而系统的研究,并取得了一系列有价值的研究成果,概括起来主要包括以下几个方面：
(1)在对BPEL规范、语法、语义等进行理解和分析的基础上,结合现有的对组合服务的故障分类,首次提出了基于缺陷的BPEL静态检测方法,确保流程在部署之前进行全面的检测,减少故障发生的几率。除了BPEL规范中给出的94个缺陷,我们又针对性的提出了16个BPEL缺陷。
(2)针对上面提到的110个故障提出了一种通用的缺陷检测方法：采用扩展的有限状态机(EFSM)对缺陷进行建模,沿着状态机的变迁条件对BPEL源代码进行检测。为了在控制流图中表示BPEL并发和同步的语义,对传统控制流图进行了扩展。实现中统筹考虑,将link语义和路径条件有机集合起来,提高了检测的精度；
(3)数据竞争作为困扰并发语言正确性的因素,在时间戳的基础上,采用向量时钟获得活动之间的发生序关系,为确保存在数据竞争的活动实际能够执行,减少数据竞争的误报,对事件增加了权值,进一步提高了检测效率。
(4)除了单一流程内部的控制依赖死锁,还对流程间的死锁进行了深入分析,提出了“流程摘要”的概念,用以记录流程执行信息。该信息只与具体缺陷相关,从而在进行流程间的缺陷分析时,仅通过“流程摘要”便可以检测出流程间的通信问题,减少全面流程依赖图分析的系统开销。
除此而外,本文还对组合服务产生的背景、研究现状、研究热点以及其它相关问题进行了高度的概括和总结,对全面认识和把握基于BPEL的组合web服务具有积极的作用。
Web services have become a vital part of our lives.Service Oriented Computing (SOC) is aimed at providing the bases for building software by assembling independent, loosely coupled services. As any software development activity, also building a composite service requires strategies for performing quality assessment of applications and, in particular, verification and testing. The correctness and verification of web service orchestration is very important.
Service composition can provide a lot of funchtions, such as composition language, specification and so on; it is a current trend of SOA. It characterized by heterogeneous, open, distributed and other distinctive. The emergence and development portfolio of services propose the direction for the future evolution of software development, and also put forward new tasks and challenges for the industry and academia.
With the growing populariy of BPEL-based service composition, many of today's enterprises construct their IT in such a way that individual applications are encapsulated as services which has become an important component in the enterprise applications. However, there is no guarantee that a composition of even very good services will always work, showing a weak and incredible features and event impose an irreversible economic loss. For the security-critical BPEL process, perhaps a small error can cause a significant economic loss. So improving the redibility of composition service becomes a top priority problem.
Currently, service composition is far from being mature, in order to achieve large-scale commerce application, there are many key technologies and specific problem need to be break through. Any enterprise or individual can not guarantee that the development of the business process is correct, if we can find the errors during the development phase, it can reduce the probability of orrurrence of serious errors during the running phase. Modeling checking and variety of dynamic testing methods have emerged, which validating and certificating the process from part of aspects, but these methods have some liminations to some extent, such as the size of process under test and the testing cost. In the defect-based software testing technology, there is no need to run the system under test, and can also avoids the state exposition problem of model checking. Through the detecting algorithm and defect model, it can detect the corresponding defects in the process. So it can further enhance the credibility of the process reliability. In this context, this dissertation makes deep and systematic research on the defects, which is the core in the static analysis, and made a series of valuable research results, the main contributions are as follows:
Firstly, on the basis of understanding and analyzing BPEL specification、 syntax、semantics, combined with the existing fault classification for service composition, firstly proposed the defect-based static detecting method of BPEL This method can ensure the comprehensive detection priori to deployment and reduce the risk of failure. In addition to the94defects, we give16defects specially.
Secondly, we propose a common method to defect the110defects given above—using the extened finite state machine (EFSM) to model the defects and detecting the BPEL source code along the transidion condition of EFSM. In order to express the semantic of concurrency and synchronization, the tranditional control flow graph is expanded. During the analysis, based on the overall consideration, we attempt to combine the path consition and link complete semantic, which can effectively improve the accuracy.
Thirdly, datarace is a factor that puzzles the correntness of concurrent language. On the basis of timestamp, we use the vector clock to compare the happen-before relation. To ensure that the activities of process can occur actually, reduce the number of false positive, we add the weighted value of events which further improve the efficiency of detection.
Fourthly, In addition to intra-process control dependcy deadlock, inter-processes can also generate deadlock. The "process summary" is proposed to resove this problem, which records the execution information of process and related to concrete defect, so when analyzing the defects among the inter-process, only through the "process summary" is able to detect communication problems and reduce the overall cost of the process dependence graph of the system.
In addition, for the purpose of keeping an overall understanding and grasping to the composition defects, some important issues with regard to composition defects are also described.
随着基于BPEL的组合服务在业界的日益普及,并逐渐成为企业应用集成的重要组成部分。各种组合流程经常表现的不尽人意,呈现出脆弱、难以置信的特征,甚至会给企业带来不可挽回的经济损失。对于像BPEL这种安全性要求极高的业务应用,也许一个很小的错误,就会造成重大的经济损失。因此,研究提高组合流程可信性技术成为十分重要的头等大事。
目前,服务组合技术还远未成熟,要想在大规模的商业中实现有效应用,还有许多关键技术和具体问题需要突破。任何企业和个人都无法保证所开发的业务流程一定没有问题,能够在开发的早期发现错误,便可以减少大量严重错误的发生几率,减少企业的经济损失。已经出现的模型检测技术和各种各样的动态测试技术,尽管能够对一定规模的流程进行验证,但这些方法在某种程度上都存在一定的局限性,比如流程规模(一般只适用于较小流程)和测试开销(测试费用昂贵)。而基于缺陷的软件测试技术,不需要运行被测系统,而且可以避免模型检查和组合路径的状态爆炸问题,通过对缺陷建模以及精确的检测算法,可以检测出流程中存在的相应缺陷,从而进一步提高对流程可靠性的可信度。在这种背景下,本文从组合流程中可能存在的缺陷方面入手,集中对服务组合语言BPEL中的缺陷及测试进行了深入而系统的研究,并取得了一系列有价值的研究成果,概括起来主要包括以下几个方面：
(1)在对BPEL规范、语法、语义等进行理解和分析的基础上,结合现有的对组合服务的故障分类,首次提出了基于缺陷的BPEL静态检测方法,确保流程在部署之前进行全面的检测,减少故障发生的几率。除了BPEL规范中给出的94个缺陷,我们又针对性的提出了16个BPEL缺陷。
(2)针对上面提到的110个故障提出了一种通用的缺陷检测方法：采用扩展的有限状态机(EFSM)对缺陷进行建模,沿着状态机的变迁条件对BPEL源代码进行检测。为了在控制流图中表示BPEL并发和同步的语义,对传统控制流图进行了扩展。实现中统筹考虑,将link语义和路径条件有机集合起来,提高了检测的精度；
(3)数据竞争作为困扰并发语言正确性的因素,在时间戳的基础上,采用向量时钟获得活动之间的发生序关系,为确保存在数据竞争的活动实际能够执行,减少数据竞争的误报,对事件增加了权值,进一步提高了检测效率。
(4)除了单一流程内部的控制依赖死锁,还对流程间的死锁进行了深入分析,提出了“流程摘要”的概念,用以记录流程执行信息。该信息只与具体缺陷相关,从而在进行流程间的缺陷分析时,仅通过“流程摘要”便可以检测出流程间的通信问题,减少全面流程依赖图分析的系统开销。
除此而外,本文还对组合服务产生的背景、研究现状、研究热点以及其它相关问题进行了高度的概括和总结,对全面认识和把握基于BPEL的组合web服务具有积极的作用。
Web services have become a vital part of our lives.Service Oriented Computing (SOC) is aimed at providing the bases for building software by assembling independent, loosely coupled services. As any software development activity, also building a composite service requires strategies for performing quality assessment of applications and, in particular, verification and testing. The correctness and verification of web service orchestration is very important.
Service composition can provide a lot of funchtions, such as composition language, specification and so on; it is a current trend of SOA. It characterized by heterogeneous, open, distributed and other distinctive. The emergence and development portfolio of services propose the direction for the future evolution of software development, and also put forward new tasks and challenges for the industry and academia.
With the growing populariy of BPEL-based service composition, many of today's enterprises construct their IT in such a way that individual applications are encapsulated as services which has become an important component in the enterprise applications. However, there is no guarantee that a composition of even very good services will always work, showing a weak and incredible features and event impose an irreversible economic loss. For the security-critical BPEL process, perhaps a small error can cause a significant economic loss. So improving the redibility of composition service becomes a top priority problem.
Currently, service composition is far from being mature, in order to achieve large-scale commerce application, there are many key technologies and specific problem need to be break through. Any enterprise or individual can not guarantee that the development of the business process is correct, if we can find the errors during the development phase, it can reduce the probability of orrurrence of serious errors during the running phase. Modeling checking and variety of dynamic testing methods have emerged, which validating and certificating the process from part of aspects, but these methods have some liminations to some extent, such as the size of process under test and the testing cost. In the defect-based software testing technology, there is no need to run the system under test, and can also avoids the state exposition problem of model checking. Through the detecting algorithm and defect model, it can detect the corresponding defects in the process. So it can further enhance the credibility of the process reliability. In this context, this dissertation makes deep and systematic research on the defects, which is the core in the static analysis, and made a series of valuable research results, the main contributions are as follows:
Firstly, on the basis of understanding and analyzing BPEL specification、 syntax、semantics, combined with the existing fault classification for service composition, firstly proposed the defect-based static detecting method of BPEL This method can ensure the comprehensive detection priori to deployment and reduce the risk of failure. In addition to the94defects, we give16defects specially.
Secondly, we propose a common method to defect the110defects given above—using the extened finite state machine (EFSM) to model the defects and detecting the BPEL source code along the transidion condition of EFSM. In order to express the semantic of concurrency and synchronization, the tranditional control flow graph is expanded. During the analysis, based on the overall consideration, we attempt to combine the path consition and link complete semantic, which can effectively improve the accuracy.
Thirdly, datarace is a factor that puzzles the correntness of concurrent language. On the basis of timestamp, we use the vector clock to compare the happen-before relation. To ensure that the activities of process can occur actually, reduce the number of false positive, we add the weighted value of events which further improve the efficiency of detection.
Fourthly, In addition to intra-process control dependcy deadlock, inter-processes can also generate deadlock. The "process summary" is proposed to resove this problem, which records the execution information of process and related to concrete defect, so when analyzing the defects among the inter-process, only through the "process summary" is able to detect communication problems and reduce the overall cost of the process dependence graph of the system.
In addition, for the purpose of keeping an overall understanding and grasping to the composition defects, some important issues with regard to composition defects are also described.
引文
[1-1]Domenico Bianculli, Carlo Ghezzi and Cesare Pautasso, Embedding Continuous Lifelong Verification in Service Life Cycles. In Proceedings of the 2009 International Workshop on Principles of Engineering Service Oriented Systems (PESOS 2009), pp.99-102. IEEE 2009.
[1-2]D. Bianculli and C. Ghezzi. Towards a methodology for lifelong validation of service compositions. In Proc. of SDSOA 2008, pages 7-12. ACM,2008.
[1-3]K. Beck. Test Driven Development by Example. Addison Wesley Professional, November 2002.
[1-4]Chan, K.S.M. The Usage of Formal Methods in Web services Context:a Reality Check. Technical Report,2009. http://www.cs.up.ac.za/cs/ksmchan/reports/FM_WS_Survey_2009.pdf
[1-5]宫云战.软件测试教程[M].北京：机械工业出版社,2008.
[1-6]宫云战.软件测试[M].北京：国防工业出版社,2006.
[1-7]郑人杰.计算机软件测试技术.北京：清华大学出版社,1992.
[1-8]Quinlan, D. J.; Vuduc, R. W.; Misherghi, G. Techniques for specifying bug patterns. In Proceedings of the 2007 ACM workshop on Parallel and distributed systems:testing and debugging, London, 2007:27-35.
[1-9]宫云战.一种面向故障的软件测试新方法[J].装甲兵工程学院学报,2004(1)：21-35.
[1-10]宫云战.软件测试的故障模型[J].装甲兵工程学院学报,2004：18(2)：1-5
[1-11]王雅文.基于缺陷模式的软件测试技术研究[博士学位论文],北京：北京邮电电大学,2009.
[1-12]K. S. Chan, J. Bishop, J. Steyn, L. Baresi, and S. Guinea. A Fault Taxonomy for Web Service Composition. In Proc. of the 3rd Int. Work. On Engineering Service-Oriented Applications, pages 363-375,2007.
[1-13]Pistore, M., Barbon, F., Bertoli, P., Shaparau, D., and Traverso, P. Planning and Monitoring Web Service Composition, Proc.11th Intl. Conf. on Artificial Intelligence.106-115,2004.
[2-1]K. S. Chan, J. Bishop, J. Steyn, L. Baresi, and S. Guinea. A Fault Taxonomy for Web Service Composition. In Proc. of the 3rd Int. Work. On Engineering Service-Oriented Applications, pages 363-375,2007.
[2-2]Iribarne L.:Web Components:A comparison between Web services and software components, In: Colombian Journal of Computation,5 (1):pp.47--66,2004.
[2-3]Avizienis A., Laprie J-C, Randell B., and Landwehr C.:Basic Concepts and Taxonomy of Dependable and Secure Computing, In:IEEE Transactions on Dependable and Secure Computing, 1(1):pp.11-32,2004.
[2-4]Fngini MG.Mussi E Recovery of faulty Web applications through service discovery. In proceedings of the 1st SMR-VLDB workshop, Matchmarking and Approximate Semantic-based Retrival:Issues and Perspectives.2006:67-80
[2-5]Bruning S.Weissleder S.Malek M. A fault taxonomy for service-oriented architecture In Proceedings of the 10th IEEE International Symposium on High Assurance Systems Engineering, HASE 2007:267-268.
[2-6]刘丽,况晓辉,方兰web服务故障分类方法.计算机应用系统,2010,19(8),pp：258-265。
[2-7]李喜彤,范玉顺.web服务流程相容性和相似性分析.计算机学报32(12),2009：
[2-8]van der Aalst, W.M.P.. Workflow verification:finding control-flow errors using Petri net-based techniques. Business Process Management. Berlin:Springer-Verlag,2000,161-183.
[2-9]刘方方, 史玉良, 张亮等. 基于进程代数的Web服务合成的替换分析. 计算机学报,2007,30(11)：2033-2039
[2-10]Dong W L, Yu H, Zhang Y B. Testing BPEL-based web service composition using High-level Petri Nets [C]. Proceesing of the tenth IEEE international enterprise distributed object computing conference (EDOC'06). Hong Kong,2006.
[2-11]钱柱中,路桑璐, 谢立.基于petri网的web服务自动组合研究[J].计算机学报,2006,29(7)：1057-1066.
[2-12]P.Mayer and D.Lubke, Towards a BPEL unit testing framework, Proceedings of Workshop on Testing, analysis, and verification of web services and applications, ACM Press,2006:33-42
[2-13]Z.Li, W.Sun, Z.Jiang, et al, BPEL4WS unit testing:Framework and implementation, IEEE International Conference on Web Services,2005:103-110
[2-14]Y.Yuan,Z.J.Li,W.Sun,A Graph-Search Based Approach to BPEL4WS Test Generation,International Conference on Software Engineering Advances,2006:14-14
[2-15]J.Yan,Z.J.Li,Y.Yuan,et al,BPEL4WS unit testing:Test Case Generation Using a Concurrent Path Analysis Approach,International Symposium on Software Reliability Engineering,2006:75-84
[2-16]A. Estero-Botaro, F. Palomo-Lozano, and I. Medina-Bulo, "Mutation operators for WS-BPEL 2.0," in ICSSEA 2008:21th International Conference on Software & Systems Engineering and their Applications, Paris, France,2008.
[2-17]A. Estero-Botaro, F. Palomo-Lozano, and I. Medina-Bulo, "Quantitative Evaluation of Mutation Operators for WS-BPEL Compositions". In ICSTW 2010:3rd International Conference on Software Testing, Verification, and Validation Workshops, p 142-150,2010.
[2-18]曾云峰,基于BCCFG的WS BPEL测试用例生成研究.(硕士毕业论文)
[2-19]Ganna Monakova. Ontology Based Partner Service Discovery Using a First-Order Logic Representation for BPEL Process Models. Diploma thesis, University of Stuttgart, Institute of Architecture of Application Systems,2008.
[2-20]Tevfik Bultan, Xiang Fu, Jianwen Su. Tools for Automated Verification of Web Services[C]. Farn Wang, (Editor) ATVA. Springer,2004, vol.3299 of Lecture Notes in Computer Science,8-10. URL http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=32 99&spage=8
[2-21]H. Foster, S. Uchitel, J. Magee, J. Kramer. Model-based Verification of Web Service Compositions[C].18th IEEE Inter. Conference on Automated Software Engineering (ASE'03). IEEE Computer Society,2003
[2-22]H. Foster, S. Uchitel, J.Magee, J. Kramer. Tool Support for Model-Based Engineering of Web Service Compositions[C]. Proc. of ICWS'05. Washington, DC, USA:IEEE CS,2005,95-102
[2-23]Howard Foster. A Rigorous Approach to Engineering Web Service Compositions [D]. Ph.D. thesis, Department of Computing, Imperial College of Science, Technology and Medicine, University of London, January 2006. URL http://www.doc.ic.ac.uk/-hfl/phd/downloads/hf-thesis-ds-2006.pdf.
[2-24]Mariya Koshkina, Franck van Breugel. Verification of Business Processes for Web Services[R]. Technical report CS-2003-11, York University, Oct.2003. Available from: http://www.cs.yorku.ca/techreports/2003/
[2-25]Mariya Koshkina, Franck van Breugel. Modelling and verifying web service orchestration by means of the concurrency workbench [J]. SIGSOFT Softw Eng Notes.2004,29(5):1-10.
[2-26]G. Salaun, L. Bordeaux, M. Schaerf. Describing and Reasoning on Web Services using Process Algebra[C].2nd Inter. Conference on Web Services. IEEE,2004
[2-27]G.Diaz et al.:Automatic Translation of WS-CDL Choreographies to Timed Automata. In:Proc. WS-FM'05. Number 3670 in LNCS, Springer (2005) 230-242.
[2-28]肖庆,杨朝红,毕学军.一种基于故障模式状态机的测试方法.北京化工大学学报.Vol34,sup 1,2007,pp73-76.
[2-29]Barkaoui, K.; Eslamichalandar, M.; Kaabachi, M. A structural verification of web services composition compatibility. Proceedings of the 6th International Workshop on Enterprise & Organizational Modeling and Simulation.2010:30-41.
[2-30]http://www.uml.org.cn/Test/201003033.asp.
[2-31]徐春香,屈婉玲,王捍贫等.死路径语义下的WS-BPEL流程建模.北京大学学报(自然科学版).2010,46(2)：162-170.
[3-1]OASIS. Web Service Business Process Execution Language (WS-BPEL) [EB/OL]. [2009-12-1]. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf.
[3-2]Sun Ping, Jiang Changjun. Analysis of workflow dynamic changes based on Petri net, Information and Software Technology [J],2009,51(2):284-292.
[3-3]Mukherjee A, Tari Z and Bertok P. Modeling of BPEL Composite Services Using Clustered Coloured Petri-Nets[C]//2009 World Conference on Services-Ⅱ, Washington, USA:ACM Press,2009:55-62.
[3-4]Lucchi R, Mazzara M. A pi-calculus based semantics for WS-BPEL [J]. Journal of Logic and Algebraic Programming Web Services and Formal Methods,2007,70(1):96-118.
[3-5]Yan J, Li Z, Yu. Y, et al. BPEL4WS Unit Testing:Test Case Generation Using a Concurrent Path Analysis Approach [C]//2006 International Symposium on Software Reliability Engineering (ISSRE '06), Washington, USA:ACM Press,2006:75-84.
[3-6]宫云战.一种而向故障的软件测试新方法[J].装甲兵工程学院学报,2004(1)：21-25.
[3-7]宫云战.软件测试教程[M].北京：机械工业出版社,2006.89-134.
[3-8]杨朝红,宫云战,肖庆等.基于软件缺陷模型的测试系统[J].北京邮电大学学报,2008,31(5)：1-4.
[3-9]Huynh K. Analysis through refection:walking the EMF model of BPEL4WS.Master's thesis [D]. York University, Toronto, Canada, September 2005.
[3-10]AHO A V, SETHI R, ULLMAN J D. Compilers:prin2ciples, techniques, and tools [M]. Beijing: Posts &Telecom Press, Pearson Education,2002.608-633.
[3-11]H. Foster, S. Uchitel, J, Magee and J. Kramer, Model-based verification of web service compositions. In Proc. ASE'03,2003.
[3-12]R. Kazhamiakin and M. Pistore. Static verification of control and data inweb service compositions. IEEE International Conference on web services (ICWS'06).
[3-13]R. Kazhamiakin, M. Pistore and L.Santuari. A Parametric Communication Model for the Verification of Web Service Composition. In Proc.WWW'06,2006.
[3-14]M. Rouached and C. Godart. Requirements-driven verification of wsbpel processes[C].1CWS 2007,354-363.
[3-15]M. Rouached, O.Perrin and C. Godart. Towards Formal Verification of Web Service Composition [J]. Business Process Management 2006,257-273.
[3-16]Mariya Koshkina and Franck van Breugel "Verification of Business Process for Web Services", Technical Report, Department of Computers Science, York University, Canada, Oct 2003.
[3-17]Chun Ouyang, Eric Verbeek, Wil M.P. van der Aalst, Stephan Breutel, Marlon Dumas, Arthur H.M. ter Hofstede. Applying model checking to BPEL4WS business collaborations. In ACM Symposium on Applied Computing, pages 826-830,2005.
[3-18]Juan M. vara, Valeria De Castro, and Esperanza Marcos. WSDL automatic generation from uml models in a mda framework. In International Journal of Webservices Practices, pages 112.Web Services Research Foundation, Seoul, Korea,2005.
[3-19]David Skogan, Roy Grnmo, and Ida Solheim. "Web service composition in UML". In Proceedings of 8th International Enterprise Distributed Object Computing Conference (EDOC 2004), pages 4757, Monterey, California, USA,20-24 September 2004.
[3-20]Keith Mantell. "From UML to BPEL, model driven architecture in a web services world."IBM developer works, September 9 2003.
[3-21]XiaochuanYi and Krys J. Kochut. "A CP-net-based design and verification framework for web services composition."In Proceedings of the IEEE InternationalConference on Web Services (ICWS04), pages 756-760. IEEE,2004.
[3-22]G. J. Holzmann. The SPIN Model Checker:Primer and Reference Manual. Addison-Wesley, Boston, Massachusetts,2003.
[3-23]王勇,代桂平,侯亚荣,等.基于并发事务逻辑的web服务编制验证.电子学报.2009,37(10)：2228-2233.
[3-24]张广梅,陈蕊,李晓维.面向软件故障检测的数据流分析.全国第13届计算机辅助设计与图形学(CAD/CG)学术会议,2004,pp25 1-255.
[4-1]Monakova, G., et al.:Verifying Business Rules Using an SMT Solver for BPEL Processes. In:BPSC. (2009)
[4-2]Francisco Curbera et al. Exception Handling in the BPEL4WS Language. In Conference on Business Process Management, pages 276-290. Springer,2003.
[4-3]F.van Breygel, M.Koshkina. Dead-path-elimination in BEPL4WS. Acsd,00:192-201,2005. doi: 10.1109/ACSD.2005.11.
[4-4]A.Ferrara, Webservices:A process algebra approach, in:Proceedings of 2nd International Conference on Service Oriented Computing, ACM Press, New York, NY,USA,2004,pp.242-251.
[4-5]G. Monakova, O. Kopp, and F. Leymann, "Improving control flow verification in a business process using an extended Petri net," in ZEUS 2009:1st Central-European Workshop on Services and their Composition,2009, pp.95-101.
[4-6]Sun Ping and Jiang Changjin. Analysis of workflow dynamic changes based on Petri net, Inf. Softw. Technol,2009,51(2):284-292.
[4-7]Mukherjee A, Tari Z and Bertok P. Modeling of BPEL Composite Services Using Clustered Coloured Petri-Nets. World Conference on Services-Ⅱ,2009, pp.55-62.
[4-8]J.A. Fisteus, L.S. Fernandez, and C.D. Kloos. Formal verification of BPEL4WS business collaborations. In Proceedings of 5th International Conference on Electronic Commerce and Web Technologies (EC-Web'04),2004.8,31(80) 76-85.
[4-9]Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of Web service composition. In Proceedings of 18th IEEE International Conference on Automated Software Engineering,2003.10: 152-161.
[4-10]X. Fu. Specification and Verification of Asynchronously Communication Web Service [Ph.D. dissertation]. University of California, Santa Barbara,2004.
[4-11]雷丽晖 段振华.一种基于扩展有限自动机验证组合Web服务的方法[J].软件学报,2007,18(12)：2980-2990.
[4-12]WOMBACHER A, FANKHAUSER P, MAHLEK O B, et al.Matchmaking for business processes based on choreographies[C].Proceedings of the 2004 IEEE International Conference on E-Technology, E-Commerce and E2 Service. Washington, DC:IEEE Computer Society,2004:359-368.
[4-13]杨璐,柳溪,王林章等.面向基于场景规约的web服务消息流分析与验证.计算机学报.2009,32(9)：1759-1772.
[4-14]ZHENG YONGYAN, ZHOU JIONG, KRAUSE P. Analysis of BPEL data dependencies[C]. Proceedings of the 33rd EUROM ICRO Conference on Software Engineering and Advanced Applications. Washington, DC:IEEE Computer Society,2007:351-358.
[4-15]KHALAF R, K OPP O, LEY MANN F. Maintaining data dependencies across BPEL process fragments [J]. International Journal of Cooperative Information Systems,2008,17 (3):259-282.
[4-16]O. Kopp, R. Khalaf, and F. Leymann. Reaching Definitions Analysis Respecting Dead Path Elimination Semantics in BPEL Processes. Technical Report 2007/04, University Stuttgart, IAAS, 2007.
[4-17]O.Kopp, R.Khalaf, F.Leymann. Deriving Explicit Data Links in WS-BPEL processes. In IEEE SCC 2008:367-376
[4-18]肖庆,宫云战,杨朝红等.一种路径敏感的静态缺陷检测方法.软件学报,2010.01,21(2)：209-217.
[4-19]Das M, Lerner S, Seigle M. ESP:Path-Sensitive program verification in polynomial time. In: Knoop J, Hendren LJ, eds. Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation. New York:ACM Press,2002:57-68.
[4-20]杨朝红,宫云战,肖庆等.基于软件缺陷模型的测试系统.北京邮电大学学报.2008.10,31(5)：1-4
[4-21]C. Ouyang et,al. Formal Semantics and Analysis of Control Flow in WS-BPE. Science of computer programming, Elsevier, North-Holland,2007, vol.67, pp.162-198.
[4-22]Dong Wenli, Hu Jianhua. Test Method for BEPL-Based Web Service Composition Based on Data Flow Analysis. Journal of software,2009,20(8),467-470.
[4-23]R.Farahbod, U.Glasser, M.Vajihollahi, Abstract operational semantics of the business process execution language for Web services, Technical Report SFU-CMPT-TR-2004-03, School of Computer Science, Simon Fraser University, Burnaby B.C., Canada, April2004.
[4-24]Fu, X., Bultan, T., Su,J. Analysis of interacting BPEL web services. Proceedings of the 13th international conference on World Wide Web, WWW2004, New York, NY, USA, May 17-20,2004, ACM Press (2004) 621-630
[4-25]Shin Nakajima. Model-Checking Behavioral Specification of BPEL Applications. Electronic Notes in Theoretical Computer Science.2006,151(2):89-105.
[4-26]杨朝红,宫云战,肖庆等.基于缺陷模型的软件测试中的区间运算应用.计算机付辅助与图形设计学报,2009,20(12)：1630-1635.
[4-27]Frank Leymann and Dieter Roller. Production Workflow-Concepts and Techniques. PTR Prentice Hall,2000.
[4-28]徐春香,屈婉玲,工捍贫等.死路径语义下的WS-BPEL流程建模.北京大学学报(自然科学版).2010,46(2)：162-170.
[4-29]Ouyang Chun, Verbeek E, Aalst W M P, et al. Formal semantics and analysis of control flow in WS-BPEL.Science of Computer Programming,2007,67 (2/3):162-198.
[4-30]Aho AV, Lam MS, Sethi R, Ullman JD. Compilers Principles, Techniques, and Tools.2nd ed., New York:Addison-Wesley,2006.626-632.
[5-1]P. Baldy, H. Dicky, R. Medina, M. Morvan, and J.-F. Vilarem. "Efficient Reconstruction of the Causal Relationship in Distributed Computations". Technical Report 92-013, Laboratoired'Informatique, de Robotique et deMicroelectronique de Montpellier, France, June 1992.
[5-2]J.S. Ostroff and W.M Wonham. A temporal logic approach to real time control. In Proc.24th Conf.Decision Contr. Pages 656-657,1985.
[5-3]F. Mattern. "Virtual Time and Global States in Distributed Systems". Proc. Workshop on Parallel and Distributed Algorithms, Chateau de Bonas, Oct.1988, M. Cosnard et al. (eds.), Elsevier/North Holland, pages 215-226,1989.
[5-4]C.J. Fidge, Dynamic Analysis of Event Orderings in Message-Passing Systems, doctoral dissertation, Australian Nat'l Univ.,1989.
[5-5]SAVA GES, BURROWS S, NELSON G, et al. Eraser:a dynamic data race detect for multithreaded programs [J]. ACM Transactions on Computer Systems,1997,15(4):391-411.
[5-6]M Christiaens. "TRaDe, A topological approach to on-the-fly race detection in java programs". Proceedings of the 2001 Symposium on JavaTM Virtual Machine Research and Technology Symposium.
[5-7]L. Lamport. Time, clocks, and the ordering of events in a distributed system.Communications of the ACM,21 (7):pages 558-565,1978.
[5-8]A.D. Kshemkalyani and M.Singhal. "Characterization of Distributed Deadlocks." Tech. Report OSU-CISRC-6/90-TR15. Computer and Information Science Research Center. Ohio State Univ.,Columbus,Ohio,1990
[5-9]Reinhard Schwarz. "Detecting Causal Relationships in Distributed Computations:In Search of the Holy Grail". Report SFB 124-15/92, December 1992
[5-10]K.S. Trivedi, "Probabiliy and Satistic:with Reliability, Queuing, and Computer Science Applications", Prentice Hall, Englewood Cliffs, N.J.,1982.
[5-11]M.Raynal and A.Schiper. "The Causal Ordering Abstraction and a Simple Way to Implement it.' Tech. Report 1132, INRIA.Paris,1989.
[5-12]W. Dong, H. Yu, Y. Zhang. "Testing BPEL-based Web Service Composition Using High-level Petri Nets". Enterprise Distributed Object computing Conference, EDOC, pages 441-444,2006.
[5-13]Jianjun Cui, "DRD4BPEL:A Tool for Data Race Detection of BPEL Process," wcse, World Congress on Software Engineering, pages 200-205,2009.
[5-14]S. Nakajima, "Verification of Web Service Flows with Model-Checking Techniques", Proc. of the First International Symposium on CW'02, IEEE, pages 378-385,2002.
[5-15]The Eclipse Modeling Framework (EMF) Overview, http://help.eclipse.org/ganymede/index. jsp?topic=/org.eclipse.emf.doc/references/overview/EMF.html
[5-16]Y. Zheng, J. Zhou, and P. Krause. "An automatic test Case generation framework for web services," Journal of Software, pages 64-77,2007.
[5-17]陈胜,鲍亮,陈平等BPEL流程数据竞争和死锁检测算法研究[J].西安电子科技大学学报：自然科学版,2008,35(6)：1058-1062.
[5-18]李少东,许蕾.一种基于发生序和锁集的BPEL数据竞争静态检测方法.计算机与数字工程.2010,38(8)：6-9.
[5-19]R. H. B. Netzer, B. P. M iller. What are Race Conditions? Some Issues and Formalizations [J]. ACM Letters on Programming Languages and Systems,1992,1(1):74-88
[5-20]J. Cardoso, A. Sheth, et al. Workflow Quality of Service. In International Conference on Enterprise Integration and Modeling Technology and International Enterprise Modeling Conference, Valencia, Spain, Kluwer Publishers,2002.
[5-21]Xiu, Jia-Peng, Xu Yan-Ting, Deng Fang et.al. A Petri Net-based approach for data race detection in BPEL. Journal of China Universities of Posts and Telecommunications.2011,17(2):10-15.
[5-22]吴萍,陈意云,张建.多线程程序数据竞争的静态检测.计算机研究与发展[J],2006,43(2)：329-335.
[5-23]J. D. Choi, et al., Efficient and precise datarace detection for multithreaded object-oriented programs. ACM SIGPLAN Notices, vol.37, pp.258-269,2002.
[5-24]W. Landi. Undecidability of static analysis. ACM Letters on Programming Languages and Syatems,1992,1(4):323-337.
[5-25]C.Praun, T. Gross. Static conflict analysis for multi-threaded object-oriented programs. In:Proc. ACM SIGPLAN 2003 Conf. Programming Language Design and Implementation. New York:ACM Press,2003,115-128.
[5-26]杨书新,李淑芝,张永进.基于BPEL的流程数据竞争问题研究.计算机应用,2010,30(7)：1959-1962.
[5-27]翟岩龙,宿红毅,张晗,等.基于数据流优化的BPEL流程分割力法[J].华南理大学学报,2009,37(4)：24-30.
[6-1]Koshkina M, Breugel F. Modelling and Verifying Web Service Orchest ration by Means of the Concurrency Workbench [C]//TAV2WEB Proceedings. Portland:ACM Press,2004:1210.
[6-2]E. W. Dijkstra, "Solutions of a problem in concurrent programming control," Communications of the ACM, vol.8, p.569,1965.
[6-3]E. G. Coffman, et al., "System deadlocks," ACM Computing Surveys (CSUR), vol.3, pp.67-78, 1971.
[6-4]Flanagam C,Leino K M, Lillibridge M, et al. Extended static checking for java[C]//Proceeding of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02), 2006:234-245.
[6-5]E. Farchi, et al., Concurrent bug patterns and how to test them[C]//Proceeding of the 17th International Symposium on Parallel and Distributed Processing.[S.1]:IEEE computer Society,2003.
[6-6]Hovemeyer D, Pugh W. Finding bugs is easy [J].SIGPLAN Not,2004,39(12):92-106.
[6-7]G. Yorsh, E. Yahav, and S. Chandra. Generating Precise and Concise Procedure Summaries. In Proceedings of the 35th Annual Acm Sigplan-Sigact Symposium on Principles of Programming Languages,221-234,2008.
[6-8]S. Gulwani and A. Tiwari. Computing procedure summaries for interprocedural analysis. Programming Languages and Systems:253-267,2007.
[6-9]X. Fu, T. Bultan, J. Su. Analysis of Interacting BPEL Web Services. In International World Wide Web Conference:Proceedings of the 13th international conference on World Wide Web, pp.621-630. ACM Press, New York, NY, USA,2004.
[6-10]C. Ouyang, et al., Formal semantics and analysis of control flow in WS-BPEL. Science of Computer Programming, vol.67, pp.162-198,2007.
[6-11]N. Lohmann, P. Massuthe, C. Stahl, D. Weinberg, Analyzing interacting BPEL processes, in:S. Dustdar, J.L. Fiadeiro, A.P. Sheth (Eds.),Proceedings of the International Conference on Business Process Management, BPM 2006, Vienna, Austria, September 2006, in:Lecture Notes in Computer Science, vol.4102, Springer-Verlag,2006, pp.17-32.
[6-12]Klai, K., Tata, S., Desel, J.:Symbolic Abstraction and Deadlock-Freeness Verification of Inter-enterprise Processes. Proceedings of the 7th International Conference on Business Process Management, Lecture Notes in Computer Science Vol.5701, pp 294-309 (2009).
[6-13]Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D. Analyzing interacting WS-BPEL processes using flexible model generation. Data and Knowledge Engineering 64(1),38-54 (2008).
[6-14]Cheng Y., Wang Z.:Research on Reachability Verification of Web Service Composition. World Congress on Software Engineering, pp.233-237 (2009).
[6-15]Aalst, W.M., Mooij, A.J., Stanl, C., Wolf, K. Service Interaction:Patterns, Formalization, and Analysis. Formal Methods for Web Services, p.88 (2009).
[6-16]宋艳,高春鸣.基于移动工作台的BPEL4WS死锁验证.计算机工程,2007,33(1)：92-95.
[6-17]傅建明,韩光鹏,朱福喜.两种死锁分析的逻辑方法[J].武汉大学学报(自然科学版)1999,45(3)
[6-18]Tetsuya Maruta, Senichi Onoda, Yoshitomo lkkai, et al. A deadlock detection algorithm for business processes workflow models[C]. In:Proceedings of 1998 IEEE International Conference on Systems, Man, and Cybernetics, San Diego, CA, USA,1998, pp.611-616.
[6-19]Senichi Onoda, Yoshitomo Ikkai, Takashi Kobayashi, et al. Definition of deadlock patterns for business processes work on models[C]. In:Proceedings of the Annual Hawaii International Conference on System Sciences, Maui, Hawaii,1999, pp.1-4.
[6-20]Ezpeleta J, Colom J M, and Martinez J. A Petri net based deadlock prevention policy for flexible manufacturing systems [J]. IEEE Transaction on Robotics and Automation,11(2),1995, pp.173-184.
[6-21]陈胜,鲍亮,陈平等BPEL流程数据竞争和死锁检测算法研究[J].西安电子科技大学学报,35(6),2008,pp.1056-1063.
[6-22]J. A. Fisteus, et al., Formal verification of BPEL4WS business collaborations, E-Commerce and Web Technologies, pp.123-131,2004.
[6-23]Tasharofi, S., Vakilian, M., Moghaddam, R.Z., Sirjani, M.:Modeling web service interactions using the coordination language Reo. In:Proc. of the Int. Workshop on Web Services and Formal Methods. Volume 4937 of LNCS. Springer (2008) 108-123.
[6-24]R.J. van Glabbeek, D.G. Stork, Query nets:interacting workflow modules that ensure global termination, in:W.M.P. van der Aalst, A.H.M. ter Hofstede, M. Weske (Eds.), International Conference on Business Process Management (BPM 2003), Lecture Notes in Computer Science, vol. 2678, Springer-Verlag, Berlin,2003, pp.184-199.
[6-25]G. Decker and J. Mendling, "Instantiation semantics for process models," Business Process Management, pp.164-179,2008.
[6-26]PTimothy Mark Pinkston, Sugath Warnakulasuriya,On deadlocks in interconnection networks. ACM SIGARCH Computer Architecture News,1997,25(2):38-49.
[1-2]D. Bianculli and C. Ghezzi. Towards a methodology for lifelong validation of service compositions. In Proc. of SDSOA 2008, pages 7-12. ACM,2008.
[1-3]K. Beck. Test Driven Development by Example. Addison Wesley Professional, November 2002.
[1-4]Chan, K.S.M. The Usage of Formal Methods in Web services Context:a Reality Check. Technical Report,2009. http://www.cs.up.ac.za/cs/ksmchan/reports/FM_WS_Survey_2009.pdf
[1-5]宫云战.软件测试教程[M].北京：机械工业出版社,2008.
[1-6]宫云战.软件测试[M].北京：国防工业出版社,2006.
[1-7]郑人杰.计算机软件测试技术.北京：清华大学出版社,1992.
[1-8]Quinlan, D. J.; Vuduc, R. W.; Misherghi, G. Techniques for specifying bug patterns. In Proceedings of the 2007 ACM workshop on Parallel and distributed systems:testing and debugging, London, 2007:27-35.
[1-9]宫云战.一种面向故障的软件测试新方法[J].装甲兵工程学院学报,2004(1)：21-35.
[1-10]宫云战.软件测试的故障模型[J].装甲兵工程学院学报,2004：18(2)：1-5
[1-11]王雅文.基于缺陷模式的软件测试技术研究[博士学位论文],北京：北京邮电电大学,2009.
[1-12]K. S. Chan, J. Bishop, J. Steyn, L. Baresi, and S. Guinea. A Fault Taxonomy for Web Service Composition. In Proc. of the 3rd Int. Work. On Engineering Service-Oriented Applications, pages 363-375,2007.
[1-13]Pistore, M., Barbon, F., Bertoli, P., Shaparau, D., and Traverso, P. Planning and Monitoring Web Service Composition, Proc.11th Intl. Conf. on Artificial Intelligence.106-115,2004.
[2-1]K. S. Chan, J. Bishop, J. Steyn, L. Baresi, and S. Guinea. A Fault Taxonomy for Web Service Composition. In Proc. of the 3rd Int. Work. On Engineering Service-Oriented Applications, pages 363-375,2007.
[2-2]Iribarne L.:Web Components:A comparison between Web services and software components, In: Colombian Journal of Computation,5 (1):pp.47--66,2004.
[2-3]Avizienis A., Laprie J-C, Randell B., and Landwehr C.:Basic Concepts and Taxonomy of Dependable and Secure Computing, In:IEEE Transactions on Dependable and Secure Computing, 1(1):pp.11-32,2004.
[2-4]Fngini MG.Mussi E Recovery of faulty Web applications through service discovery. In proceedings of the 1st SMR-VLDB workshop, Matchmarking and Approximate Semantic-based Retrival:Issues and Perspectives.2006:67-80
[2-5]Bruning S.Weissleder S.Malek M. A fault taxonomy for service-oriented architecture In Proceedings of the 10th IEEE International Symposium on High Assurance Systems Engineering, HASE 2007:267-268.
[2-6]刘丽,况晓辉,方兰web服务故障分类方法.计算机应用系统,2010,19(8),pp：258-265。
[2-7]李喜彤,范玉顺.web服务流程相容性和相似性分析.计算机学报32(12),2009：
[2-8]van der Aalst, W.M.P.. Workflow verification:finding control-flow errors using Petri net-based techniques. Business Process Management. Berlin:Springer-Verlag,2000,161-183.
[2-9]刘方方, 史玉良, 张亮等. 基于进程代数的Web服务合成的替换分析. 计算机学报,2007,30(11)：2033-2039
[2-10]Dong W L, Yu H, Zhang Y B. Testing BPEL-based web service composition using High-level Petri Nets [C]. Proceesing of the tenth IEEE international enterprise distributed object computing conference (EDOC'06). Hong Kong,2006.
[2-11]钱柱中,路桑璐, 谢立.基于petri网的web服务自动组合研究[J].计算机学报,2006,29(7)：1057-1066.
[2-12]P.Mayer and D.Lubke, Towards a BPEL unit testing framework, Proceedings of Workshop on Testing, analysis, and verification of web services and applications, ACM Press,2006:33-42
[2-13]Z.Li, W.Sun, Z.Jiang, et al, BPEL4WS unit testing:Framework and implementation, IEEE International Conference on Web Services,2005:103-110
[2-14]Y.Yuan,Z.J.Li,W.Sun,A Graph-Search Based Approach to BPEL4WS Test Generation,International Conference on Software Engineering Advances,2006:14-14
[2-15]J.Yan,Z.J.Li,Y.Yuan,et al,BPEL4WS unit testing:Test Case Generation Using a Concurrent Path Analysis Approach,International Symposium on Software Reliability Engineering,2006:75-84
[2-16]A. Estero-Botaro, F. Palomo-Lozano, and I. Medina-Bulo, "Mutation operators for WS-BPEL 2.0," in ICSSEA 2008:21th International Conference on Software & Systems Engineering and their Applications, Paris, France,2008.
[2-17]A. Estero-Botaro, F. Palomo-Lozano, and I. Medina-Bulo, "Quantitative Evaluation of Mutation Operators for WS-BPEL Compositions". In ICSTW 2010:3rd International Conference on Software Testing, Verification, and Validation Workshops, p 142-150,2010.
[2-18]曾云峰,基于BCCFG的WS BPEL测试用例生成研究.(硕士毕业论文)
[2-19]Ganna Monakova. Ontology Based Partner Service Discovery Using a First-Order Logic Representation for BPEL Process Models. Diploma thesis, University of Stuttgart, Institute of Architecture of Application Systems,2008.
[2-20]Tevfik Bultan, Xiang Fu, Jianwen Su. Tools for Automated Verification of Web Services[C]. Farn Wang, (Editor) ATVA. Springer,2004, vol.3299 of Lecture Notes in Computer Science,8-10. URL http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=32 99&spage=8
[2-21]H. Foster, S. Uchitel, J. Magee, J. Kramer. Model-based Verification of Web Service Compositions[C].18th IEEE Inter. Conference on Automated Software Engineering (ASE'03). IEEE Computer Society,2003
[2-22]H. Foster, S. Uchitel, J.Magee, J. Kramer. Tool Support for Model-Based Engineering of Web Service Compositions[C]. Proc. of ICWS'05. Washington, DC, USA:IEEE CS,2005,95-102
[2-23]Howard Foster. A Rigorous Approach to Engineering Web Service Compositions [D]. Ph.D. thesis, Department of Computing, Imperial College of Science, Technology and Medicine, University of London, January 2006. URL http://www.doc.ic.ac.uk/-hfl/phd/downloads/hf-thesis-ds-2006.pdf.
[2-24]Mariya Koshkina, Franck van Breugel. Verification of Business Processes for Web Services[R]. Technical report CS-2003-11, York University, Oct.2003. Available from: http://www.cs.yorku.ca/techreports/2003/
[2-25]Mariya Koshkina, Franck van Breugel. Modelling and verifying web service orchestration by means of the concurrency workbench [J]. SIGSOFT Softw Eng Notes.2004,29(5):1-10.
[2-26]G. Salaun, L. Bordeaux, M. Schaerf. Describing and Reasoning on Web Services using Process Algebra[C].2nd Inter. Conference on Web Services. IEEE,2004
[2-27]G.Diaz et al.:Automatic Translation of WS-CDL Choreographies to Timed Automata. In:Proc. WS-FM'05. Number 3670 in LNCS, Springer (2005) 230-242.
[2-28]肖庆,杨朝红,毕学军.一种基于故障模式状态机的测试方法.北京化工大学学报.Vol34,sup 1,2007,pp73-76.
[2-29]Barkaoui, K.; Eslamichalandar, M.; Kaabachi, M. A structural verification of web services composition compatibility. Proceedings of the 6th International Workshop on Enterprise & Organizational Modeling and Simulation.2010:30-41.
[2-30]http://www.uml.org.cn/Test/201003033.asp.
[2-31]徐春香,屈婉玲,王捍贫等.死路径语义下的WS-BPEL流程建模.北京大学学报(自然科学版).2010,46(2)：162-170.
[3-1]OASIS. Web Service Business Process Execution Language (WS-BPEL) [EB/OL]. [2009-12-1]. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf.
[3-2]Sun Ping, Jiang Changjun. Analysis of workflow dynamic changes based on Petri net, Information and Software Technology [J],2009,51(2):284-292.
[3-3]Mukherjee A, Tari Z and Bertok P. Modeling of BPEL Composite Services Using Clustered Coloured Petri-Nets[C]//2009 World Conference on Services-Ⅱ, Washington, USA:ACM Press,2009:55-62.
[3-4]Lucchi R, Mazzara M. A pi-calculus based semantics for WS-BPEL [J]. Journal of Logic and Algebraic Programming Web Services and Formal Methods,2007,70(1):96-118.
[3-5]Yan J, Li Z, Yu. Y, et al. BPEL4WS Unit Testing:Test Case Generation Using a Concurrent Path Analysis Approach [C]//2006 International Symposium on Software Reliability Engineering (ISSRE '06), Washington, USA:ACM Press,2006:75-84.
[3-6]宫云战.一种而向故障的软件测试新方法[J].装甲兵工程学院学报,2004(1)：21-25.
[3-7]宫云战.软件测试教程[M].北京：机械工业出版社,2006.89-134.
[3-8]杨朝红,宫云战,肖庆等.基于软件缺陷模型的测试系统[J].北京邮电大学学报,2008,31(5)：1-4.
[3-9]Huynh K. Analysis through refection:walking the EMF model of BPEL4WS.Master's thesis [D]. York University, Toronto, Canada, September 2005.
[3-10]AHO A V, SETHI R, ULLMAN J D. Compilers:prin2ciples, techniques, and tools [M]. Beijing: Posts &Telecom Press, Pearson Education,2002.608-633.
[3-11]H. Foster, S. Uchitel, J, Magee and J. Kramer, Model-based verification of web service compositions. In Proc. ASE'03,2003.
[3-12]R. Kazhamiakin and M. Pistore. Static verification of control and data inweb service compositions. IEEE International Conference on web services (ICWS'06).
[3-13]R. Kazhamiakin, M. Pistore and L.Santuari. A Parametric Communication Model for the Verification of Web Service Composition. In Proc.WWW'06,2006.
[3-14]M. Rouached and C. Godart. Requirements-driven verification of wsbpel processes[C].1CWS 2007,354-363.
[3-15]M. Rouached, O.Perrin and C. Godart. Towards Formal Verification of Web Service Composition [J]. Business Process Management 2006,257-273.
[3-16]Mariya Koshkina and Franck van Breugel "Verification of Business Process for Web Services", Technical Report, Department of Computers Science, York University, Canada, Oct 2003.
[3-17]Chun Ouyang, Eric Verbeek, Wil M.P. van der Aalst, Stephan Breutel, Marlon Dumas, Arthur H.M. ter Hofstede. Applying model checking to BPEL4WS business collaborations. In ACM Symposium on Applied Computing, pages 826-830,2005.
[3-18]Juan M. vara, Valeria De Castro, and Esperanza Marcos. WSDL automatic generation from uml models in a mda framework. In International Journal of Webservices Practices, pages 112.Web Services Research Foundation, Seoul, Korea,2005.
[3-19]David Skogan, Roy Grnmo, and Ida Solheim. "Web service composition in UML". In Proceedings of 8th International Enterprise Distributed Object Computing Conference (EDOC 2004), pages 4757, Monterey, California, USA,20-24 September 2004.
[3-20]Keith Mantell. "From UML to BPEL, model driven architecture in a web services world."IBM developer works, September 9 2003.
[3-21]XiaochuanYi and Krys J. Kochut. "A CP-net-based design and verification framework for web services composition."In Proceedings of the IEEE InternationalConference on Web Services (ICWS04), pages 756-760. IEEE,2004.
[3-22]G. J. Holzmann. The SPIN Model Checker:Primer and Reference Manual. Addison-Wesley, Boston, Massachusetts,2003.
[3-23]王勇,代桂平,侯亚荣,等.基于并发事务逻辑的web服务编制验证.电子学报.2009,37(10)：2228-2233.
[3-24]张广梅,陈蕊,李晓维.面向软件故障检测的数据流分析.全国第13届计算机辅助设计与图形学(CAD/CG)学术会议,2004,pp25 1-255.
[4-1]Monakova, G., et al.:Verifying Business Rules Using an SMT Solver for BPEL Processes. In:BPSC. (2009)
[4-2]Francisco Curbera et al. Exception Handling in the BPEL4WS Language. In Conference on Business Process Management, pages 276-290. Springer,2003.
[4-3]F.van Breygel, M.Koshkina. Dead-path-elimination in BEPL4WS. Acsd,00:192-201,2005. doi: 10.1109/ACSD.2005.11.
[4-4]A.Ferrara, Webservices:A process algebra approach, in:Proceedings of 2nd International Conference on Service Oriented Computing, ACM Press, New York, NY,USA,2004,pp.242-251.
[4-5]G. Monakova, O. Kopp, and F. Leymann, "Improving control flow verification in a business process using an extended Petri net," in ZEUS 2009:1st Central-European Workshop on Services and their Composition,2009, pp.95-101.
[4-6]Sun Ping and Jiang Changjin. Analysis of workflow dynamic changes based on Petri net, Inf. Softw. Technol,2009,51(2):284-292.
[4-7]Mukherjee A, Tari Z and Bertok P. Modeling of BPEL Composite Services Using Clustered Coloured Petri-Nets. World Conference on Services-Ⅱ,2009, pp.55-62.
[4-8]J.A. Fisteus, L.S. Fernandez, and C.D. Kloos. Formal verification of BPEL4WS business collaborations. In Proceedings of 5th International Conference on Electronic Commerce and Web Technologies (EC-Web'04),2004.8,31(80) 76-85.
[4-9]Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of Web service composition. In Proceedings of 18th IEEE International Conference on Automated Software Engineering,2003.10: 152-161.
[4-10]X. Fu. Specification and Verification of Asynchronously Communication Web Service [Ph.D. dissertation]. University of California, Santa Barbara,2004.
[4-11]雷丽晖 段振华.一种基于扩展有限自动机验证组合Web服务的方法[J].软件学报,2007,18(12)：2980-2990.
[4-12]WOMBACHER A, FANKHAUSER P, MAHLEK O B, et al.Matchmaking for business processes based on choreographies[C].Proceedings of the 2004 IEEE International Conference on E-Technology, E-Commerce and E2 Service. Washington, DC:IEEE Computer Society,2004:359-368.
[4-13]杨璐,柳溪,王林章等.面向基于场景规约的web服务消息流分析与验证.计算机学报.2009,32(9)：1759-1772.
[4-14]ZHENG YONGYAN, ZHOU JIONG, KRAUSE P. Analysis of BPEL data dependencies[C]. Proceedings of the 33rd EUROM ICRO Conference on Software Engineering and Advanced Applications. Washington, DC:IEEE Computer Society,2007:351-358.
[4-15]KHALAF R, K OPP O, LEY MANN F. Maintaining data dependencies across BPEL process fragments [J]. International Journal of Cooperative Information Systems,2008,17 (3):259-282.
[4-16]O. Kopp, R. Khalaf, and F. Leymann. Reaching Definitions Analysis Respecting Dead Path Elimination Semantics in BPEL Processes. Technical Report 2007/04, University Stuttgart, IAAS, 2007.
[4-17]O.Kopp, R.Khalaf, F.Leymann. Deriving Explicit Data Links in WS-BPEL processes. In IEEE SCC 2008:367-376
[4-18]肖庆,宫云战,杨朝红等.一种路径敏感的静态缺陷检测方法.软件学报,2010.01,21(2)：209-217.
[4-19]Das M, Lerner S, Seigle M. ESP:Path-Sensitive program verification in polynomial time. In: Knoop J, Hendren LJ, eds. Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation. New York:ACM Press,2002:57-68.
[4-20]杨朝红,宫云战,肖庆等.基于软件缺陷模型的测试系统.北京邮电大学学报.2008.10,31(5)：1-4
[4-21]C. Ouyang et,al. Formal Semantics and Analysis of Control Flow in WS-BPE. Science of computer programming, Elsevier, North-Holland,2007, vol.67, pp.162-198.
[4-22]Dong Wenli, Hu Jianhua. Test Method for BEPL-Based Web Service Composition Based on Data Flow Analysis. Journal of software,2009,20(8),467-470.
[4-23]R.Farahbod, U.Glasser, M.Vajihollahi, Abstract operational semantics of the business process execution language for Web services, Technical Report SFU-CMPT-TR-2004-03, School of Computer Science, Simon Fraser University, Burnaby B.C., Canada, April2004.
[4-24]Fu, X., Bultan, T., Su,J. Analysis of interacting BPEL web services. Proceedings of the 13th international conference on World Wide Web, WWW2004, New York, NY, USA, May 17-20,2004, ACM Press (2004) 621-630
[4-25]Shin Nakajima. Model-Checking Behavioral Specification of BPEL Applications. Electronic Notes in Theoretical Computer Science.2006,151(2):89-105.
[4-26]杨朝红,宫云战,肖庆等.基于缺陷模型的软件测试中的区间运算应用.计算机付辅助与图形设计学报,2009,20(12)：1630-1635.
[4-27]Frank Leymann and Dieter Roller. Production Workflow-Concepts and Techniques. PTR Prentice Hall,2000.
[4-28]徐春香,屈婉玲,工捍贫等.死路径语义下的WS-BPEL流程建模.北京大学学报(自然科学版).2010,46(2)：162-170.
[4-29]Ouyang Chun, Verbeek E, Aalst W M P, et al. Formal semantics and analysis of control flow in WS-BPEL.Science of Computer Programming,2007,67 (2/3):162-198.
[4-30]Aho AV, Lam MS, Sethi R, Ullman JD. Compilers Principles, Techniques, and Tools.2nd ed., New York:Addison-Wesley,2006.626-632.
[5-1]P. Baldy, H. Dicky, R. Medina, M. Morvan, and J.-F. Vilarem. "Efficient Reconstruction of the Causal Relationship in Distributed Computations". Technical Report 92-013, Laboratoired'Informatique, de Robotique et deMicroelectronique de Montpellier, France, June 1992.
[5-2]J.S. Ostroff and W.M Wonham. A temporal logic approach to real time control. In Proc.24th Conf.Decision Contr. Pages 656-657,1985.
[5-3]F. Mattern. "Virtual Time and Global States in Distributed Systems". Proc. Workshop on Parallel and Distributed Algorithms, Chateau de Bonas, Oct.1988, M. Cosnard et al. (eds.), Elsevier/North Holland, pages 215-226,1989.
[5-4]C.J. Fidge, Dynamic Analysis of Event Orderings in Message-Passing Systems, doctoral dissertation, Australian Nat'l Univ.,1989.
[5-5]SAVA GES, BURROWS S, NELSON G, et al. Eraser:a dynamic data race detect for multithreaded programs [J]. ACM Transactions on Computer Systems,1997,15(4):391-411.
[5-6]M Christiaens. "TRaDe, A topological approach to on-the-fly race detection in java programs". Proceedings of the 2001 Symposium on JavaTM Virtual Machine Research and Technology Symposium.
[5-7]L. Lamport. Time, clocks, and the ordering of events in a distributed system.Communications of the ACM,21 (7):pages 558-565,1978.
[5-8]A.D. Kshemkalyani and M.Singhal. "Characterization of Distributed Deadlocks." Tech. Report OSU-CISRC-6/90-TR15. Computer and Information Science Research Center. Ohio State Univ.,Columbus,Ohio,1990
[5-9]Reinhard Schwarz. "Detecting Causal Relationships in Distributed Computations:In Search of the Holy Grail". Report SFB 124-15/92, December 1992
[5-10]K.S. Trivedi, "Probabiliy and Satistic:with Reliability, Queuing, and Computer Science Applications", Prentice Hall, Englewood Cliffs, N.J.,1982.
[5-11]M.Raynal and A.Schiper. "The Causal Ordering Abstraction and a Simple Way to Implement it.' Tech. Report 1132, INRIA.Paris,1989.
[5-12]W. Dong, H. Yu, Y. Zhang. "Testing BPEL-based Web Service Composition Using High-level Petri Nets". Enterprise Distributed Object computing Conference, EDOC, pages 441-444,2006.
[5-13]Jianjun Cui, "DRD4BPEL:A Tool for Data Race Detection of BPEL Process," wcse, World Congress on Software Engineering, pages 200-205,2009.
[5-14]S. Nakajima, "Verification of Web Service Flows with Model-Checking Techniques", Proc. of the First International Symposium on CW'02, IEEE, pages 378-385,2002.
[5-15]The Eclipse Modeling Framework (EMF) Overview, http://help.eclipse.org/ganymede/index. jsp?topic=/org.eclipse.emf.doc/references/overview/EMF.html
[5-16]Y. Zheng, J. Zhou, and P. Krause. "An automatic test Case generation framework for web services," Journal of Software, pages 64-77,2007.
[5-17]陈胜,鲍亮,陈平等BPEL流程数据竞争和死锁检测算法研究[J].西安电子科技大学学报：自然科学版,2008,35(6)：1058-1062.
[5-18]李少东,许蕾.一种基于发生序和锁集的BPEL数据竞争静态检测方法.计算机与数字工程.2010,38(8)：6-9.
[5-19]R. H. B. Netzer, B. P. M iller. What are Race Conditions? Some Issues and Formalizations [J]. ACM Letters on Programming Languages and Systems,1992,1(1):74-88
[5-20]J. Cardoso, A. Sheth, et al. Workflow Quality of Service. In International Conference on Enterprise Integration and Modeling Technology and International Enterprise Modeling Conference, Valencia, Spain, Kluwer Publishers,2002.
[5-21]Xiu, Jia-Peng, Xu Yan-Ting, Deng Fang et.al. A Petri Net-based approach for data race detection in BPEL. Journal of China Universities of Posts and Telecommunications.2011,17(2):10-15.
[5-22]吴萍,陈意云,张建.多线程程序数据竞争的静态检测.计算机研究与发展[J],2006,43(2)：329-335.
[5-23]J. D. Choi, et al., Efficient and precise datarace detection for multithreaded object-oriented programs. ACM SIGPLAN Notices, vol.37, pp.258-269,2002.
[5-24]W. Landi. Undecidability of static analysis. ACM Letters on Programming Languages and Syatems,1992,1(4):323-337.
[5-25]C.Praun, T. Gross. Static conflict analysis for multi-threaded object-oriented programs. In:Proc. ACM SIGPLAN 2003 Conf. Programming Language Design and Implementation. New York:ACM Press,2003,115-128.
[5-26]杨书新,李淑芝,张永进.基于BPEL的流程数据竞争问题研究.计算机应用,2010,30(7)：1959-1962.
[5-27]翟岩龙,宿红毅,张晗,等.基于数据流优化的BPEL流程分割力法[J].华南理大学学报,2009,37(4)：24-30.
[6-1]Koshkina M, Breugel F. Modelling and Verifying Web Service Orchest ration by Means of the Concurrency Workbench [C]//TAV2WEB Proceedings. Portland:ACM Press,2004:1210.
[6-2]E. W. Dijkstra, "Solutions of a problem in concurrent programming control," Communications of the ACM, vol.8, p.569,1965.
[6-3]E. G. Coffman, et al., "System deadlocks," ACM Computing Surveys (CSUR), vol.3, pp.67-78, 1971.
[6-4]Flanagam C,Leino K M, Lillibridge M, et al. Extended static checking for java[C]//Proceeding of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02), 2006:234-245.
[6-5]E. Farchi, et al., Concurrent bug patterns and how to test them[C]//Proceeding of the 17th International Symposium on Parallel and Distributed Processing.[S.1]:IEEE computer Society,2003.
[6-6]Hovemeyer D, Pugh W. Finding bugs is easy [J].SIGPLAN Not,2004,39(12):92-106.
[6-7]G. Yorsh, E. Yahav, and S. Chandra. Generating Precise and Concise Procedure Summaries. In Proceedings of the 35th Annual Acm Sigplan-Sigact Symposium on Principles of Programming Languages,221-234,2008.
[6-8]S. Gulwani and A. Tiwari. Computing procedure summaries for interprocedural analysis. Programming Languages and Systems:253-267,2007.
[6-9]X. Fu, T. Bultan, J. Su. Analysis of Interacting BPEL Web Services. In International World Wide Web Conference:Proceedings of the 13th international conference on World Wide Web, pp.621-630. ACM Press, New York, NY, USA,2004.
[6-10]C. Ouyang, et al., Formal semantics and analysis of control flow in WS-BPEL. Science of Computer Programming, vol.67, pp.162-198,2007.
[6-11]N. Lohmann, P. Massuthe, C. Stahl, D. Weinberg, Analyzing interacting BPEL processes, in:S. Dustdar, J.L. Fiadeiro, A.P. Sheth (Eds.),Proceedings of the International Conference on Business Process Management, BPM 2006, Vienna, Austria, September 2006, in:Lecture Notes in Computer Science, vol.4102, Springer-Verlag,2006, pp.17-32.
[6-12]Klai, K., Tata, S., Desel, J.:Symbolic Abstraction and Deadlock-Freeness Verification of Inter-enterprise Processes. Proceedings of the 7th International Conference on Business Process Management, Lecture Notes in Computer Science Vol.5701, pp 294-309 (2009).
[6-13]Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D. Analyzing interacting WS-BPEL processes using flexible model generation. Data and Knowledge Engineering 64(1),38-54 (2008).
[6-14]Cheng Y., Wang Z.:Research on Reachability Verification of Web Service Composition. World Congress on Software Engineering, pp.233-237 (2009).
[6-15]Aalst, W.M., Mooij, A.J., Stanl, C., Wolf, K. Service Interaction:Patterns, Formalization, and Analysis. Formal Methods for Web Services, p.88 (2009).
[6-16]宋艳,高春鸣.基于移动工作台的BPEL4WS死锁验证.计算机工程,2007,33(1)：92-95.
[6-17]傅建明,韩光鹏,朱福喜.两种死锁分析的逻辑方法[J].武汉大学学报(自然科学版)1999,45(3)
[6-18]Tetsuya Maruta, Senichi Onoda, Yoshitomo lkkai, et al. A deadlock detection algorithm for business processes workflow models[C]. In:Proceedings of 1998 IEEE International Conference on Systems, Man, and Cybernetics, San Diego, CA, USA,1998, pp.611-616.
[6-19]Senichi Onoda, Yoshitomo Ikkai, Takashi Kobayashi, et al. Definition of deadlock patterns for business processes work on models[C]. In:Proceedings of the Annual Hawaii International Conference on System Sciences, Maui, Hawaii,1999, pp.1-4.
[6-20]Ezpeleta J, Colom J M, and Martinez J. A Petri net based deadlock prevention policy for flexible manufacturing systems [J]. IEEE Transaction on Robotics and Automation,11(2),1995, pp.173-184.
[6-21]陈胜,鲍亮,陈平等BPEL流程数据竞争和死锁检测算法研究[J].西安电子科技大学学报,35(6),2008,pp.1056-1063.
[6-22]J. A. Fisteus, et al., Formal verification of BPEL4WS business collaborations, E-Commerce and Web Technologies, pp.123-131,2004.
[6-23]Tasharofi, S., Vakilian, M., Moghaddam, R.Z., Sirjani, M.:Modeling web service interactions using the coordination language Reo. In:Proc. of the Int. Workshop on Web Services and Formal Methods. Volume 4937 of LNCS. Springer (2008) 108-123.
[6-24]R.J. van Glabbeek, D.G. Stork, Query nets:interacting workflow modules that ensure global termination, in:W.M.P. van der Aalst, A.H.M. ter Hofstede, M. Weske (Eds.), International Conference on Business Process Management (BPM 2003), Lecture Notes in Computer Science, vol. 2678, Springer-Verlag, Berlin,2003, pp.184-199.
[6-25]G. Decker and J. Mendling, "Instantiation semantics for process models," Business Process Management, pp.164-179,2008.
[6-26]PTimothy Mark Pinkston, Sugath Warnakulasuriya,On deadlocks in interconnection networks. ACM SIGARCH Computer Architecture News,1997,25(2):38-49.