基于赋时有色Petri网的Web服务组合建模验证与测试技术研究
|
摘要
Web服务（Web Service）是一种自包含、自描述、模块化的应用程序，它吸收了分布式计算、网格计算和XML等各种技术的优点，解决了异构分布式计算以及代码与数据重用等问题，具有高度的互操作性、跨平台性和松耦合性，已经在电子商务、企业应用集成等领域发挥着重要作用，特别是Web服务组合技术，因其能实现服务的重用和增值而引起了世界范围内学术界和工业界的关注。
Web服务组合本身是一项易于产生错误的任务，因为在组合中候选的服务之间进行复杂的交互。Web服务业务流程执行语言(Web Service Business ProcessExecution Language，WS-BPEL，简称BPEL)用于实现Web服务的组合和合并，它建立在IBM的Web服务流语言（Web Services Flow Language，WSFL）和Microsoft的XML业务流程语言（XML Business Process Language，XLANG）之上，结合了这两种语言的特性，这样就引起了某些方面的不一致和语义的模糊；BPEL的语义是用英语定义的，这样无法避免其二义性、模糊性和不完全性。WS-BPEL技术委员会公认为需要对BPEL语义给出形式化定义。
由于要处理并发，具有复杂特性，如补偿处理、相关性、死路径删除（Dead-Path-Elimination，DPE）等，BPEL过程是容易出错的。
本文主要研究由BPEL生成的Web服务组合流程的建模、验证、测试问题。
针对BPEL流程建模，目前采用的方法有Petri网、SPIN工具、进程代数、抽象状态机和自动机等方法。本文采用赋时有色Petri网对BPEL流程建模。首先对BPEL的各种活动建模，将BPEL流程看作是活动的嵌套，将嵌套关系对应于层次化有色Petri网的层次关系缓解了有色Petri网模型过于庞大以及状态爆炸问题。本文提出的层次化有色Petri网的展开算法，使层次化Petri网可以展开成等价的非层次化Petri网，能够呈现出模型的细节。本文还完善了层次化有色Petri网的定义。
Web服务的形式化验证是近年来才开始进入研究领域的，但是已经获得了很多研究人员的关注。针对BPEL模型验证，本文给出了利用有色Petri网的属性对BPEL流程的基本属性进行验证，使用扩展时态逻辑ASK-CTL来描述要验证的属性，对模型的动态属性进行验证的一种方法。为了处理程序验证过程中出现的状态爆炸问题，本文还对谓词抽象技术和惰性抽象技术进行了研究，将CP-nets的状态图生成过程，以及状态图的谓词抽象过程合为一体，在状态生成过程中形成抽象状态图，从而避免了状态爆炸问题。本文将惰性抽象用于BPEL流程的安全性验证方法CEGAR中，优化了“抽象-验证-反例”中的前两个步骤，使得这个方法可以用于规模较大的程序上。
Web服务为分布式计算提供了灵活的、可重用的、松散耦合的模型，BPEL是半形式化的、具有复杂特性的、易含有错误行为的语言。在Web服务发布之前对服务进行验证、测试，确认服务符合设计模型是必需的。本文针对BPEL流程的CP-nets模型，提出了模型的可执行程序单元概念，基于可执行程序单元，给出了BPEL程序的测试用例生成方法，该方法可以有效的处理BPEL的并发、DPE等特性。
Web service is a kind of application which is self-contained, self-description andmodularization. It got various advantages from Distributed Computing, Grid Compute,XML and other technologies. It has solved some problems on heterogeneous distributedcompute, code and data reuse. It is interoperation, independent of platforms, and looselycoupled. It has played an important role in a variety of domains including electricbusiness and enterprise application integration. Especially, Web service compositiontechnology has got great focus in academia and industry over the world, due to itsimplementation of service reusing and service increment.
Web service composition is a task prone to errors, because its candidate servicestake complex interactions within it. Web Service Business Process Execution Language(WS-BPEL, BPEL) implements the composition and integration of web services. BPELbuilds on IBM’s WSFL and Microsoft’s XLANG and combines the features of bothlanguages, which lead to some inconsistencies and semantic ambiguities. Like mostlanguages, the semantics of BPEL is defined in English prose. Although oftenmasterpieces of apparent clarity, such descriptions usually suffer from inconsistency,ambiguity and incompleteness. The WSBPEL TC recognized the need for a formalismto define the semantics of BPEL.
With complex features, such as compensation, correlation,DPE(Dead-Path-Elimination，DPE) and concurrence, Process coded in BPEL is errorprone.
The main research work of this thesis is modeling, verification, and test Webservice composition process coded in BPEL.
Some approaches have applied to BPEL process model, such as Petri nets, SPINtool, process algebras, abstract state machines and automata, et al. This theise presentsan approach to model Web services composition based on transformation from BPEL toTimed colored Petri net (TCP-net). Each BPEL’s activity is modeled using a TCP-net.A BPEL process is regard as an activity which embedded some activities hierarchically.This hierarchical relation is mapped into TCP-net’s hierarchy.
The normal Petri net was applied to model BPEL process in some literatures. Theexperience shows the model is usually on a large scale and result in state explosion.Modeling BPEL process by hierarchical TCP-net can relieve some problems on scaleand state explosion.
An algorithm to unfold a hierarchical CP-net into equivalence un-hierarchicalCP-net is presented in this thesis. Any hierarchical CP-net has an equivalenceun-hierarchical CP-net with respect to their behaviors. But the equivalenceun-hierarchical CP-net exposes more details of the model. Also, the formal definition ofhierarchical CP-net proposed by K. Jensen is improved in this thesis..
The formal verification of Web services came into research field in recent years,but it has obtained great attention. An approach is proposed in this thesis for modelchecking. The BPEL’s basic properties are verified by checking corresponding CP-net’sbasic properties. Dynamic properties are represented in a CTL-like temporal logic calledASK-CTL. The logic is an extension of CTL which is branch time logic. Such thedynamic properties are verified in this form. In order to solve the state space explosion,predicate abstract and lazy abstract are discussed in this thesis. The CP-nets state spacegeneration and the predicate abstract of the state space are integrated together. Duringthe state space generation, a reduced state space by predicate abstract are calculatedavoiding state space explosion. Lazy abstract applied to CEGAR approach to verifysafety property of BPEL process, which the first two steps of“abstract-verify-counterexample” optimized. This approach can be applied to large scaleprogram.
Web services provide loose coupled models with flexibility and usability fordistributed compute. BPEL is a self-formal language with complex features and errorprone. Before a Web service released, verification and testing is require to confirm itsconsistence to the design model. The concept of execute program units is introduced forCP-nets models. Based on execute program units, a new test case generation method isgiven, in which concurrence and DPE features considered properly, as well as otherfeatures.
Web服务组合本身是一项易于产生错误的任务，因为在组合中候选的服务之间进行复杂的交互。Web服务业务流程执行语言(Web Service Business ProcessExecution Language，WS-BPEL，简称BPEL)用于实现Web服务的组合和合并，它建立在IBM的Web服务流语言（Web Services Flow Language，WSFL）和Microsoft的XML业务流程语言（XML Business Process Language，XLANG）之上，结合了这两种语言的特性，这样就引起了某些方面的不一致和语义的模糊；BPEL的语义是用英语定义的，这样无法避免其二义性、模糊性和不完全性。WS-BPEL技术委员会公认为需要对BPEL语义给出形式化定义。
由于要处理并发，具有复杂特性，如补偿处理、相关性、死路径删除（Dead-Path-Elimination，DPE）等，BPEL过程是容易出错的。
本文主要研究由BPEL生成的Web服务组合流程的建模、验证、测试问题。
针对BPEL流程建模，目前采用的方法有Petri网、SPIN工具、进程代数、抽象状态机和自动机等方法。本文采用赋时有色Petri网对BPEL流程建模。首先对BPEL的各种活动建模，将BPEL流程看作是活动的嵌套，将嵌套关系对应于层次化有色Petri网的层次关系缓解了有色Petri网模型过于庞大以及状态爆炸问题。本文提出的层次化有色Petri网的展开算法，使层次化Petri网可以展开成等价的非层次化Petri网，能够呈现出模型的细节。本文还完善了层次化有色Petri网的定义。
Web服务的形式化验证是近年来才开始进入研究领域的，但是已经获得了很多研究人员的关注。针对BPEL模型验证，本文给出了利用有色Petri网的属性对BPEL流程的基本属性进行验证，使用扩展时态逻辑ASK-CTL来描述要验证的属性，对模型的动态属性进行验证的一种方法。为了处理程序验证过程中出现的状态爆炸问题，本文还对谓词抽象技术和惰性抽象技术进行了研究，将CP-nets的状态图生成过程，以及状态图的谓词抽象过程合为一体，在状态生成过程中形成抽象状态图，从而避免了状态爆炸问题。本文将惰性抽象用于BPEL流程的安全性验证方法CEGAR中，优化了“抽象-验证-反例”中的前两个步骤，使得这个方法可以用于规模较大的程序上。
Web服务为分布式计算提供了灵活的、可重用的、松散耦合的模型，BPEL是半形式化的、具有复杂特性的、易含有错误行为的语言。在Web服务发布之前对服务进行验证、测试，确认服务符合设计模型是必需的。本文针对BPEL流程的CP-nets模型，提出了模型的可执行程序单元概念，基于可执行程序单元，给出了BPEL程序的测试用例生成方法，该方法可以有效的处理BPEL的并发、DPE等特性。
Web service is a kind of application which is self-contained, self-description andmodularization. It got various advantages from Distributed Computing, Grid Compute,XML and other technologies. It has solved some problems on heterogeneous distributedcompute, code and data reuse. It is interoperation, independent of platforms, and looselycoupled. It has played an important role in a variety of domains including electricbusiness and enterprise application integration. Especially, Web service compositiontechnology has got great focus in academia and industry over the world, due to itsimplementation of service reusing and service increment.
Web service composition is a task prone to errors, because its candidate servicestake complex interactions within it. Web Service Business Process Execution Language(WS-BPEL, BPEL) implements the composition and integration of web services. BPELbuilds on IBM’s WSFL and Microsoft’s XLANG and combines the features of bothlanguages, which lead to some inconsistencies and semantic ambiguities. Like mostlanguages, the semantics of BPEL is defined in English prose. Although oftenmasterpieces of apparent clarity, such descriptions usually suffer from inconsistency,ambiguity and incompleteness. The WSBPEL TC recognized the need for a formalismto define the semantics of BPEL.
With complex features, such as compensation, correlation,DPE(Dead-Path-Elimination，DPE) and concurrence, Process coded in BPEL is errorprone.
The main research work of this thesis is modeling, verification, and test Webservice composition process coded in BPEL.
Some approaches have applied to BPEL process model, such as Petri nets, SPINtool, process algebras, abstract state machines and automata, et al. This theise presentsan approach to model Web services composition based on transformation from BPEL toTimed colored Petri net (TCP-net). Each BPEL’s activity is modeled using a TCP-net.A BPEL process is regard as an activity which embedded some activities hierarchically.This hierarchical relation is mapped into TCP-net’s hierarchy.
The normal Petri net was applied to model BPEL process in some literatures. Theexperience shows the model is usually on a large scale and result in state explosion.Modeling BPEL process by hierarchical TCP-net can relieve some problems on scaleand state explosion.
An algorithm to unfold a hierarchical CP-net into equivalence un-hierarchicalCP-net is presented in this thesis. Any hierarchical CP-net has an equivalenceun-hierarchical CP-net with respect to their behaviors. But the equivalenceun-hierarchical CP-net exposes more details of the model. Also, the formal definition ofhierarchical CP-net proposed by K. Jensen is improved in this thesis..
The formal verification of Web services came into research field in recent years,but it has obtained great attention. An approach is proposed in this thesis for modelchecking. The BPEL’s basic properties are verified by checking corresponding CP-net’sbasic properties. Dynamic properties are represented in a CTL-like temporal logic calledASK-CTL. The logic is an extension of CTL which is branch time logic. Such thedynamic properties are verified in this form. In order to solve the state space explosion,predicate abstract and lazy abstract are discussed in this thesis. The CP-nets state spacegeneration and the predicate abstract of the state space are integrated together. Duringthe state space generation, a reduced state space by predicate abstract are calculatedavoiding state space explosion. Lazy abstract applied to CEGAR approach to verifysafety property of BPEL process, which the first two steps of“abstract-verify-counterexample” optimized. This approach can be applied to large scaleprogram.
Web services provide loose coupled models with flexibility and usability fordistributed compute. BPEL is a self-formal language with complex features and errorprone. Before a Web service released, verification and testing is require to confirm itsconsistence to the design model. The concept of execute program units is introduced forCP-nets models. Based on execute program units, a new test case generation method isgiven, in which concurrence and DPE features considered properly, as well as otherfeatures.
引文
[1] G. Caprio. An Introduction to Service-Oriented Architecture.URL http://www.devx.com/codemag/Article/28254. June8,2005.
[2] H. B. Zhu. Building Reusable Components with Service-Oriented Architectures.Proceedings of2005IEEE International Conference on Information Reuse andIntegration (IEEE IRI-2005). Las Vegas, Nevada, USA: August2005,pages96-101.
[3] L.Roger, H. Ashok, and C. Chia-Chu et al. A framework for dynamicallyconverting components to web services. Proceeding of SERA'05.2005,pages431-437
[4] E. Cerami. Web Service Essentials:Dsitributed Applications with XML-RPC,SOAP, UDDI&WSDL. O’Reilly&Associates,Inc.2002
[5] WSDL:Web Service Definition Language1.1.URL http://www.w3.org/TR/uddi.
[6] SOAP. Simple Object Access Protlcol(SOAP1.1).URL http://www.w3.org/TR/SOAP.
[7] Web Services Glossary. W3C Working Group Note. February11,2004. URLhttp://www.w3.org/TR/2004/NOTE-ws-gloss-20040211/. Retrieved2011-04-22.
[8] UDDI.Universal Description,Discovery and Integeration2.0.URL http://www. w3.org/TR/wsdl.
[9] OASIS. Web Services Business Process Execution Language Version2.0. URLhttp://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.pdf.2008.
[10]吕毅.形式化方法综述—基本概念、技术源流和典型应用.技术报告,2003
[11] W. M. P. van der Aalst (Editor), Boualem Benatallah (Editor), and Fabio Casati(Editor), et.al.. Proceedings of the3rd International Conference on BusinessProcess Management,volume3649of Lecture Notes in Computer Science.Nancy,France: Springer-Verlag, September,2005.
[12]. Desel (Editor), B. Pernici (Editor), and M. Weske (Editor). Proceedings of the2nd International Conference on Business Process Management, volume3080ofLecture Notes in Computer Science. Potsdam, Germany: Springer-Verlag, June2004.
[13] W. M. P. van der Aalst (Editor), A. ter Hofstede (Editor), and M. Weske (Editor).Proceedings of the International Conference on Business ProcessManagement,volume2678of Lecture Notes in Computer Science. Eindhoven,Netherlands: Springer-Verlag, June2003.
[14] IEEE Computer Society. Proceedings of the2005IEEE InternationalConference on Web Services. Orlando, Florid, USA:2005.
[15] IEEE Computer Society. Proceedings of the2nd IEEE International Conferenceon Web Services. San Diego, California, USA:2004.
[16] IEEE Computer Society. Proceedings of the International Conference on WebServices. Las Vegas, NV, USA: CSREA Press,June2003.
[17] M. Bravetti, G. Zavattaro. Proceedings of the2nd International Workshop onWeb Services and Formal Methods, Volume3670of Lecture Notes in ComputerScience. Versailles, France: Sringer-Verlag, September2005..
[18] M. Bravetti, G. Zavattaro. Proceedings of the1st International Workshop onWeb Services and Formal Methods, volume105of Electronic Notes inTheoretical Computer Science. Pisa, Italy: Elsevier, February2004.
[19] F. van Breugel, M. Koshkina. Models and Verification of BPEL.http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf. September2006.
[20] K. Xu, Y. Liu, and G. G. Pu. Formalization, Verification and Restructuring ofBPEL Models with Pi Calculus and Model Checking. Research Report,RC-23962, IBM Thomas J. Watson Research Center, Yorktown Heights, NY10598(2006).
[21] Y. Liu, S. Müller, K. Xu. A static compliance-checking framework for businessprocess models. IBM SYSTEM JOURNAL, Vol46, No2.2007.
[22] T. He, H. K. Miao, Z. S. Gian. Analysis and modeling of web services flowusing Π-calculus. Journal of Southeast University (English Edition). March2006,Vol22(3), Pages315-318.
[23]高春鸣,黄邵,陈火旺. Web服务组合语言的出错与补偿处理的Pi演算编码.计算机工程与科学.2007，03，Vol29(3)，pages112-116.
[24] G. Salaun, A. Ferrara, and A. Chirichiello. Negotiation among web servicesusing LOTOS/CADP. In European conference on web services. September2004.
[25] G. Salaun, L. Bordeaux, and M. Schaerf. Describing and Reasoning on WebServices using Process Algebra. In IEEE International Conference on WebService (ICWS04).2004.
[26] M. Kovács, L. G nczy. Simulation and Formal Analysis of Workflow Models.Proceedings of the5th International Workshop on Graph Transformation andVisual Modeling Techniques, Vienna, Austria,2006.pages215-224.
[27] R. Gerth. Concise Promela Reference. Technical report, Eindhoven University,June1997.
[28] G. J. Holzmann. The Spin Model Checker, Primer and Reference Manual.Technical report, Addison-Wesley, Boston, MA, USA,2004.
[29] M. Mongiello, D. Castelluccia. Modelling and verification of BPEL businessprocesses. Proceedings of the Fourth Workshop on Model-Based Developmentof Computer-Based Systems and Third International Workshop on Model-BasedMethodologies for Pervasive and Embedded Software (MBD-MOMPES'06)-Vol00,2006.IEEE.
[30] S. Nakajima. Lightweight Formal Analysis of Web Service Flows. In Progressin Informatics, No.2, November2005.
[31] S. Nakajima. Model-Checking Behavioral Specifications of BPEL Applications.In WLFM’05, July2005.
[32] X. Fu, T. Bultan, and J. W. Su. Analysis of interacting BPEL web services.Proceedings of the13th International World Wide Web Conference, New York,NY, USA, May2004. ACM.pages621-630,
[33] X. Fu, T. Bultan, and J. W. Su. Synchronizability of conversations among webservices. IEEE Transactions on Software Engineering, December2005,Vol31(12), pages:1042-1055,
[34] M. Pistore, P. Traverso, and P. Bertoli et.al. Automated Synthesis of CompositeBPEL4WS Web Services. Proceedings of ICWS.2005, pages293-301.
[35] R. Kazhamiakin, M. Pistore. A Parametric Communication Model for theVerification of BPEL4WS Compositions. Proceedings of EPEW/WS-FM.2005.pages318-332
[36] R. Farahbod, R. Glsser, and M. Vajihollahi. A formal semantic for the BusinessProcess Execution Language for Web Services. In Web Services andModel-Driven Enterprise Information Services. May2005.
[37] D. Fahland. Complete Abstract Operational Semantics for the Web ServiceBusiness Process Execution Language. Technical report, Humboldt-Universit tzu Berlin, Institut für Informatik,Germany,2005.
[38] T. Bultan, X. Fu, and R. Hull et al. Conversation Specification: A NewApproach to Design and Analysis of E-Service Composition. Proceeding ofTwelfth International World Wide Web Conference (WWW2003).2003.
[39] H. Foster. A Rigorous Approach To Engineering Web Service Compositions.PhD thesis, Imperial College London, University Of London, January2006.
[40] H. Foster, S. Uchitel, and Magee et al. Model-based verification of Web servicecomposition. Proceedings of18th IEEE International Conference on AutomatedSoftware Engineering. Montreal, Canada: October2003, pages152-161.
[41] M. Simon, M. Axel, and H. Marc et al. Approach for Generating CompatibleWS-BPEL Partner Processes. Proceedings of the4th International Conferenceon Business Process Management. Vienna:September2006.
[42] X. P. Zhao, C. Antonio, and K. Padmanabhan. Verifying BPEL WorkflowsUnder Authorisation Containts. Proceedings of the4th InternationalConference on Business Process Management. Vienna: September2006.
[43] D. Karastoyanova, F. Leymann, J. Nitzsche et al. Parameterized BPELProcesses: Concepts and Implementation. Proceedings of the4th InternationalConference on Business Process Management. Vienna: September2006.pages471-476.
[44] S. Wang, J. Wan, and X. Yang. Describing, Verifying and Developing WebService Using the B-method. In International Conference on Next GenerationWeb Services Practices (NWeSP’06).2006.
[45] J. R. Abrial. The B-Book:Assigningprogramsto meanings. CambridgeUniversity Press.1996.
[46] K. Schmidt and C. Stahl. A Petri net semantic for BPEL4WS validation andapplication. Proceedings of the11th Workshop on Algorithms and Tools for PetriNets. Paderborn, Germany:September/October2004. pages1-6,
[47] C. Stahl. Transformation von BPEL4WS in Petrinetze. Master's thesis,Humboldt Universit at zu Berlin, Berlin, Germany, April2004.
[48] C. Stah. A Petri Net Semantics for BPEL. Technical Report188, HumboldtUniversit t zu Berlin, Institut für Informatik.2005.
[49] N. Lohmann, P. Massuthe, C. Stahl et al. Analyzing Interacting BPEL Processes.Proceedings of the4th International Conference on Business ProcessManagement. Vienna, Austria: September,2006.
[50] N. Lohmann. A Feature-Complete Petri Net Semantics or WS-BPEL2.0. In WebServices and Formal Methods International Workshop (WSFM07).2007.pages77–91.
[51] G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual.Addison-Wesley, Boston, MA, USA:2004.
[52] K. Schmidt. LoLA-a low level analyser. Proceedings of the21st InternationalConference on Application and Theory of Petri Nets, volume1825of LectureNotes in Computer Science. Aarhus, Denmark: Springer-Verlag, June2000,pages465-474.
[53] W. M. P. van der Aalst, M. Dumas, and C. Ouyang et al. ChoreographyConformance hecking: An Approach based on BPEL and Petri Nets. Proceedingsof the4th International Conference on Business Process Management, Vienna,Austria: September,2006.
[54] C. Ouyang, E. Verbeek, and W. M. P. Van der Aalst et al. Formal semantics andanalysis of control flow in WS-BPEL. Science of Computer Programmingarchive. July2007, Vol67(2-3), pages162-198
[55] R. Farahbod, U. Glsser, and M. Vajihollahi. A formal semantics for the BusinessProcess Execution Language for Web Services. In Web Services andModel-Driven Enterprise Information Services. May2005.
[56] H. Verbeek, W. M. P. Van der Aalst. Analyzing BPEL processes usingPetri-Nets. In Second International Workshop on Application of Petri-Nets toCoordination Workflow and Business Process Management. October2005.
[57] H. Kang, X. L. Yang, and S. M. Yuan. Modeling and Verification of WebServices Composition based on CPNIssue.2007IFIP International Conferenceon Network and Parallel Computing Workshops (NPC2007). September2007,pages613-617.
[57] Y. Yang, Q. Tan, and Y. Xiao. Verifying web services composition. InProceedings of the ER2005Workshops, Vol3770of Lecture Notes in ComputerScience. Klagenfurt, Austria: Springer Verlag, October2005. pages354-363,.
[59] Y. Yang, Q. Tan, and Y. Xiao et al. Exploiting hierarchical CP-netss to increasereliability of web services workflow. Proceeding of the International Symposiumon Applications and the Internet. Phoeniz, AZ, USA:January2006.pages116-122.
[60] Y. Yang, Q. Tan, and Y. Xiao et al. Verifying web services composition:Atransformation-based approach. Proceedings of the6th International Conferenceon Parallel and Distributed Computing. Dalian, China: December2005,pages546-548.
[61] Y. Yang, Q. Tan, and Y. Xiao. Verifying web services composition based onhierarchical colored Petri nets. Proceedings of the1st International Workshop onInteroperability of Heterogeneous Information Systems. Bremen, Germany:November2005, pages47-54.
[62] X. Yi and K. J. Kochut. Process composition of web services with complexconversation protocols: a colored Petri nets based approach. Proceedings of theDesign, Analysis, and Simulation of Distributed Systems Symposium. Arlington,VA, USA: April2004, pages141-148,.
[63] S. Thatte. XLANG: Web Services for Business Process Design. MicrosoftCorporation. URLhttp://www.gotdotnet.com/team/xml_wsspecs/xlang-c/default.htm.2001.
[64] F. Leymann. Web Services Flow Language (WSFL1.0). IBM Corporation, May2001. URLhttp://www-4.ibm.com/software/solutions/webservices/pdf/WSFL.pdf
[65] F. Curbera, Y. Goland, and J. Klein et al. Business process execution languagefor web services, version1.0. July2002.
[66] T. Murat. Petri nets: Properties, analysis and applications. Proceedings of theIEEE,1989,Vol77(4),541–580.
[67] K. Jensen, L. M. Kristensen, and L. Wells. Coloured Petri Nets and CPN Toolsfor Modelling and Validation of Concurrent Systems. International Journal onSoftware Tools for Technology Transfer. Springer Verlag, September2007,pages213-254
[68] V. M. P. Van der Aalst. The Application of Petri Nets to Workflow Management.Journal of Circuits, Systems and Computers.1998, vol8(1),. pages21-66.
[69] K. Jensen. An Introduction to the Theoretical Aspects of Coloured Petri Nets.A Decade of Concurrency, Lecture Notes in Computer Science. Springer-Verlag,1994, Vol803, pages230-272.
[70] J. L. Peterson. Petri Net Theory and the Modeling of Systems. Prentice-HallInternational,1981.
[71] X. Yi, J. K. Krys. A Framework for Web Services Composition Design andVerification. UGA Computer Science Technical Report, UGA-CS-TR-04-001.URL http://www.cs.uga.edu/~xyi/tr04001.pdf
[72] S. Chatterjee, J. Webber. Developing Enterprise Web Services:An Architect’sGuide. Prentice Hall,2004.
[73] CP-nets tools. URL http://www.daimi.au.dk/CP-netstools/
[74] T. Suzuki, S. M. Shatz, and T. A. Murata. Protocol Modeling and VerificationApproach Based on a Specification Language and Petri Nets.1990, vol16(5),pages523-536.
[75] J. Billington, M. Diaz, and G. Rozenberg(eds.). Application of Petri nets tocommunication networks: advances in Petri nets. Lecture Notes in ComputerScience. Springer,1999.
[76] L. D. Silva, A. Perkusich. A model-based approach to formal specification andverification of embedded systems using coloured petri nets. Component-BasedSoftware Development for Embedded Systems. Springer Berlin Heidelberg:2005, vol3778, pages35-58.
[77] K. Jensen. Computer verification tool: Colored Petri nets.URL http://wiki.daimi.au.dk/cpntools.2010-10-01
[78] A. W. Appel, D. B. Macqueen. Standard ML of New Jersey. In3rd InternationalSymposium on Programming Language Implementation and LogicProgramming. New York, USA. Vol.528of Lecture Notes in Computer Science.Springer-Verlag.1991.
[79] S. Narayanan, S. McIlraith. Analysis and simulation of Web services, ComputerNetworks.2003, Vol.42, pages675-693.
[80] URL http://wiki.daimi.au.dk/cpntools-help/.2008-11-24
[81] Fehling, A. Rainer Concept of Hierarchical Petri Nets with Building Blocks. the12th International Conference on Application and Theory of Petri Nets.1991.
[82]郝克刚,葛玮.关于高级网系统的等价及谱系的研究.计算机学报.1993年第7期.
[83]郝克刚,丁剑洁.层次结构的Petri网.计算机科学与探索.2008,vol2(2).
[84] K. Jense. Coloured Petri Nets. Basic Concepts, Analysis Methods and PracticalUse. Vol.1: Basic Concepts. EATCS Monographs on Theoretical ComputerScience. Springer-Verlag,1992.
[85] N. Lohmann, H. Verbeek, C. Ouyang et al. Comparing and evaluating Petri netsemantics for BPEL. Computer Science Report07/23, Eindhoven University ofTechnology, Eindhoven, The Netherlands (2007)
[86] E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press,Cambridge, MA, USA:1999.
[87]林惠民,张文辉.模型检测：理论、方法与应用.电子学报.2002, Vol12(3),pages1906-912.
[88] A. Cheng A, S. Christensen, K. H. Mortensen. Model checking colored Petrinets exploiting strongly connected components. Proceeding of the InternationalWorkshop on Discrete Event Systems. Edinburgh, Scotland, UK:1996,pages169-177.
[89] P. Colin, Stirling. Modal and temporal logics for processes. Technical report,Department of Computer Science, University of Edinburgh. August1993.
[90] M. Hut, M. Ryan. Logic in Computer Science.北京:机械工业出版社,2005
[91] J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. InPLDI02: Programming Language Design and Implementation. ACM:2002.pages1-12.
[92] M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification inpolynomial time. In PLDI02: Programming Language Design andImplementation. ACM:2002, pages57-68.
[93] R. Alur, A. Itai, and R. P. Kurshan et al. Timing verification by successiveapproximation. Information and Computation.1995, vol118(1), pages:142-157.
[94] T. Ball, S. K. Rajamani. Automatically validating temporal safety properties ofinterfaces. In SPIN2001: SPIN Workshop, LNCS2057,. Springer-Verlag,2001.pages103-122.
[95] H. Saidi Model checking guided abstraction and analysis. In SAS00:Static-Analysis Symposium. LNCS1824, Springer-Verlag,2000. pages377-396.
[96] E. Clarke, O. Grumberg, and S. Jha et al. Counterexample-guided abstractionrefinement. In CAV00: Computer Aided Verification, LNCS1855,Springer-Verlag,2000, pages154-169.
[97] S. Graf, H. Saidi. Construction of abstract state graphs with PVS. Proceedingsof the9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel,June1997, pages7283.
[98] S. Das. Predicate Abstraction. Ph.D. Thesis.Department of ElectricalEngineering, Stanford University, December2003.
[99] E. M. Clarke, O. Grumberg O, and D. E. Long. Model checking and abstraction.ACM Transactions on Programming Languages and Systems.1994, Vol16(5),pages1512–1542.
[100] L. M. Kristensen. State Space Methods for Coloured Petri Nets. Department ofComputer Science, University of Aarhus, Denmark,2000.
[101] T. A. Henzinger, R. Jhala, and R. Majumdar. Lazy abstraction. Proceeding of theACM Sympsium on Principles of Programming Languages. Oregon: ACM Press,2002, pages5870.
[102] R. Jhala. Program Verification by Lazy Abstraction. Ph.D. Thesis. Departmentof Computer Science, University of California Berkeley, Fall2004
[103] H. J. Genrich, K. Lautenbach. System Modeling with High Level Petri Nets.Theoretical Compoter Science.1981, Vol13.
[104] P. Huber, A. M. Jensen, and L. O. Jepsen et al. Reachability Trees for HighLevel Petri Nets. Theoretical Computer Science.1986, vol45(3).
[105] R. N. Taylor, D. L. Levine, and C. D. Kelly. Structural testing of concurrentprograms. IEEE Transactions on Software Engineering. March,1992, vol18(3),pages206–215.
[106] J. Cardoso. Complexity Analysis of BPEL Web Processes. Software Process:Improvement and Practice Journal.2006, vol12, pages35–49.
[107] J. Thomas. McCabe. A Complexity Measure. IEEE Transaction on SoftwareEngineering, SE-2(4).1976, pages308–320.
[108] W. Michael, Whalen, A. Rajan et al. Coverage metrics for requirements-basedtesting. In ISSTA’06: Proceedings of the2006international symposium onSoftware testing and analysis. New York, NY, USA: ACM Press,2006,pages25–36.
[109] J. R. Horgan and S. London. Data flow coverage and the C language. In TAV4:Proceedings of the symposium on Testing, analysis, and verification, New York,NY, USA: ACM Press,1991, pages87–97.
[110] J. Garca-Fanjul, J. Tuya, and C. De la Riva. Generating Test Cases Specicationsfor BPEL Compositions of Web Services Using SPIN. In InternationalWorkshop on Web Services Modeling and Testing (WS-MaTe2006).2006.
[111] L. Mei, W. K. Chan, and T. H. Tse. Data Flow Testing of Service-OrientedWorkflow Applications. Proceedings of the30th International Conference onSoftware Engineering (ICSE2008), New York, NY, USA: ACM,2008,pages371–380.
[112] J. Yan, Z. Li, Y. Yuan et al. BPEL4WS Unit Testing: Test Case Generation Usinga Concurrent Path Analysis Approach. In17th International Symposium onSoftware Reliability Engineering (ISSRE’06). IEEE,2006.
[113] D. L¨ubke and A. Salnikow. Definition and Formalization of BPEL Process TestCoverage. Technical report, Leibniz Universit¨at Hannover, FG SoftwareEngineering. URL http://www.se.uni-hannover.de/techreports/2009-01DefinitionAndFormalizationOfBpelProcessTestCoverage.pdf,2008.
[114] D. Lubke, L. Singer, A. Salnikow. Calculating BPEL Test Coverage throughInstrumentation. Proceedings of the4th International Workshop on Automationof Software Test, AST2009, Vancouver, BC, Canada: May2009.
[115] M. Phili. BPELUnit. URL http://www.bpelunit.org.2007-09-01.
[116] R. D. Yang and C. G. Chung. A path analysis approach to concurrent programtesting. Information and Software Technology.1992, Vol34(1), pages43–56.
[117] L. Mei, W. K. Chan, and T. H. Tse. Data Flow Testing of Service-OrientedWorkflow Applications. Proceedings of the30th International Conference onSoftware Engineering (ICSE2008), New York, NY, USA: ACM,2008,pages371–380,
[118] IEEE standard glossary of software engineering terminology, IEEE Std610.12-1990, September1990.
[119] Y. Yuan, Z. Li, and W. Sun. A Graph-Search Based Approach to BPEL4WS TestGeneration. International Conference on Software Engineering Advances.2006.
[120] Z. J. Li, H. F. Tan, H. H. Liu et al. Business-process-driven gray-box SOAtesting. IBM Systems Journal.2008, Vol47, pages457-472.
[121] C. H. Liu, S. L. Chen, and X. Y. Li. A WS-BPEL Based Structural TestingApproach for Web Service Compositions. IEEE International Symposium onService-Oriented System Engineering (SOSE '08).2008.
[122] R. Blanco, J. Garcia-Fanjul, and J. Tuya. A First Approach to Test CaseGeneration for BPEL Compositions of Web Services Using Scatter Search.International Conference on Software Testing, Verification and ValidationWorkshops (ICSTW '09).2009.
[123] A. T. Endo, A. D. Simao, S. Souza et al. Web Services Composition Testing: AStrategy Based on Structural Testing of Parallel Programs. Testing: Academic&Industrial Conference Practice and Research Techniques (TAIC PART '08).2008.
[124] Z. Li, W, Sun, Z. B. Jiang et al. BPEL4WS unit testing: framework andimplementation. Proceedings of the IEEE International Conference on WebServices (ICWS2005).2005.
[125] M. Staples, M. Niazi. Experiences using systematic review guidelines. Journalof Systems and Software.2007, Vol80, pages1425-1437.
[126] J. J. Domínguez-Jiménez, A. Estero-Botaro, and I. Medina-Bulo. A Frameworkfor Mutant Genetic Generation for WSBPEL. in SOFSEM2009: Theory andPractice of Computer Science,2009. pages229-240.
[127] J. Zhang, X. Wang. A constraint solver and its application to path feasibilityanalysis. International Journal of Software Engineering&KnowledgeEngineering.2001. Vol11(2), pages139–156.
[128] URL http://en.wikipedia.org/wiki/Static_single_assignment_form.2011-2-14
[129] T. Katayama, E. Itoh, and Z. Furukawa. Test-case generation for concurrentprograms with the testing criteria using interaction sequences. Proceedings ofthe6th Asian-Pacific Software Engineering Conference. December1999,pages590–597.
[130] E. Farchi, Y. Nir, and S. Ur. Concurrent bug patterns and how to test them.Proceedings of the17th International Symposium on Parallel and DistributedProcessing.2003, page286.
[2] H. B. Zhu. Building Reusable Components with Service-Oriented Architectures.Proceedings of2005IEEE International Conference on Information Reuse andIntegration (IEEE IRI-2005). Las Vegas, Nevada, USA: August2005,pages96-101.
[3] L.Roger, H. Ashok, and C. Chia-Chu et al. A framework for dynamicallyconverting components to web services. Proceeding of SERA'05.2005,pages431-437
[4] E. Cerami. Web Service Essentials:Dsitributed Applications with XML-RPC,SOAP, UDDI&WSDL. O’Reilly&Associates,Inc.2002
[5] WSDL:Web Service Definition Language1.1.URL http://www.w3.org/TR/uddi.
[6] SOAP. Simple Object Access Protlcol(SOAP1.1).URL http://www.w3.org/TR/SOAP.
[7] Web Services Glossary. W3C Working Group Note. February11,2004. URLhttp://www.w3.org/TR/2004/NOTE-ws-gloss-20040211/. Retrieved2011-04-22.
[8] UDDI.Universal Description,Discovery and Integeration2.0.URL http://www. w3.org/TR/wsdl.
[9] OASIS. Web Services Business Process Execution Language Version2.0. URLhttp://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.pdf.2008.
[10]吕毅.形式化方法综述—基本概念、技术源流和典型应用.技术报告,2003
[11] W. M. P. van der Aalst (Editor), Boualem Benatallah (Editor), and Fabio Casati(Editor), et.al.. Proceedings of the3rd International Conference on BusinessProcess Management,volume3649of Lecture Notes in Computer Science.Nancy,France: Springer-Verlag, September,2005.
[12]. Desel (Editor), B. Pernici (Editor), and M. Weske (Editor). Proceedings of the2nd International Conference on Business Process Management, volume3080ofLecture Notes in Computer Science. Potsdam, Germany: Springer-Verlag, June2004.
[13] W. M. P. van der Aalst (Editor), A. ter Hofstede (Editor), and M. Weske (Editor).Proceedings of the International Conference on Business ProcessManagement,volume2678of Lecture Notes in Computer Science. Eindhoven,Netherlands: Springer-Verlag, June2003.
[14] IEEE Computer Society. Proceedings of the2005IEEE InternationalConference on Web Services. Orlando, Florid, USA:2005.
[15] IEEE Computer Society. Proceedings of the2nd IEEE International Conferenceon Web Services. San Diego, California, USA:2004.
[16] IEEE Computer Society. Proceedings of the International Conference on WebServices. Las Vegas, NV, USA: CSREA Press,June2003.
[17] M. Bravetti, G. Zavattaro. Proceedings of the2nd International Workshop onWeb Services and Formal Methods, Volume3670of Lecture Notes in ComputerScience. Versailles, France: Sringer-Verlag, September2005..
[18] M. Bravetti, G. Zavattaro. Proceedings of the1st International Workshop onWeb Services and Formal Methods, volume105of Electronic Notes inTheoretical Computer Science. Pisa, Italy: Elsevier, February2004.
[19] F. van Breugel, M. Koshkina. Models and Verification of BPEL.http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf. September2006.
[20] K. Xu, Y. Liu, and G. G. Pu. Formalization, Verification and Restructuring ofBPEL Models with Pi Calculus and Model Checking. Research Report,RC-23962, IBM Thomas J. Watson Research Center, Yorktown Heights, NY10598(2006).
[21] Y. Liu, S. Müller, K. Xu. A static compliance-checking framework for businessprocess models. IBM SYSTEM JOURNAL, Vol46, No2.2007.
[22] T. He, H. K. Miao, Z. S. Gian. Analysis and modeling of web services flowusing Π-calculus. Journal of Southeast University (English Edition). March2006,Vol22(3), Pages315-318.
[23]高春鸣,黄邵,陈火旺. Web服务组合语言的出错与补偿处理的Pi演算编码.计算机工程与科学.2007，03，Vol29(3)，pages112-116.
[24] G. Salaun, A. Ferrara, and A. Chirichiello. Negotiation among web servicesusing LOTOS/CADP. In European conference on web services. September2004.
[25] G. Salaun, L. Bordeaux, and M. Schaerf. Describing and Reasoning on WebServices using Process Algebra. In IEEE International Conference on WebService (ICWS04).2004.
[26] M. Kovács, L. G nczy. Simulation and Formal Analysis of Workflow Models.Proceedings of the5th International Workshop on Graph Transformation andVisual Modeling Techniques, Vienna, Austria,2006.pages215-224.
[27] R. Gerth. Concise Promela Reference. Technical report, Eindhoven University,June1997.
[28] G. J. Holzmann. The Spin Model Checker, Primer and Reference Manual.Technical report, Addison-Wesley, Boston, MA, USA,2004.
[29] M. Mongiello, D. Castelluccia. Modelling and verification of BPEL businessprocesses. Proceedings of the Fourth Workshop on Model-Based Developmentof Computer-Based Systems and Third International Workshop on Model-BasedMethodologies for Pervasive and Embedded Software (MBD-MOMPES'06)-Vol00,2006.IEEE.
[30] S. Nakajima. Lightweight Formal Analysis of Web Service Flows. In Progressin Informatics, No.2, November2005.
[31] S. Nakajima. Model-Checking Behavioral Specifications of BPEL Applications.In WLFM’05, July2005.
[32] X. Fu, T. Bultan, and J. W. Su. Analysis of interacting BPEL web services.Proceedings of the13th International World Wide Web Conference, New York,NY, USA, May2004. ACM.pages621-630,
[33] X. Fu, T. Bultan, and J. W. Su. Synchronizability of conversations among webservices. IEEE Transactions on Software Engineering, December2005,Vol31(12), pages:1042-1055,
[34] M. Pistore, P. Traverso, and P. Bertoli et.al. Automated Synthesis of CompositeBPEL4WS Web Services. Proceedings of ICWS.2005, pages293-301.
[35] R. Kazhamiakin, M. Pistore. A Parametric Communication Model for theVerification of BPEL4WS Compositions. Proceedings of EPEW/WS-FM.2005.pages318-332
[36] R. Farahbod, R. Glsser, and M. Vajihollahi. A formal semantic for the BusinessProcess Execution Language for Web Services. In Web Services andModel-Driven Enterprise Information Services. May2005.
[37] D. Fahland. Complete Abstract Operational Semantics for the Web ServiceBusiness Process Execution Language. Technical report, Humboldt-Universit tzu Berlin, Institut für Informatik,Germany,2005.
[38] T. Bultan, X. Fu, and R. Hull et al. Conversation Specification: A NewApproach to Design and Analysis of E-Service Composition. Proceeding ofTwelfth International World Wide Web Conference (WWW2003).2003.
[39] H. Foster. A Rigorous Approach To Engineering Web Service Compositions.PhD thesis, Imperial College London, University Of London, January2006.
[40] H. Foster, S. Uchitel, and Magee et al. Model-based verification of Web servicecomposition. Proceedings of18th IEEE International Conference on AutomatedSoftware Engineering. Montreal, Canada: October2003, pages152-161.
[41] M. Simon, M. Axel, and H. Marc et al. Approach for Generating CompatibleWS-BPEL Partner Processes. Proceedings of the4th International Conferenceon Business Process Management. Vienna:September2006.
[42] X. P. Zhao, C. Antonio, and K. Padmanabhan. Verifying BPEL WorkflowsUnder Authorisation Containts. Proceedings of the4th InternationalConference on Business Process Management. Vienna: September2006.
[43] D. Karastoyanova, F. Leymann, J. Nitzsche et al. Parameterized BPELProcesses: Concepts and Implementation. Proceedings of the4th InternationalConference on Business Process Management. Vienna: September2006.pages471-476.
[44] S. Wang, J. Wan, and X. Yang. Describing, Verifying and Developing WebService Using the B-method. In International Conference on Next GenerationWeb Services Practices (NWeSP’06).2006.
[45] J. R. Abrial. The B-Book:Assigningprogramsto meanings. CambridgeUniversity Press.1996.
[46] K. Schmidt and C. Stahl. A Petri net semantic for BPEL4WS validation andapplication. Proceedings of the11th Workshop on Algorithms and Tools for PetriNets. Paderborn, Germany:September/October2004. pages1-6,
[47] C. Stahl. Transformation von BPEL4WS in Petrinetze. Master's thesis,Humboldt Universit at zu Berlin, Berlin, Germany, April2004.
[48] C. Stah. A Petri Net Semantics for BPEL. Technical Report188, HumboldtUniversit t zu Berlin, Institut für Informatik.2005.
[49] N. Lohmann, P. Massuthe, C. Stahl et al. Analyzing Interacting BPEL Processes.Proceedings of the4th International Conference on Business ProcessManagement. Vienna, Austria: September,2006.
[50] N. Lohmann. A Feature-Complete Petri Net Semantics or WS-BPEL2.0. In WebServices and Formal Methods International Workshop (WSFM07).2007.pages77–91.
[51] G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual.Addison-Wesley, Boston, MA, USA:2004.
[52] K. Schmidt. LoLA-a low level analyser. Proceedings of the21st InternationalConference on Application and Theory of Petri Nets, volume1825of LectureNotes in Computer Science. Aarhus, Denmark: Springer-Verlag, June2000,pages465-474.
[53] W. M. P. van der Aalst, M. Dumas, and C. Ouyang et al. ChoreographyConformance hecking: An Approach based on BPEL and Petri Nets. Proceedingsof the4th International Conference on Business Process Management, Vienna,Austria: September,2006.
[54] C. Ouyang, E. Verbeek, and W. M. P. Van der Aalst et al. Formal semantics andanalysis of control flow in WS-BPEL. Science of Computer Programmingarchive. July2007, Vol67(2-3), pages162-198
[55] R. Farahbod, U. Glsser, and M. Vajihollahi. A formal semantics for the BusinessProcess Execution Language for Web Services. In Web Services andModel-Driven Enterprise Information Services. May2005.
[56] H. Verbeek, W. M. P. Van der Aalst. Analyzing BPEL processes usingPetri-Nets. In Second International Workshop on Application of Petri-Nets toCoordination Workflow and Business Process Management. October2005.
[57] H. Kang, X. L. Yang, and S. M. Yuan. Modeling and Verification of WebServices Composition based on CPNIssue.2007IFIP International Conferenceon Network and Parallel Computing Workshops (NPC2007). September2007,pages613-617.
[57] Y. Yang, Q. Tan, and Y. Xiao. Verifying web services composition. InProceedings of the ER2005Workshops, Vol3770of Lecture Notes in ComputerScience. Klagenfurt, Austria: Springer Verlag, October2005. pages354-363,.
[59] Y. Yang, Q. Tan, and Y. Xiao et al. Exploiting hierarchical CP-netss to increasereliability of web services workflow. Proceeding of the International Symposiumon Applications and the Internet. Phoeniz, AZ, USA:January2006.pages116-122.
[60] Y. Yang, Q. Tan, and Y. Xiao et al. Verifying web services composition:Atransformation-based approach. Proceedings of the6th International Conferenceon Parallel and Distributed Computing. Dalian, China: December2005,pages546-548.
[61] Y. Yang, Q. Tan, and Y. Xiao. Verifying web services composition based onhierarchical colored Petri nets. Proceedings of the1st International Workshop onInteroperability of Heterogeneous Information Systems. Bremen, Germany:November2005, pages47-54.
[62] X. Yi and K. J. Kochut. Process composition of web services with complexconversation protocols: a colored Petri nets based approach. Proceedings of theDesign, Analysis, and Simulation of Distributed Systems Symposium. Arlington,VA, USA: April2004, pages141-148,.
[63] S. Thatte. XLANG: Web Services for Business Process Design. MicrosoftCorporation. URLhttp://www.gotdotnet.com/team/xml_wsspecs/xlang-c/default.htm.2001.
[64] F. Leymann. Web Services Flow Language (WSFL1.0). IBM Corporation, May2001. URLhttp://www-4.ibm.com/software/solutions/webservices/pdf/WSFL.pdf
[65] F. Curbera, Y. Goland, and J. Klein et al. Business process execution languagefor web services, version1.0. July2002.
[66] T. Murat. Petri nets: Properties, analysis and applications. Proceedings of theIEEE,1989,Vol77(4),541–580.
[67] K. Jensen, L. M. Kristensen, and L. Wells. Coloured Petri Nets and CPN Toolsfor Modelling and Validation of Concurrent Systems. International Journal onSoftware Tools for Technology Transfer. Springer Verlag, September2007,pages213-254
[68] V. M. P. Van der Aalst. The Application of Petri Nets to Workflow Management.Journal of Circuits, Systems and Computers.1998, vol8(1),. pages21-66.
[69] K. Jensen. An Introduction to the Theoretical Aspects of Coloured Petri Nets.A Decade of Concurrency, Lecture Notes in Computer Science. Springer-Verlag,1994, Vol803, pages230-272.
[70] J. L. Peterson. Petri Net Theory and the Modeling of Systems. Prentice-HallInternational,1981.
[71] X. Yi, J. K. Krys. A Framework for Web Services Composition Design andVerification. UGA Computer Science Technical Report, UGA-CS-TR-04-001.URL http://www.cs.uga.edu/~xyi/tr04001.pdf
[72] S. Chatterjee, J. Webber. Developing Enterprise Web Services:An Architect’sGuide. Prentice Hall,2004.
[73] CP-nets tools. URL http://www.daimi.au.dk/CP-netstools/
[74] T. Suzuki, S. M. Shatz, and T. A. Murata. Protocol Modeling and VerificationApproach Based on a Specification Language and Petri Nets.1990, vol16(5),pages523-536.
[75] J. Billington, M. Diaz, and G. Rozenberg(eds.). Application of Petri nets tocommunication networks: advances in Petri nets. Lecture Notes in ComputerScience. Springer,1999.
[76] L. D. Silva, A. Perkusich. A model-based approach to formal specification andverification of embedded systems using coloured petri nets. Component-BasedSoftware Development for Embedded Systems. Springer Berlin Heidelberg:2005, vol3778, pages35-58.
[77] K. Jensen. Computer verification tool: Colored Petri nets.URL http://wiki.daimi.au.dk/cpntools.2010-10-01
[78] A. W. Appel, D. B. Macqueen. Standard ML of New Jersey. In3rd InternationalSymposium on Programming Language Implementation and LogicProgramming. New York, USA. Vol.528of Lecture Notes in Computer Science.Springer-Verlag.1991.
[79] S. Narayanan, S. McIlraith. Analysis and simulation of Web services, ComputerNetworks.2003, Vol.42, pages675-693.
[80] URL http://wiki.daimi.au.dk/cpntools-help/.2008-11-24
[81] Fehling, A. Rainer Concept of Hierarchical Petri Nets with Building Blocks. the12th International Conference on Application and Theory of Petri Nets.1991.
[82]郝克刚,葛玮.关于高级网系统的等价及谱系的研究.计算机学报.1993年第7期.
[83]郝克刚,丁剑洁.层次结构的Petri网.计算机科学与探索.2008,vol2(2).
[84] K. Jense. Coloured Petri Nets. Basic Concepts, Analysis Methods and PracticalUse. Vol.1: Basic Concepts. EATCS Monographs on Theoretical ComputerScience. Springer-Verlag,1992.
[85] N. Lohmann, H. Verbeek, C. Ouyang et al. Comparing and evaluating Petri netsemantics for BPEL. Computer Science Report07/23, Eindhoven University ofTechnology, Eindhoven, The Netherlands (2007)
[86] E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press,Cambridge, MA, USA:1999.
[87]林惠民,张文辉.模型检测：理论、方法与应用.电子学报.2002, Vol12(3),pages1906-912.
[88] A. Cheng A, S. Christensen, K. H. Mortensen. Model checking colored Petrinets exploiting strongly connected components. Proceeding of the InternationalWorkshop on Discrete Event Systems. Edinburgh, Scotland, UK:1996,pages169-177.
[89] P. Colin, Stirling. Modal and temporal logics for processes. Technical report,Department of Computer Science, University of Edinburgh. August1993.
[90] M. Hut, M. Ryan. Logic in Computer Science.北京:机械工业出版社,2005
[91] J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. InPLDI02: Programming Language Design and Implementation. ACM:2002.pages1-12.
[92] M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification inpolynomial time. In PLDI02: Programming Language Design andImplementation. ACM:2002, pages57-68.
[93] R. Alur, A. Itai, and R. P. Kurshan et al. Timing verification by successiveapproximation. Information and Computation.1995, vol118(1), pages:142-157.
[94] T. Ball, S. K. Rajamani. Automatically validating temporal safety properties ofinterfaces. In SPIN2001: SPIN Workshop, LNCS2057,. Springer-Verlag,2001.pages103-122.
[95] H. Saidi Model checking guided abstraction and analysis. In SAS00:Static-Analysis Symposium. LNCS1824, Springer-Verlag,2000. pages377-396.
[96] E. Clarke, O. Grumberg, and S. Jha et al. Counterexample-guided abstractionrefinement. In CAV00: Computer Aided Verification, LNCS1855,Springer-Verlag,2000, pages154-169.
[97] S. Graf, H. Saidi. Construction of abstract state graphs with PVS. Proceedingsof the9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel,June1997, pages7283.
[98] S. Das. Predicate Abstraction. Ph.D. Thesis.Department of ElectricalEngineering, Stanford University, December2003.
[99] E. M. Clarke, O. Grumberg O, and D. E. Long. Model checking and abstraction.ACM Transactions on Programming Languages and Systems.1994, Vol16(5),pages1512–1542.
[100] L. M. Kristensen. State Space Methods for Coloured Petri Nets. Department ofComputer Science, University of Aarhus, Denmark,2000.
[101] T. A. Henzinger, R. Jhala, and R. Majumdar. Lazy abstraction. Proceeding of theACM Sympsium on Principles of Programming Languages. Oregon: ACM Press,2002, pages5870.
[102] R. Jhala. Program Verification by Lazy Abstraction. Ph.D. Thesis. Departmentof Computer Science, University of California Berkeley, Fall2004
[103] H. J. Genrich, K. Lautenbach. System Modeling with High Level Petri Nets.Theoretical Compoter Science.1981, Vol13.
[104] P. Huber, A. M. Jensen, and L. O. Jepsen et al. Reachability Trees for HighLevel Petri Nets. Theoretical Computer Science.1986, vol45(3).
[105] R. N. Taylor, D. L. Levine, and C. D. Kelly. Structural testing of concurrentprograms. IEEE Transactions on Software Engineering. March,1992, vol18(3),pages206–215.
[106] J. Cardoso. Complexity Analysis of BPEL Web Processes. Software Process:Improvement and Practice Journal.2006, vol12, pages35–49.
[107] J. Thomas. McCabe. A Complexity Measure. IEEE Transaction on SoftwareEngineering, SE-2(4).1976, pages308–320.
[108] W. Michael, Whalen, A. Rajan et al. Coverage metrics for requirements-basedtesting. In ISSTA’06: Proceedings of the2006international symposium onSoftware testing and analysis. New York, NY, USA: ACM Press,2006,pages25–36.
[109] J. R. Horgan and S. London. Data flow coverage and the C language. In TAV4:Proceedings of the symposium on Testing, analysis, and verification, New York,NY, USA: ACM Press,1991, pages87–97.
[110] J. Garca-Fanjul, J. Tuya, and C. De la Riva. Generating Test Cases Specicationsfor BPEL Compositions of Web Services Using SPIN. In InternationalWorkshop on Web Services Modeling and Testing (WS-MaTe2006).2006.
[111] L. Mei, W. K. Chan, and T. H. Tse. Data Flow Testing of Service-OrientedWorkflow Applications. Proceedings of the30th International Conference onSoftware Engineering (ICSE2008), New York, NY, USA: ACM,2008,pages371–380.
[112] J. Yan, Z. Li, Y. Yuan et al. BPEL4WS Unit Testing: Test Case Generation Usinga Concurrent Path Analysis Approach. In17th International Symposium onSoftware Reliability Engineering (ISSRE’06). IEEE,2006.
[113] D. L¨ubke and A. Salnikow. Definition and Formalization of BPEL Process TestCoverage. Technical report, Leibniz Universit¨at Hannover, FG SoftwareEngineering. URL http://www.se.uni-hannover.de/techreports/2009-01DefinitionAndFormalizationOfBpelProcessTestCoverage.pdf,2008.
[114] D. Lubke, L. Singer, A. Salnikow. Calculating BPEL Test Coverage throughInstrumentation. Proceedings of the4th International Workshop on Automationof Software Test, AST2009, Vancouver, BC, Canada: May2009.
[115] M. Phili. BPELUnit. URL http://www.bpelunit.org.2007-09-01.
[116] R. D. Yang and C. G. Chung. A path analysis approach to concurrent programtesting. Information and Software Technology.1992, Vol34(1), pages43–56.
[117] L. Mei, W. K. Chan, and T. H. Tse. Data Flow Testing of Service-OrientedWorkflow Applications. Proceedings of the30th International Conference onSoftware Engineering (ICSE2008), New York, NY, USA: ACM,2008,pages371–380,
[118] IEEE standard glossary of software engineering terminology, IEEE Std610.12-1990, September1990.
[119] Y. Yuan, Z. Li, and W. Sun. A Graph-Search Based Approach to BPEL4WS TestGeneration. International Conference on Software Engineering Advances.2006.
[120] Z. J. Li, H. F. Tan, H. H. Liu et al. Business-process-driven gray-box SOAtesting. IBM Systems Journal.2008, Vol47, pages457-472.
[121] C. H. Liu, S. L. Chen, and X. Y. Li. A WS-BPEL Based Structural TestingApproach for Web Service Compositions. IEEE International Symposium onService-Oriented System Engineering (SOSE '08).2008.
[122] R. Blanco, J. Garcia-Fanjul, and J. Tuya. A First Approach to Test CaseGeneration for BPEL Compositions of Web Services Using Scatter Search.International Conference on Software Testing, Verification and ValidationWorkshops (ICSTW '09).2009.
[123] A. T. Endo, A. D. Simao, S. Souza et al. Web Services Composition Testing: AStrategy Based on Structural Testing of Parallel Programs. Testing: Academic&Industrial Conference Practice and Research Techniques (TAIC PART '08).2008.
[124] Z. Li, W, Sun, Z. B. Jiang et al. BPEL4WS unit testing: framework andimplementation. Proceedings of the IEEE International Conference on WebServices (ICWS2005).2005.
[125] M. Staples, M. Niazi. Experiences using systematic review guidelines. Journalof Systems and Software.2007, Vol80, pages1425-1437.
[126] J. J. Domínguez-Jiménez, A. Estero-Botaro, and I. Medina-Bulo. A Frameworkfor Mutant Genetic Generation for WSBPEL. in SOFSEM2009: Theory andPractice of Computer Science,2009. pages229-240.
[127] J. Zhang, X. Wang. A constraint solver and its application to path feasibilityanalysis. International Journal of Software Engineering&KnowledgeEngineering.2001. Vol11(2), pages139–156.
[128] URL http://en.wikipedia.org/wiki/Static_single_assignment_form.2011-2-14
[129] T. Katayama, E. Itoh, and Z. Furukawa. Test-case generation for concurrentprograms with the testing criteria using interaction sequences. Proceedings ofthe6th Asian-Pacific Software Engineering Conference. December1999,pages590–597.
[130] E. Farchi, Y. Nir, and S. Ur. Concurrent bug patterns and how to test them.Proceedings of the17th International Symposium on Parallel and DistributedProcessing.2003, page286.