面向服务的业务事务建模与验证方法研究
|
摘要
面向服务的计算(Service-Oriented Computing, SOC)是一种以Web服务作为基本组件的分布式计算模式，它支持开放、动态和异构环境下分布式应用的系统集成。Web服务正从最初关注描述、发布和交互向支持健壮的业务协作新阶段发展。为了保证面向服务的应用获得正确、一致的执行结果，大多数工作流和B2B协作应用程序都需要支持复杂的、长时间运行的业务事务。面向服务的业务流程除了关注服务组合业务流程的功能特性外，应该整合考虑合成之上的事务特性。如何设计正确的Web服务组合业务流程，让它们协同工作并保持一致，即确保面向服务的业务事务(Business Transactions for Services, BTS)正确地执行是当前一个具有挑战性的重要问题。本文从操作系统进程管理的视角提出了面向服务的业务事务的概念视图,将现阶段的事务处理归结为在业务流程执行过程中对服务、活动及流程的分层管理。从建模语言到验证方法、从建模分析到验证实现，本文为面向服务的业务事务的正确性保障建立了一套系统的解决方案。主要研究成果如下：
(1)提出了一种支持非功能性描述的移动进程代数MPi-演算。根据应用语义需求引入进程作用域的概念，扩展了Pi-演算进程移动性的含义。用链接相对进程作用域的移动来表示进程的移动，使得MPi-演算能够描述组件之间交互行为的非功能属性，具有兼顾系统功能性和非功能性描述的表达能力。提出了一种膜互模拟关系，使得在进程作用域内部具有不同行为的两个进程也可以被认为是等价的，并引入了膜等价概念，得出与强/弱互模拟等价类似的性质。
(2)提出了一种等价自动机转换的模型验证方法。MPi-演算能够被解释成标号迁移系统(Labelled Transition System, LTS)，NuSMV是基于Kripke结构(Kripke Structure, KS)的符号模型检验器，LTS与KS都属于状态自动机(StateAutomata)。根据元模型LTS和KS之间的语义映射关系，给出了从MPi-演算模型到NuSMV的输入语言SMV的语法转换规则。基于元模型定义的语义映射关系和语法转换规则可以提高模型转换的可复用性和可移植性。
(3)在服务层研究了如何保持业务流程参与者之间的协调一致性问题，提出了支持业务事务验证的服务协调模型。针对Web服务事务标准(WS-TX)定义的参与者之间交互消息缺乏严格的语义，用Pi-演算形式化描述了WS-TX规范中定义业务活动事务的WS-BA协议，在此基础上建立了适用于多个参与者的服务协调模型，并验证分析了协议的安全性和活性。实验结果表明，基于服务协调模型的业务事务验证方法，能够有效地提高业务流程执行的可靠性和一致性。
(4)在活动层研究了如何利用Web服务事务模型分析事务的等价性问题，提出了面向服务的柔性事务建模与分析方法。用MPi-演算对柔性事务模型进行了形式化描述，考虑进程行为的事务依赖性，提出了一种事务膜等价关系。通过一个典型的柔性事务实例，阐述了利用事务膜开互模拟分析事务等价关系的方法。实验结果表明，事务膜开互模拟分析方法能够判别事务等价关系，约简目标系统模型，有效降低系统验证的复杂度。
(5)在流程层研究了如何保证跨组织业务流程的可靠性问题，提出了跨组织多业务事务的建模与验证方法。将进程的动作交互与跨组织膜活动建立动态关联，提出了跨组织多业务事务建模方法。验证分析了多业务事务中排他性、响应性、非阻塞性和非平凡性等关键性质。实验结果表明，对于复杂的多业务事务，经过抽象或分解后，同样能够采用该方法保障多业务流程在设计与实现过程中的可靠性。
(6)提出了基于策略的面向服务的业务事务验证支撑系统框架，提供了一种事务运行时的验证机制。设计和实现了面向服务的业务事务形式化验证原型工具VBT4S(Verification ofBusiness Transactions for Services)，支持主流开源的符号模型检验器NuSMV2。实验结果表明，系统支持非功能属性(如事务的完整性和一致性等)相关命题性质的模型检测，具有功能和非功能性质的统一验证与分析能力。
Service Oriented Computing (SOC) is an emerging paradigm for distributed computing that usesservices as basic computational entities. SOC supports distributed application system integration inthe open-ended, dynamic and heterogeneous environment. Web services are moving from their initialcapability of description, publication and interaction to a new stage in which the robust businesscollaboration is supported. To ensure that service-based applications achieve correct and consistentoutcomes, most of the workflows and the B2B collaboration applications need to support complexand long-running business transactions. In addition to functional features of the business processprovided by service compositions, we should bring into consideration transactional features abovecompositions in business processes for services. How to verify correctness in the design of businessprocess provided by service compositions and keep them in consistent agreement on the outcomesfrom their working together, that is, correctness verification in the implementation of businesstransactions for services (BTS), is a challenging and important problem. A conceptual view of BTS isproposed in this paper from a process-management perspective in the operating system. Thetransaction processing at this stage is boiled down to the layer management of services, activities andprocesses during the execution of business processes. From modeling languages to verificationmethods, and then from modeling analysis to verifying implementations, a systemic solution isproposed to ensure the correctness of BTS. The main contributions of this dissertation are summarizedas follows:
Firstly, a calculus of mobile processes named MPi-calculus is proposed in support of thenon-functional specifications. According to the requirements of application semantics, the concept ofthe process scope is introduced, and then the meaning of the process mobility is extended. Themovement of a process can be represented entirely by the movement of its links relative to its scope.This enables MPi-calculus to describe non-functional attributes of interactive behaviour between thecomponents and to have the expressive power for describing the functional and non-functionalcharacteristics. A new relationship named membrane bisimulation is proposed, which allows twoprocesses to be considered equivalent even if they have dissimilar patterns of the behaviour insidetheir process scope. The membrane equivalence is introduced, and then some properties similar to thestrong/weak equivalence are obtained.
Secondly, a model verification methodology is proposed by equal value transformation of the finite state automaton. Traditionally the behavior of MPi-calculus is modeled on a Labeled TransitionSystem (LTS), and a symbolic model checker named NuSMV is based on the transition relation of aKripke structure. LTS and KS are very similar and they can be seen as generalizations of stateautomata. According to semantic mapping relations between two meta-models, i.e., LTS and KS,syntactic transformation rules are presented from MPi-calculus processes to the input language ofNuSMV. These semantic mapping relations and syntactic transformation rules defined by meta-modelcan improve the reusability and portability of the model transformation.
Thirdly, at the service-level, a service coordination model is proposed in support of the businesstransactions verification by studying the problem of how to keep consistent agreement among theparticipants involved in the business process. For the definitions of the message exchanges that takeplace between the process and each one of its partners in WS-TX standard lack the precise semanticdescriptions, the Pi-calculus description of the WS-Business Activity protocol (WS-BA) is given,which specifies coordination types for long running loosely coupled business transactions. A servicecoordination model for multi-participants is proposed based on the formalization of the messaginginteractions semantics in WS-BA. Then this research verifies a system whether the protocol satisfiesthe principles of safety and liveness. Experimental results show that the business transactionverification based on service coordination model can effectively enhance the reliability andconsistency in business process execution.
Fourthly, at the activity-level, the modeling and analysis method of flexible transactions forservices is proposed by studying the problem of how to analyze transactional equivalence relationsusing Web services transaction model. The formal description of the flexible transaction model inMPi-calculus is given. A transactional membrane equivalence relation is defined by introducingtransactional dependencies of the process behaviour. A running example presents the methodanalyzing transactional equivalence relation with the transactional membrane open bisimulation.Experimental results show that this method can judge the transactional equivalence relation, andreduce the target system model. This will effectively decrease the complexity of system verification.
Fifthly, at the process-level, the modeling and verification method of cross-organizationalmulti-business transactions is proposed by studying the problem of how to ensure the reliability in thedesign and implementation of cross-organizational business processes. In the modeling approach,transaction semantics are introduced by the connection between the process interactions andcross-organizational membrane activities. The model checker is employed for checking whether or not the multi-business transactions satisfy the given key properties such as excludability,responsibility, non-blocking and non-triviality. Experimental results show that this method worksequally well for complex multi-business transactions by completing the abstraction or decomposition.
Lastly, a supporting system framework for verification of business transactions for services(VBT4S) based on the policy enforcement is proposed, which provides a mechanism for runtimeverification of transactions. A prototype system named VBT4S is designed and implemented, whichsupports the major open source symbolic model checker (e.g. NuSMV2). Experimental results showthat the system can support the specification of non-functional properties (e.g. transactional integrityand consistency), and provide approaches to formally verify and analyze functional andnon-functional properties in a unified way.
(1)提出了一种支持非功能性描述的移动进程代数MPi-演算。根据应用语义需求引入进程作用域的概念，扩展了Pi-演算进程移动性的含义。用链接相对进程作用域的移动来表示进程的移动，使得MPi-演算能够描述组件之间交互行为的非功能属性，具有兼顾系统功能性和非功能性描述的表达能力。提出了一种膜互模拟关系，使得在进程作用域内部具有不同行为的两个进程也可以被认为是等价的，并引入了膜等价概念，得出与强/弱互模拟等价类似的性质。
(2)提出了一种等价自动机转换的模型验证方法。MPi-演算能够被解释成标号迁移系统(Labelled Transition System, LTS)，NuSMV是基于Kripke结构(Kripke Structure, KS)的符号模型检验器，LTS与KS都属于状态自动机(StateAutomata)。根据元模型LTS和KS之间的语义映射关系，给出了从MPi-演算模型到NuSMV的输入语言SMV的语法转换规则。基于元模型定义的语义映射关系和语法转换规则可以提高模型转换的可复用性和可移植性。
(3)在服务层研究了如何保持业务流程参与者之间的协调一致性问题，提出了支持业务事务验证的服务协调模型。针对Web服务事务标准(WS-TX)定义的参与者之间交互消息缺乏严格的语义，用Pi-演算形式化描述了WS-TX规范中定义业务活动事务的WS-BA协议，在此基础上建立了适用于多个参与者的服务协调模型，并验证分析了协议的安全性和活性。实验结果表明，基于服务协调模型的业务事务验证方法，能够有效地提高业务流程执行的可靠性和一致性。
(4)在活动层研究了如何利用Web服务事务模型分析事务的等价性问题，提出了面向服务的柔性事务建模与分析方法。用MPi-演算对柔性事务模型进行了形式化描述，考虑进程行为的事务依赖性，提出了一种事务膜等价关系。通过一个典型的柔性事务实例，阐述了利用事务膜开互模拟分析事务等价关系的方法。实验结果表明，事务膜开互模拟分析方法能够判别事务等价关系，约简目标系统模型，有效降低系统验证的复杂度。
(5)在流程层研究了如何保证跨组织业务流程的可靠性问题，提出了跨组织多业务事务的建模与验证方法。将进程的动作交互与跨组织膜活动建立动态关联，提出了跨组织多业务事务建模方法。验证分析了多业务事务中排他性、响应性、非阻塞性和非平凡性等关键性质。实验结果表明，对于复杂的多业务事务，经过抽象或分解后，同样能够采用该方法保障多业务流程在设计与实现过程中的可靠性。
(6)提出了基于策略的面向服务的业务事务验证支撑系统框架，提供了一种事务运行时的验证机制。设计和实现了面向服务的业务事务形式化验证原型工具VBT4S(Verification ofBusiness Transactions for Services)，支持主流开源的符号模型检验器NuSMV2。实验结果表明，系统支持非功能属性(如事务的完整性和一致性等)相关命题性质的模型检测，具有功能和非功能性质的统一验证与分析能力。
Service Oriented Computing (SOC) is an emerging paradigm for distributed computing that usesservices as basic computational entities. SOC supports distributed application system integration inthe open-ended, dynamic and heterogeneous environment. Web services are moving from their initialcapability of description, publication and interaction to a new stage in which the robust businesscollaboration is supported. To ensure that service-based applications achieve correct and consistentoutcomes, most of the workflows and the B2B collaboration applications need to support complexand long-running business transactions. In addition to functional features of the business processprovided by service compositions, we should bring into consideration transactional features abovecompositions in business processes for services. How to verify correctness in the design of businessprocess provided by service compositions and keep them in consistent agreement on the outcomesfrom their working together, that is, correctness verification in the implementation of businesstransactions for services (BTS), is a challenging and important problem. A conceptual view of BTS isproposed in this paper from a process-management perspective in the operating system. Thetransaction processing at this stage is boiled down to the layer management of services, activities andprocesses during the execution of business processes. From modeling languages to verificationmethods, and then from modeling analysis to verifying implementations, a systemic solution isproposed to ensure the correctness of BTS. The main contributions of this dissertation are summarizedas follows:
Firstly, a calculus of mobile processes named MPi-calculus is proposed in support of thenon-functional specifications. According to the requirements of application semantics, the concept ofthe process scope is introduced, and then the meaning of the process mobility is extended. Themovement of a process can be represented entirely by the movement of its links relative to its scope.This enables MPi-calculus to describe non-functional attributes of interactive behaviour between thecomponents and to have the expressive power for describing the functional and non-functionalcharacteristics. A new relationship named membrane bisimulation is proposed, which allows twoprocesses to be considered equivalent even if they have dissimilar patterns of the behaviour insidetheir process scope. The membrane equivalence is introduced, and then some properties similar to thestrong/weak equivalence are obtained.
Secondly, a model verification methodology is proposed by equal value transformation of the finite state automaton. Traditionally the behavior of MPi-calculus is modeled on a Labeled TransitionSystem (LTS), and a symbolic model checker named NuSMV is based on the transition relation of aKripke structure. LTS and KS are very similar and they can be seen as generalizations of stateautomata. According to semantic mapping relations between two meta-models, i.e., LTS and KS,syntactic transformation rules are presented from MPi-calculus processes to the input language ofNuSMV. These semantic mapping relations and syntactic transformation rules defined by meta-modelcan improve the reusability and portability of the model transformation.
Thirdly, at the service-level, a service coordination model is proposed in support of the businesstransactions verification by studying the problem of how to keep consistent agreement among theparticipants involved in the business process. For the definitions of the message exchanges that takeplace between the process and each one of its partners in WS-TX standard lack the precise semanticdescriptions, the Pi-calculus description of the WS-Business Activity protocol (WS-BA) is given,which specifies coordination types for long running loosely coupled business transactions. A servicecoordination model for multi-participants is proposed based on the formalization of the messaginginteractions semantics in WS-BA. Then this research verifies a system whether the protocol satisfiesthe principles of safety and liveness. Experimental results show that the business transactionverification based on service coordination model can effectively enhance the reliability andconsistency in business process execution.
Fourthly, at the activity-level, the modeling and analysis method of flexible transactions forservices is proposed by studying the problem of how to analyze transactional equivalence relationsusing Web services transaction model. The formal description of the flexible transaction model inMPi-calculus is given. A transactional membrane equivalence relation is defined by introducingtransactional dependencies of the process behaviour. A running example presents the methodanalyzing transactional equivalence relation with the transactional membrane open bisimulation.Experimental results show that this method can judge the transactional equivalence relation, andreduce the target system model. This will effectively decrease the complexity of system verification.
Fifthly, at the process-level, the modeling and verification method of cross-organizationalmulti-business transactions is proposed by studying the problem of how to ensure the reliability in thedesign and implementation of cross-organizational business processes. In the modeling approach,transaction semantics are introduced by the connection between the process interactions andcross-organizational membrane activities. The model checker is employed for checking whether or not the multi-business transactions satisfy the given key properties such as excludability,responsibility, non-blocking and non-triviality. Experimental results show that this method worksequally well for complex multi-business transactions by completing the abstraction or decomposition.
Lastly, a supporting system framework for verification of business transactions for services(VBT4S) based on the policy enforcement is proposed, which provides a mechanism for runtimeverification of transactions. A prototype system named VBT4S is designed and implemented, whichsupports the major open source symbolic model checker (e.g. NuSMV2). Experimental results showthat the system can support the specification of non-functional properties (e.g. transactional integrityand consistency), and provide approaches to formally verify and analyze functional andnon-functional properties in a unified way.
引文
[1] Greenfield P., Kuo D., Nepal S., Fekete A. Consistency for web services applications. In: Proc.of the31st international conference on Very large data bases (VLDB '05).2005.1199-1203.
[2] Gray J., Reuter A. Transaction Processing: Concepts and Techniques. Morgan Kaufmann,1993.4-5.
[3] Thomas E. Service-Oriented Architecture: A Field Guide to Integrating XML and Web Services.Prentice Hall,2004.
[4] Singh M. P., Huhns M. N. Service-Oriented Computing: Semantics, Processes, Agents. JohnWiley&Sons, Ltd.,2005.
[5]喻坚,韩燕波.面向服务的计算--原理和应用.北京:清华大学出版社,2006.178-191.
[6] Tsai W. T. Service-Oriented System Engineering: A New Paradigm. In: Proc. of IEEEInternational Workshop on Service-Oriented System Engineering (SOSE). IEEE ComputerSociety,2005.3-8.
[7]韩燕波.《面向服务的计算》专辑介绍.计算机学报,2006,26(07):3-4.
[8]任怡,吴泉源,贾焰.事务处理技术研究综述.计算机研究与发展,2005,42(10):136-141.
[9] Bjork L. A., Davies J. C. T. The Semantics of the Preservation and Recovery of Integrity in a DataSystem. IBM General Products Division, TR02.540,1972.
[10] Bjork L. A. Recovery scenario for a DB/DC system. In: Proc. of the ACM annual conference.ACM,1973.142-146.
[11] Davies J. C. T. Data processing spheres of control. IBM Systems Journal,1978,17(2):179-198.
[12] Elmagarmid A. K. Database Transaction Models for Advanced Applications. Morgan Kaufmann,1992.
[13] Eliot J., Moss B. Nested transactions: an introduction. In: K. B. Bharat, ed. Concurrency controland reliability in distributed systems: Van Nostrand Reinhold Co.,1987.395-425.
[14] Weikum G. Principles and realization strategies of multilevel transaction management. ACMTransactions on Database Systems (TODS),1991,16(1):132-180.
[15] Garcia-Molina H., Salem K. Sagas. In: Proc. of the ACM international conference onManagement of data (SIGMOD).1987.249-259.
[16] Pu C., Kaiser G. E., Hutchinson N. C. Split-Transactions for Open-Ended Activities. In: Proc. ofthe14th International Conference on Very Large Data Bases(VLDB). Morgan KaufmannPublishers Inc.,1988.26-37.
[17] Bukhres O. A., Elmagarmid A. K., Kühn e. Implementation of the Flex Transaction Model. IEEEData Engineering Bulletin,1993,16(2):28-32.
[18] Zhang A., Nodine M., Bhargava B. Global Scheduling for Flexible Transactions in HeterogeneousDistributed Database Systems. IEEE Transactions on Knowledge and Data Engineering,2001,13(3):439-450.
[19]唐飞龙,李明禄,曹健.一个Web服务事务处理模型:结构、算法和事务补偿.电子学报,2003,31(12A):2074-2078.
[20]任怡,吴泉源,戴华东,吴庆波.一种基于QoS的事务工作流并发调度算法.电子学报,2007,35(4):621-628.
[21] Huang T., Ding X., Wei J. An application-semantics-based relaxed transaction model forinternetware. Science in China Series F: Information Sciences,2006,49(6):774-791.
[22] Sheth A. P., Rusinkiewicz M. On Transactional Workflows IEEE Data Engineering Bulletin,1993,16(2):37-40.
[23] Hagen C., Alonso G. Exception Handling in Workflow Management Systems. IEEE Transactionson Software Engineering,2000,26(10):943-958.
[24] Curbera F., Khalaf R., Mukhi N., Tai S., Weerawarana S. The next step in Web services.Communications of the ACM,2003,46(10):29-34.
[25] Jordan D., Evdemon J., Alves A., Arkin A., Askary S., Barreto C., Bloch B., Curbera F., Ford M.,Goland Y., Web services business process execution language, version2.0, OASIS Standard, May2007.
[26] Little M., Freund T., Feingold M., Robinson I. Web Services Transaction (WS-TX Version1.2).Feb.2009.
[27] Wang W., Hidvégi Z., Bailey A. D., Whinston A. B. E-process design and assurance using modelchecking. Computer,2000,33(10):48-53.
[28] Fu X., Bultan T., Su J. Analysis of interacting BPEL web services. In: Proc. of the13thinternational conference on World Wide Web(WWW '04).2004.621-630.
[29] Fu X., Bultan T., Su J. WSAT: A Tool for Formal Analysis of Web Services. In: Computer AidedVerification, LNCS3114: Springer Berlin/Heidelberg,2004.394-395.
[30] Pu G., Zhao X., Wang S., Qiu Z. Towards the Semantics and Verification of BPEL4WS.Electronic Notes in Theoretical Computer Science (ENTCS),2006,151(2):33-52.
[31] Foster H., Uchitel S., Magee J., Kramer J. Compatibility Verification for Web ServiceChoreography. In: Proceedings of the IEEE International Conference on Web Services(ICWS'04). IEEE Computer Society,2004.738-741.
[32] Magee J., Kramer J. Concurrency-State Models&Java Programs.2edition: John Wiley,2006.
[33] Foster H., Uchitel S., Magee J., Kramer J. LTSA-WS: a tool for model-based verification of webservice compositions and choreography. In: Proceedings of the28th international conference onSoftware engineering(ICSE '06). ACM,2006.771-774.
[34] Aalst W. M. P. v. d. Modeling and Analyzing Interorganizational Workflows. In: Proc. of theInternational Conference on Application of Concurrency to System Design(ACSD'98). IEEEComputer Society,1998.262-272.
[35] Aalst W. M. P. v. d., Hee K. M. v. Workflow Management: Models, Methods, and Systems.Cambridge: MIT Press,2004.
[36] Aalst W. M. P. v. d. The Application of Petri Nets to Workflow Management. Journal of CircuitsSystems and Computers,1998,8(1):21-66.
[37] Aalst W. M. P. v. d. Verification of Workflow Nets. In: Proc. of the18th InternationalConference on Application and Theory of Petri Nets. Springer-Verlag,1997.407-426.
[38] Sun P., Jiang C. Analysis of workflow dynamic changes based on Petri net. Information andSoftware Technology,2009,51(2):284-292.
[39] Cicirelli F., Furfaro A., Nigro L. A service-based architecture for dynamically reconfigurableworkflows. Journal of Systems and Software,83(7):1148-1164.
[40] Hamadi R., Benatallah B. A Petri net-based model for web service composition. In: Proc. of the14th Australasian database conference(ADC '03). Australian Computer Society, Inc.,2003.191-200.
[41] Ouyang C., Verbeek E., van der Aalst W., Breutel S., Dumas M., ter Hofstede A. WofBPEL: ATool for Automated Analysis of BPEL Processes. In: Service-Oriented Computing-ICSOC2005, LNCS3826: Springer Berlin/Heidelberg,2005.484-489.
[42] Valero V. n., Cambronero M. E., D′az G., Macià H. A Petri net approach for the design andanalysis of Web Services Choreographies. Journal of Logic and Algebraic Programming,2009,78(5):359-380.
[43]范贵生,虞慧群,陈丽琼,刘冬梅.基于Petri网的服务组合故障诊断与处理.软件学报,2010,21(02):231-247.
[44]唐飞龙,李明禄,黄哲学,王卓立.服务网格中的事务服务及基于Petri网的正确性分析.计算机学报,2005,28(04):667-676.
[45] Hoare C. A. R. Communicating sequential processes. Communications of the ACM,1978,21(8):666-677.
[46] Milner R. A Calculus of Communicating Systems. New York: Springer-Verlag,1982.
[47] Milner R., Parrow J., Walker D. A calculus of mobile processes. Part I/II. Information andComputation,1992,100(1):1-77.
[48] Momtahan L., Martin A., Roscoe A. W. A Taxonomy of Web Services Using CSP. ElectronicNotes in Theoretical Computer Science,2006,151(2):71-87.
[49] Brogi A., Canal C., Pimentel E., Vallecillo A. Formalizing Web Service Choreographies.Electronic Notes in Theoretical Computer Science,2004,105.73-94.
[50] Cámara J., Canal C., Cubo J., Vallecillo A. Formalizing WSBPEL Business Processes UsingProcess Algebra. Electronic Notes in Theoretical Computer Science,2006,154(1):159-173.
[51] Butler M., Ferreira C. An operational semantics for StAC, a language for modelling long-runningbusiness transactions. In: R. D. Nicola, G.-L. Ferrari, G. Meredith, eds. Proc. of the6thInternational Conference on Coordination Models and Languages (COORDINATION2004),LNCS2949, Belin, Heidelberg: Springer-Verlag,2004.87-104.
[52] Bocchi L., Laneve C., Zavattaro G. A Calculus for Long-Running Transactions. In: E. Najm, U.Nestmann, P. Stevens, eds. Proc. of the6th IFIP International Conference on Formal Methods forOpen Object-Based Distributed Systems (FMOODS2003), LNCS2884, Belin, Heidelberg:Springer-Verlag,2003.124-138.
[53] Mazzara M., Lucchi R. A Framework for Generic Error Handling in Business Processes.Electronic Notes in Theoretical Computer Science,2004,105(10):133-145.
[54] Laneve C., Zavattaro G. Foundations of Web Transactions. In: Foundations of Software Scienceand Computational Structures,2005.282-298.
[55] Fischer J., Majumdar R. Ensuring consistency in long running transactions. In: Proceedings ofthe22nd IEEE/ACM international conference on Automated software engineering.2007.54-63.
[56] Lanese I., Vaz C., Ferreira C. On the expressive power of primitives for compensation handling.In: Proc. of the19th European conference on Programming Languages and Systems(ESOP'10).Springer-Verlag,2010.366-386.
[57] Anderson B. B., Hansen J. V., Lowry P. B., Summers S. L. The application of model checking forsecuring e-commerce transactions. Communications of the ACM,2006,49(6):97-101.
[58] Anderson B. B., Hansen J. V., Lowry P. B., Summers S. L. Standards and verification forfair-exchange and atomicity in e-commerce transactions. Information Sciences,2006,176(8):1045-1066.
[59] K nig D., Lohmann N., Moser S., Stahl C., Wolf K. Extending the compatibility notion forabstract WS-BPEL processes. In: Proc. of the17th international conference on World Wide Web.ACM,2008.785-794.
[60] Foster H., Uchitel S., Magee J., Kramer J. Tool Support for Model-Based Engineering of WebService Compositions. In: Proc. of the IEEE International Conference on Web Services. IEEEComputer Society,2005.95-102.
[61] Qi Z., Li M., Fu C., Shi D., You J. Membrane Calculus: a formal method for Grid transactions.Concurrency and Computation: Practice and Experience,2006,18(14):1799-1809.
[62] Liu Y., Müller S., Xu K. A static compliance-checking framework for business process models.IBM Systems Journal2007,46(2):335-361.
[63] Yuan M., Huang Z., Hu J., Li X., Zhu Y. Ensuring Coordination of Multi-business Interactions. In:Proc. of the6th IEEE International Conference on Services Computing (SCC2009). Washington,D. C.: IEEE Computer Society,2009.356-363.
[64] Yuan M., Huang Z., Li X., Yan Y. Towards a Formal Verification Approach for Business ProcessCoordination. In: Proc. of the8th IEEE International Conference on Web Services (ICWS2010).Washington, D. C.: IEEE Computer Society,2010.361-368.
[65] Victor B., Moller F. The Mobility Workbench-A Tool for the Pi-Calculus. In: D. L. Dill, ed. Proc.of the6th International Conference on Computer Aided Verification (CAV1994), LNCS818,Belin, Heidelberg: Springer-Verlag,1994.428-440.
[66] Ferrari G.-L., Gnesi S., Montanari U., Pistore M. A model-checking verification environment formobile processes. ACM Transactions on Software Engineering and Methodology,2003,12(4):440-473.
[67] OMG. XML Metadata Interchange (XMI), v2.0.2003. http://www.omg.org/cgi-bin/doc?formal/2003-05-02/03-05-02.pdf.
[68] Dalal S., Temel S., Little M., Potts M., Webber J. Coordinating business transactions on theweb. IEEE Internet Computing,2003,7(1):30-39.
[69] Bravetti M., Zavattaro G. Service oriented computing from a process algebraic perspective.Journal of Logic and Algebraic Programming,2007,70(1):3-14.
[70]董荣胜,古天龙.计算机科学与技术方法论.北京:人民邮电出版社,2002.132-147.
[71] Aalst W. M. P. v. d. Pi calculus versus Petri nets:Let us eat "humble pie" rather than further inflatethe "Pi hype". BP Trends,2005,3(5):1-11.
[72] Alrifai M., Dolog P., Balke W.-T., Nejdl W. Distributed Management of Concurrent Web ServiceTransactions. IEEE Transactions on Services Computing,2009,2(4):289-302.
[73]徐甲同,陆丽娜,谷建华.计算机操作系统教程.第2版,西安:西安电子科技大学出版社,2006.8-93.
[74]刘方方,史玉良,张亮,施伯乐.基于进程代数的Web服务合成的替换分析.计算机学报,2007,30(11):2033-2039.
[75] Roberts J., Srinivasan K. Tentative Hold Protocol Part1: White Paper.2001. http://www.w3.org/TR/tenthold-1/.
[76] Papazoglou M. P. Web Services: Principles and Technology. Boston: Pearson Prentice Hall,2007.
[77] Cardelli L., Gordon A. Mobile ambients. In: M. Nivat, ed. Foundations of Software Science andComputation Structures, Lecture Notes in Computer Science(LNCS)1378, New York:Springer-Verlag,1998.140-155.
[78]魏峻,冯玉琳.移动计算形式理论分析与研究.计算机研究与发展,2000,37(2):129-139.
[79] Vitek J., Castagna G. A calculus of secure mobile computations. In: Proc. of the IEEE Workshopon Internet Programming Languages(WIPL).1998.47-77.
[80]金龙飞,刘磊. Seal演算的偶图语义.计算机学报,2008,31(3):522-528.
[81] Milner R. Communicating and Mobile Systems: the π-Calculus. Cambridge: CambridgeUniversity Press,1999.
[82] Sangiorgi D., Walker D. The Pi-calculus: A Theory of Mobile Processes. Cambridge UniversityPress,2001.
[83]林惠民,柳欣欣,刘佳,屈楠.通信与移动系统:π演算.北京:清华大学出版社,2009.
[84] Sangiorgi D. A theory of bisimulation for the Pi-calculus. Acta informatica,1996,33(1):69-97.
[85] Hermanns H., Herzog U., Katoen J.-P. Process algebra for performance evaluation. TheoreticalComputer Science,2002,274(1-2):43-87.
[86] Moller F., Tofts C., Baeten J., Klop J. A temporal calculus of communicating systems. In:CONCUR '90Theories of Concurrency: Unification and Extension, Lecture Notes in ComputerScience(LNCS): Springer Berlin/Heidelberg,1990.401-415.
[87] Reed G. M., Roscoe A. W. A timed model for communicating sequential processes. TheoreticalComputer Science,1988,58(1-3):249-261.
[88] Clark A., Gilmore S., Hillston J., Tribastone M., Bernardo M. Stochastic Process Algebras. In:Formal Methods for Performance Evaluation, Lecture Notes in Computer Science(LNCS):Springer Berlin/Heidelberg,2007.132-179.
[89] Hermanns H., Herzog U., Mertsiotakis V. Stochastic process algebras\—between LOTOSand Markov chains. Computer Networks and ISDN Systems,1998,30(9-10):901-924.
[90] Hillston J. A compositional approach to performance modelling. Cambridge: CambridgeUniversity Press1996.
[91] Bernardo M., Gorrieri R. A tutorial on EMPA: A theory of concurrent processes withnondeterminism, priorities, probabilities and time. Theoretical Computer Science,1998,202(1-2):1-54.
[92] Lee I., Philippou A., Sokolsky O. Resources in process algebra. Journal of Logic and AlgebraicProgramming,2007,72(1):98-122.
[93] Bolognesi T. A conceptual framework for state-based and event-based formal behaviouralspecification languages. In: Proc. of the9th IEEE International Conference on EngineeringComplex Computer Systems. IEEE Computer Society,2004.107-116.
[94] Abadi M., Lamport L. Composing specifications. ACM Transactions on Programming Languagesand Systems (TOPLAS)1993,15(1):73-132.
[95] Guessarian I., De Nicola R., Vaandrager F. Action versus state based logics for transition systems.In: I. Guessarian, ed. Proc of the LITP Spring School on Theoretical Computer Science, LNCS469, Belin, Heidelberg: Springer-Verlag,1990.407-419.
[96] Hansen H., Virtanen H., Valmari A. Merging State-Based and Action-Based Verification. In:Proceedings of the Third International Conference on Application of Concurrency to SystemDesign(ACSD '03). IEEE Computer Society,2003.150-156
[97] ter Beek M., Fantechi A., Gnesi S., Mazzanti F., Leue S., Merino P. An Action/State-BasedModel-Checking Approach for the Analysis of Communication Protocols for Service-OrientedApplications. In: Formal Methods for Industrial Critical Systems, LNCS4916: Springer Berlin/Heidelberg,2008.133-148.
[98] Chaki S., Clarke E., Ouaknine J., Sharygina N., Sinha N., Boiten E., Derrick J., Smith G.State/Event-Based Software Model Checking. In: Integrated Formal Methods, Lecture Notes inComputer Science(LNCS)2999: Springer Berlin/Heidelberg,2004.128-147.
[99] Xu K., Wang Y., Wu C. Formal verification technique for grid service chain model and itsapplication. Science in China Series F: Information Sciences,2007,50(1):1-20.
[100] Xiao F., Huang Z., Cao Z., Hu J., Liu L., Yuan M. Unified Modelling Functional andNon-Functional Aspects of Web Services Composition Using PTCCS. International Journal ofWeb Services Research (IJWSR),2011,8(4):47-80.
[101] Jouault F., Kurtev I. Transforming models with ATL. In: Proc. of the Satellite Events on the8thInternational Conference on Model Driven Engineering Languages and Systems(MoDELS),LNCS3844: Springer Berlin/Heidelberg,2006.128-138.
[102] Nicola R. D., Vaandrager F. Three logics for branching bisimulation. Journal of the ACM,1995,42(2):458-487.
[103]李祥. Web服务事务协调协议WS-TX的形式化分析与验证,[硕士学位论文],南京:南京航空航天大学,2009.
[104] Liu Y., Müller S., Xu K. A static compliance-checking framework for business process models.IBM Systems Journal,2007,46(2):335-361.
[105]张天, JOUAULT F., ATTIOGBé C., BéZIVIN J.,李宣东.基于MDE的异构模型转换:从MARTE模型到FIACRE模型.软件学报,2007,20(2):214-233.
[106]何积丰,金芝,李宣东.面向服务的计算专刊前言.软件学报,2007,18(12):2965-2966.
[107] Jordan D., Evdemon J., Alves A., Arkin A., Askary S., Barreto C., Bloch B., Curbera F., Ford M.,Goland Y. Web services business process execution language (WSBPEL Version2.0).2007.
[108] Little M. A History of Extended Transactions.2006. http://www.infoq.com/articles/History-of-Extended-Transactions.
[109]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证.计算机学报,2005,28(4):635-643.
[110] Guidi C., Lucchi R., Mazzara M. A Formal Framework for Web Services Coordination. ElectronicNotes in Theoretical Computer Science,2007,180(2):55-70.
[111] Desai N., Chopra A. K., Singh M. P. Amoeba: A methodology for modeling and evolvingcross-organizational business processes. ACM Trans. Softw. Eng. Methodol.,2009,19(2):1-45.
[112] Yang Z., Liu C. Implementing a Flexible Compensation Mechanism for Business Processes inWeb Service Environment. In: Proc. of the IEEE International Conference on Web Services.IEEE Computer Society,2006.753-760.
[113] Sch fer M., Dolog P., Nejdl W. An environment for flexible advanced compensations of Webservice transactions. ACM Trans. Web,2008,2(2):1-36.
[114]乔晓强,魏峻,黄涛.基于分布式协调模型的服务协作方法研究.软件学报,2009,20(6):1470-1486.
[115] Victor B., Moller F. The mobility workbench: A tool for the pi-calculus. In: Proc. of the6th CAV.Berlin: Springer-Verlag,1994.428-440.
[116]戚正伟,尤晋元.基于细胞膜演算的Web服务事务处理形式化描述与验证.计算机学报,2006,29(7):1137-1141.
[117] Papazoglou M. P. Web Services and Business Transactions. World Wide Web,2003,6(1):49-91.
[118] Elmagarmid A. K., Leu Y., Litwin W., Rusinkiewicz M. A Multidatabase Transaction Model forInterBase. In: Proc. of the16th VLDB. Morgan Kaufmann Publishers Inc.,1990.507-518.
[119] Bouali A., Gnesi S., Larosa S. The Integration Project for the JACK Environment. Bulletin of theEATCS,1994,54.207-223.
[120] Bruni R., Melgratti H., Montanari U. Nested commits for mobile calculi:extending Join. In: Proc.of the3rd IFIP International Conference on Theoretical Computer Science.2004.569-582.
[121] Qiu Z. Y., Wang S. L., Pu G. G., Zhao X. P. Semantics of BPEL4WS-like fault and compensationhandling. In: Proc. of the13th International Symposium of Formal Methods Europe (FM2005),LNCS3582: Springer-Verlag,2005.350-365.
[122] Pu G., Zhu H., Qiu Z., Wang S., Zhao X., He J., Gorrieri R., Wehrheim H. TheoreticalFoundations of Scope-Based Compensable Flow Language for Web Service. In: FormalMethods for Open Object-Based Distributed Systems, LNCS4037: Springer Berlin/Heidelberg,2006.251-266.
[123] He J., Zhu H., Pu G. A model for BPEL-like languages. Frontiers of Computer Science in China,2007,1(1):9-19.
[124] Qi Z., Fu C., Shi D., You J., Li M., Jin H., Pan Y., Xiao N., Sun J. Membrane Calculus: A FormalMethod for Grid Transactions. In: Grid and Cooperative Computing(GCC2004), LNCS3251:Springer Berlin/Heidelberg,2004.73-80.
[125] Ho Y.-C., Pepyne D. L. Simple Explanation of the No Free Lunch Theorem of Optimization.Journal Cybernetics and Systems Analysis,2002,38(2):292-298.
[126] Cao J.-W., Zhang F., Xu K., Liu L.-C., Wu C. Formal Verification of Temporal Properties forReduced Overhead in Grid Scientific Workflows. Journal of Computer Science andTechnology,26(6):1017-1030.
[127] Ye C., Cheung S. C., Chan W. K., Xu C. Atomicity Analysis of Service Composition acrossOrganizations. IEEE Transactions on Software Engineering,2009,35(1):2-28.
[128] Srinivasan K., Malu P. G., Moakley G. Automatic Multibusiness Transactions. IEEE InternetComputing,2003,7(3):66-73.
[129] Roberts J., Collier T., Malu P., Srinivasan K. Tentative Hold Protocol Part2: TechnicalSpecification.2001. http://www.w3.org/TR/tenthold-2/.
[130] Park J., Choi K.-S. An adaptive coordination framework for fast atomic multi-businesstransactions using web services. Decision Support Systems,2006,42(3):1959-1973.
[131] Limthanmaphon B., Zhang Y. Web service composition transaction management. In: K.-D.Schewe, H. Williams, eds. Proc. of the15th Australasian database conference (ADC2004).Sydney: Australian Computer Society, Inc.,2004.171-179.
[132] Younas M., Li Y., Lo C.-C. An Efficient Transaction Commit Protocol for Composite WebServices. In: Proc. of the20th International Conference on Advanced Information Networkingand Applications (AINA2006). Washington, D. C.: IEEE Computer Society,2006.591-596.
[133] Gray J., Lamport L. Consensus on transaction commit. ACM Transactions on Database Systems2006,31(1):133-160.
[134]林惠民,张文辉.模型检测:理论、方法与应用.电子学报,2002,30(12A):1907-1912.
[135] Clarke E. M., Grumberg O., Long D. E. Model checking and abstraction. ACM Transactions onProgramming Languages and Systems,1994,16(5):1512-1542.
[136] Grumberg O., Long D. E. Model checking and modular verification. ACM Transactions onProgramming Languages and Systems,1994,16(3):843-871.
[137]文艳军,王戟,齐治昌.并发反应式系统的组合模型检验与组合精化检验.软件学报,2007,18(6):1270-1281.
[138] Berger M., Honda K. The Two-Phase Commitment Protocol in an Extended Pi-Calculus.Electronic Notes in Theoretical Computer Science,2003,39(1):21-46.
[139] Bocchi L., Laneve C., Zavattaro G. A calculus for long-running transactions. In: E. Najm, U.Nestmann, P. Stevens, eds. Proc. of the6th FMOODS. Springer-Verlag Berlin,2003.124-138.
[140] Ripon S. H. Process algebraic support for web service composition. ACM SIGSOFT SoftwareEngineering Notes,35(2):1-7.
[141] Tsai W. T., Malek M., Chen Y., Bastani F. Perspectives on Service-Oriented Computing andService-Oriented System Engineering. In: Proc. of the Second IEEE International Symposiumon Service-Oriented System Engineering (SOSE2006). IEEE Computer Society,2006.3-10.
[142] W3C. Web Services Policy1.5-Framework.2007. http://www.w3.org/TR/2007/REC-ws-policy-20070904/.
[143]蔡维德,白晓颖,陈以农.浅谈深析面向服务的软件工程.北京:清华大学出版社,2008.41-108.
[144] Parr T. The Definitive ANTLR Reference: Building Domain-Specific Languages. Lewisville:Pragmatic Bookshelf,2007.
[145] The GUI edition for NuSMV2(gNuSMV).2002. http://nusmv.fbk.eu/gnusmv/.
[146] Cleaveland R., Sims S. The NCSU Concurrency Workbench. In: Proceedings of the8thInternational Conference on Computer Aided Verification(CAV '96). Springer-Verlag,1996.394-397.
[2] Gray J., Reuter A. Transaction Processing: Concepts and Techniques. Morgan Kaufmann,1993.4-5.
[3] Thomas E. Service-Oriented Architecture: A Field Guide to Integrating XML and Web Services.Prentice Hall,2004.
[4] Singh M. P., Huhns M. N. Service-Oriented Computing: Semantics, Processes, Agents. JohnWiley&Sons, Ltd.,2005.
[5]喻坚,韩燕波.面向服务的计算--原理和应用.北京:清华大学出版社,2006.178-191.
[6] Tsai W. T. Service-Oriented System Engineering: A New Paradigm. In: Proc. of IEEEInternational Workshop on Service-Oriented System Engineering (SOSE). IEEE ComputerSociety,2005.3-8.
[7]韩燕波.《面向服务的计算》专辑介绍.计算机学报,2006,26(07):3-4.
[8]任怡,吴泉源,贾焰.事务处理技术研究综述.计算机研究与发展,2005,42(10):136-141.
[9] Bjork L. A., Davies J. C. T. The Semantics of the Preservation and Recovery of Integrity in a DataSystem. IBM General Products Division, TR02.540,1972.
[10] Bjork L. A. Recovery scenario for a DB/DC system. In: Proc. of the ACM annual conference.ACM,1973.142-146.
[11] Davies J. C. T. Data processing spheres of control. IBM Systems Journal,1978,17(2):179-198.
[12] Elmagarmid A. K. Database Transaction Models for Advanced Applications. Morgan Kaufmann,1992.
[13] Eliot J., Moss B. Nested transactions: an introduction. In: K. B. Bharat, ed. Concurrency controland reliability in distributed systems: Van Nostrand Reinhold Co.,1987.395-425.
[14] Weikum G. Principles and realization strategies of multilevel transaction management. ACMTransactions on Database Systems (TODS),1991,16(1):132-180.
[15] Garcia-Molina H., Salem K. Sagas. In: Proc. of the ACM international conference onManagement of data (SIGMOD).1987.249-259.
[16] Pu C., Kaiser G. E., Hutchinson N. C. Split-Transactions for Open-Ended Activities. In: Proc. ofthe14th International Conference on Very Large Data Bases(VLDB). Morgan KaufmannPublishers Inc.,1988.26-37.
[17] Bukhres O. A., Elmagarmid A. K., Kühn e. Implementation of the Flex Transaction Model. IEEEData Engineering Bulletin,1993,16(2):28-32.
[18] Zhang A., Nodine M., Bhargava B. Global Scheduling for Flexible Transactions in HeterogeneousDistributed Database Systems. IEEE Transactions on Knowledge and Data Engineering,2001,13(3):439-450.
[19]唐飞龙,李明禄,曹健.一个Web服务事务处理模型:结构、算法和事务补偿.电子学报,2003,31(12A):2074-2078.
[20]任怡,吴泉源,戴华东,吴庆波.一种基于QoS的事务工作流并发调度算法.电子学报,2007,35(4):621-628.
[21] Huang T., Ding X., Wei J. An application-semantics-based relaxed transaction model forinternetware. Science in China Series F: Information Sciences,2006,49(6):774-791.
[22] Sheth A. P., Rusinkiewicz M. On Transactional Workflows IEEE Data Engineering Bulletin,1993,16(2):37-40.
[23] Hagen C., Alonso G. Exception Handling in Workflow Management Systems. IEEE Transactionson Software Engineering,2000,26(10):943-958.
[24] Curbera F., Khalaf R., Mukhi N., Tai S., Weerawarana S. The next step in Web services.Communications of the ACM,2003,46(10):29-34.
[25] Jordan D., Evdemon J., Alves A., Arkin A., Askary S., Barreto C., Bloch B., Curbera F., Ford M.,Goland Y., Web services business process execution language, version2.0, OASIS Standard, May2007.
[26] Little M., Freund T., Feingold M., Robinson I. Web Services Transaction (WS-TX Version1.2).Feb.2009.
[27] Wang W., Hidvégi Z., Bailey A. D., Whinston A. B. E-process design and assurance using modelchecking. Computer,2000,33(10):48-53.
[28] Fu X., Bultan T., Su J. Analysis of interacting BPEL web services. In: Proc. of the13thinternational conference on World Wide Web(WWW '04).2004.621-630.
[29] Fu X., Bultan T., Su J. WSAT: A Tool for Formal Analysis of Web Services. In: Computer AidedVerification, LNCS3114: Springer Berlin/Heidelberg,2004.394-395.
[30] Pu G., Zhao X., Wang S., Qiu Z. Towards the Semantics and Verification of BPEL4WS.Electronic Notes in Theoretical Computer Science (ENTCS),2006,151(2):33-52.
[31] Foster H., Uchitel S., Magee J., Kramer J. Compatibility Verification for Web ServiceChoreography. In: Proceedings of the IEEE International Conference on Web Services(ICWS'04). IEEE Computer Society,2004.738-741.
[32] Magee J., Kramer J. Concurrency-State Models&Java Programs.2edition: John Wiley,2006.
[33] Foster H., Uchitel S., Magee J., Kramer J. LTSA-WS: a tool for model-based verification of webservice compositions and choreography. In: Proceedings of the28th international conference onSoftware engineering(ICSE '06). ACM,2006.771-774.
[34] Aalst W. M. P. v. d. Modeling and Analyzing Interorganizational Workflows. In: Proc. of theInternational Conference on Application of Concurrency to System Design(ACSD'98). IEEEComputer Society,1998.262-272.
[35] Aalst W. M. P. v. d., Hee K. M. v. Workflow Management: Models, Methods, and Systems.Cambridge: MIT Press,2004.
[36] Aalst W. M. P. v. d. The Application of Petri Nets to Workflow Management. Journal of CircuitsSystems and Computers,1998,8(1):21-66.
[37] Aalst W. M. P. v. d. Verification of Workflow Nets. In: Proc. of the18th InternationalConference on Application and Theory of Petri Nets. Springer-Verlag,1997.407-426.
[38] Sun P., Jiang C. Analysis of workflow dynamic changes based on Petri net. Information andSoftware Technology,2009,51(2):284-292.
[39] Cicirelli F., Furfaro A., Nigro L. A service-based architecture for dynamically reconfigurableworkflows. Journal of Systems and Software,83(7):1148-1164.
[40] Hamadi R., Benatallah B. A Petri net-based model for web service composition. In: Proc. of the14th Australasian database conference(ADC '03). Australian Computer Society, Inc.,2003.191-200.
[41] Ouyang C., Verbeek E., van der Aalst W., Breutel S., Dumas M., ter Hofstede A. WofBPEL: ATool for Automated Analysis of BPEL Processes. In: Service-Oriented Computing-ICSOC2005, LNCS3826: Springer Berlin/Heidelberg,2005.484-489.
[42] Valero V. n., Cambronero M. E., D′az G., Macià H. A Petri net approach for the design andanalysis of Web Services Choreographies. Journal of Logic and Algebraic Programming,2009,78(5):359-380.
[43]范贵生,虞慧群,陈丽琼,刘冬梅.基于Petri网的服务组合故障诊断与处理.软件学报,2010,21(02):231-247.
[44]唐飞龙,李明禄,黄哲学,王卓立.服务网格中的事务服务及基于Petri网的正确性分析.计算机学报,2005,28(04):667-676.
[45] Hoare C. A. R. Communicating sequential processes. Communications of the ACM,1978,21(8):666-677.
[46] Milner R. A Calculus of Communicating Systems. New York: Springer-Verlag,1982.
[47] Milner R., Parrow J., Walker D. A calculus of mobile processes. Part I/II. Information andComputation,1992,100(1):1-77.
[48] Momtahan L., Martin A., Roscoe A. W. A Taxonomy of Web Services Using CSP. ElectronicNotes in Theoretical Computer Science,2006,151(2):71-87.
[49] Brogi A., Canal C., Pimentel E., Vallecillo A. Formalizing Web Service Choreographies.Electronic Notes in Theoretical Computer Science,2004,105.73-94.
[50] Cámara J., Canal C., Cubo J., Vallecillo A. Formalizing WSBPEL Business Processes UsingProcess Algebra. Electronic Notes in Theoretical Computer Science,2006,154(1):159-173.
[51] Butler M., Ferreira C. An operational semantics for StAC, a language for modelling long-runningbusiness transactions. In: R. D. Nicola, G.-L. Ferrari, G. Meredith, eds. Proc. of the6thInternational Conference on Coordination Models and Languages (COORDINATION2004),LNCS2949, Belin, Heidelberg: Springer-Verlag,2004.87-104.
[52] Bocchi L., Laneve C., Zavattaro G. A Calculus for Long-Running Transactions. In: E. Najm, U.Nestmann, P. Stevens, eds. Proc. of the6th IFIP International Conference on Formal Methods forOpen Object-Based Distributed Systems (FMOODS2003), LNCS2884, Belin, Heidelberg:Springer-Verlag,2003.124-138.
[53] Mazzara M., Lucchi R. A Framework for Generic Error Handling in Business Processes.Electronic Notes in Theoretical Computer Science,2004,105(10):133-145.
[54] Laneve C., Zavattaro G. Foundations of Web Transactions. In: Foundations of Software Scienceand Computational Structures,2005.282-298.
[55] Fischer J., Majumdar R. Ensuring consistency in long running transactions. In: Proceedings ofthe22nd IEEE/ACM international conference on Automated software engineering.2007.54-63.
[56] Lanese I., Vaz C., Ferreira C. On the expressive power of primitives for compensation handling.In: Proc. of the19th European conference on Programming Languages and Systems(ESOP'10).Springer-Verlag,2010.366-386.
[57] Anderson B. B., Hansen J. V., Lowry P. B., Summers S. L. The application of model checking forsecuring e-commerce transactions. Communications of the ACM,2006,49(6):97-101.
[58] Anderson B. B., Hansen J. V., Lowry P. B., Summers S. L. Standards and verification forfair-exchange and atomicity in e-commerce transactions. Information Sciences,2006,176(8):1045-1066.
[59] K nig D., Lohmann N., Moser S., Stahl C., Wolf K. Extending the compatibility notion forabstract WS-BPEL processes. In: Proc. of the17th international conference on World Wide Web.ACM,2008.785-794.
[60] Foster H., Uchitel S., Magee J., Kramer J. Tool Support for Model-Based Engineering of WebService Compositions. In: Proc. of the IEEE International Conference on Web Services. IEEEComputer Society,2005.95-102.
[61] Qi Z., Li M., Fu C., Shi D., You J. Membrane Calculus: a formal method for Grid transactions.Concurrency and Computation: Practice and Experience,2006,18(14):1799-1809.
[62] Liu Y., Müller S., Xu K. A static compliance-checking framework for business process models.IBM Systems Journal2007,46(2):335-361.
[63] Yuan M., Huang Z., Hu J., Li X., Zhu Y. Ensuring Coordination of Multi-business Interactions. In:Proc. of the6th IEEE International Conference on Services Computing (SCC2009). Washington,D. C.: IEEE Computer Society,2009.356-363.
[64] Yuan M., Huang Z., Li X., Yan Y. Towards a Formal Verification Approach for Business ProcessCoordination. In: Proc. of the8th IEEE International Conference on Web Services (ICWS2010).Washington, D. C.: IEEE Computer Society,2010.361-368.
[65] Victor B., Moller F. The Mobility Workbench-A Tool for the Pi-Calculus. In: D. L. Dill, ed. Proc.of the6th International Conference on Computer Aided Verification (CAV1994), LNCS818,Belin, Heidelberg: Springer-Verlag,1994.428-440.
[66] Ferrari G.-L., Gnesi S., Montanari U., Pistore M. A model-checking verification environment formobile processes. ACM Transactions on Software Engineering and Methodology,2003,12(4):440-473.
[67] OMG. XML Metadata Interchange (XMI), v2.0.2003. http://www.omg.org/cgi-bin/doc?formal/2003-05-02/03-05-02.pdf.
[68] Dalal S., Temel S., Little M., Potts M., Webber J. Coordinating business transactions on theweb. IEEE Internet Computing,2003,7(1):30-39.
[69] Bravetti M., Zavattaro G. Service oriented computing from a process algebraic perspective.Journal of Logic and Algebraic Programming,2007,70(1):3-14.
[70]董荣胜,古天龙.计算机科学与技术方法论.北京:人民邮电出版社,2002.132-147.
[71] Aalst W. M. P. v. d. Pi calculus versus Petri nets:Let us eat "humble pie" rather than further inflatethe "Pi hype". BP Trends,2005,3(5):1-11.
[72] Alrifai M., Dolog P., Balke W.-T., Nejdl W. Distributed Management of Concurrent Web ServiceTransactions. IEEE Transactions on Services Computing,2009,2(4):289-302.
[73]徐甲同,陆丽娜,谷建华.计算机操作系统教程.第2版,西安:西安电子科技大学出版社,2006.8-93.
[74]刘方方,史玉良,张亮,施伯乐.基于进程代数的Web服务合成的替换分析.计算机学报,2007,30(11):2033-2039.
[75] Roberts J., Srinivasan K. Tentative Hold Protocol Part1: White Paper.2001. http://www.w3.org/TR/tenthold-1/.
[76] Papazoglou M. P. Web Services: Principles and Technology. Boston: Pearson Prentice Hall,2007.
[77] Cardelli L., Gordon A. Mobile ambients. In: M. Nivat, ed. Foundations of Software Science andComputation Structures, Lecture Notes in Computer Science(LNCS)1378, New York:Springer-Verlag,1998.140-155.
[78]魏峻,冯玉琳.移动计算形式理论分析与研究.计算机研究与发展,2000,37(2):129-139.
[79] Vitek J., Castagna G. A calculus of secure mobile computations. In: Proc. of the IEEE Workshopon Internet Programming Languages(WIPL).1998.47-77.
[80]金龙飞,刘磊. Seal演算的偶图语义.计算机学报,2008,31(3):522-528.
[81] Milner R. Communicating and Mobile Systems: the π-Calculus. Cambridge: CambridgeUniversity Press,1999.
[82] Sangiorgi D., Walker D. The Pi-calculus: A Theory of Mobile Processes. Cambridge UniversityPress,2001.
[83]林惠民,柳欣欣,刘佳,屈楠.通信与移动系统:π演算.北京:清华大学出版社,2009.
[84] Sangiorgi D. A theory of bisimulation for the Pi-calculus. Acta informatica,1996,33(1):69-97.
[85] Hermanns H., Herzog U., Katoen J.-P. Process algebra for performance evaluation. TheoreticalComputer Science,2002,274(1-2):43-87.
[86] Moller F., Tofts C., Baeten J., Klop J. A temporal calculus of communicating systems. In:CONCUR '90Theories of Concurrency: Unification and Extension, Lecture Notes in ComputerScience(LNCS): Springer Berlin/Heidelberg,1990.401-415.
[87] Reed G. M., Roscoe A. W. A timed model for communicating sequential processes. TheoreticalComputer Science,1988,58(1-3):249-261.
[88] Clark A., Gilmore S., Hillston J., Tribastone M., Bernardo M. Stochastic Process Algebras. In:Formal Methods for Performance Evaluation, Lecture Notes in Computer Science(LNCS):Springer Berlin/Heidelberg,2007.132-179.
[89] Hermanns H., Herzog U., Mertsiotakis V. Stochastic process algebras\—between LOTOSand Markov chains. Computer Networks and ISDN Systems,1998,30(9-10):901-924.
[90] Hillston J. A compositional approach to performance modelling. Cambridge: CambridgeUniversity Press1996.
[91] Bernardo M., Gorrieri R. A tutorial on EMPA: A theory of concurrent processes withnondeterminism, priorities, probabilities and time. Theoretical Computer Science,1998,202(1-2):1-54.
[92] Lee I., Philippou A., Sokolsky O. Resources in process algebra. Journal of Logic and AlgebraicProgramming,2007,72(1):98-122.
[93] Bolognesi T. A conceptual framework for state-based and event-based formal behaviouralspecification languages. In: Proc. of the9th IEEE International Conference on EngineeringComplex Computer Systems. IEEE Computer Society,2004.107-116.
[94] Abadi M., Lamport L. Composing specifications. ACM Transactions on Programming Languagesand Systems (TOPLAS)1993,15(1):73-132.
[95] Guessarian I., De Nicola R., Vaandrager F. Action versus state based logics for transition systems.In: I. Guessarian, ed. Proc of the LITP Spring School on Theoretical Computer Science, LNCS469, Belin, Heidelberg: Springer-Verlag,1990.407-419.
[96] Hansen H., Virtanen H., Valmari A. Merging State-Based and Action-Based Verification. In:Proceedings of the Third International Conference on Application of Concurrency to SystemDesign(ACSD '03). IEEE Computer Society,2003.150-156
[97] ter Beek M., Fantechi A., Gnesi S., Mazzanti F., Leue S., Merino P. An Action/State-BasedModel-Checking Approach for the Analysis of Communication Protocols for Service-OrientedApplications. In: Formal Methods for Industrial Critical Systems, LNCS4916: Springer Berlin/Heidelberg,2008.133-148.
[98] Chaki S., Clarke E., Ouaknine J., Sharygina N., Sinha N., Boiten E., Derrick J., Smith G.State/Event-Based Software Model Checking. In: Integrated Formal Methods, Lecture Notes inComputer Science(LNCS)2999: Springer Berlin/Heidelberg,2004.128-147.
[99] Xu K., Wang Y., Wu C. Formal verification technique for grid service chain model and itsapplication. Science in China Series F: Information Sciences,2007,50(1):1-20.
[100] Xiao F., Huang Z., Cao Z., Hu J., Liu L., Yuan M. Unified Modelling Functional andNon-Functional Aspects of Web Services Composition Using PTCCS. International Journal ofWeb Services Research (IJWSR),2011,8(4):47-80.
[101] Jouault F., Kurtev I. Transforming models with ATL. In: Proc. of the Satellite Events on the8thInternational Conference on Model Driven Engineering Languages and Systems(MoDELS),LNCS3844: Springer Berlin/Heidelberg,2006.128-138.
[102] Nicola R. D., Vaandrager F. Three logics for branching bisimulation. Journal of the ACM,1995,42(2):458-487.
[103]李祥. Web服务事务协调协议WS-TX的形式化分析与验证,[硕士学位论文],南京:南京航空航天大学,2009.
[104] Liu Y., Müller S., Xu K. A static compliance-checking framework for business process models.IBM Systems Journal,2007,46(2):335-361.
[105]张天, JOUAULT F., ATTIOGBé C., BéZIVIN J.,李宣东.基于MDE的异构模型转换:从MARTE模型到FIACRE模型.软件学报,2007,20(2):214-233.
[106]何积丰,金芝,李宣东.面向服务的计算专刊前言.软件学报,2007,18(12):2965-2966.
[107] Jordan D., Evdemon J., Alves A., Arkin A., Askary S., Barreto C., Bloch B., Curbera F., Ford M.,Goland Y. Web services business process execution language (WSBPEL Version2.0).2007.
[108] Little M. A History of Extended Transactions.2006. http://www.infoq.com/articles/History-of-Extended-Transactions.
[109]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证.计算机学报,2005,28(4):635-643.
[110] Guidi C., Lucchi R., Mazzara M. A Formal Framework for Web Services Coordination. ElectronicNotes in Theoretical Computer Science,2007,180(2):55-70.
[111] Desai N., Chopra A. K., Singh M. P. Amoeba: A methodology for modeling and evolvingcross-organizational business processes. ACM Trans. Softw. Eng. Methodol.,2009,19(2):1-45.
[112] Yang Z., Liu C. Implementing a Flexible Compensation Mechanism for Business Processes inWeb Service Environment. In: Proc. of the IEEE International Conference on Web Services.IEEE Computer Society,2006.753-760.
[113] Sch fer M., Dolog P., Nejdl W. An environment for flexible advanced compensations of Webservice transactions. ACM Trans. Web,2008,2(2):1-36.
[114]乔晓强,魏峻,黄涛.基于分布式协调模型的服务协作方法研究.软件学报,2009,20(6):1470-1486.
[115] Victor B., Moller F. The mobility workbench: A tool for the pi-calculus. In: Proc. of the6th CAV.Berlin: Springer-Verlag,1994.428-440.
[116]戚正伟,尤晋元.基于细胞膜演算的Web服务事务处理形式化描述与验证.计算机学报,2006,29(7):1137-1141.
[117] Papazoglou M. P. Web Services and Business Transactions. World Wide Web,2003,6(1):49-91.
[118] Elmagarmid A. K., Leu Y., Litwin W., Rusinkiewicz M. A Multidatabase Transaction Model forInterBase. In: Proc. of the16th VLDB. Morgan Kaufmann Publishers Inc.,1990.507-518.
[119] Bouali A., Gnesi S., Larosa S. The Integration Project for the JACK Environment. Bulletin of theEATCS,1994,54.207-223.
[120] Bruni R., Melgratti H., Montanari U. Nested commits for mobile calculi:extending Join. In: Proc.of the3rd IFIP International Conference on Theoretical Computer Science.2004.569-582.
[121] Qiu Z. Y., Wang S. L., Pu G. G., Zhao X. P. Semantics of BPEL4WS-like fault and compensationhandling. In: Proc. of the13th International Symposium of Formal Methods Europe (FM2005),LNCS3582: Springer-Verlag,2005.350-365.
[122] Pu G., Zhu H., Qiu Z., Wang S., Zhao X., He J., Gorrieri R., Wehrheim H. TheoreticalFoundations of Scope-Based Compensable Flow Language for Web Service. In: FormalMethods for Open Object-Based Distributed Systems, LNCS4037: Springer Berlin/Heidelberg,2006.251-266.
[123] He J., Zhu H., Pu G. A model for BPEL-like languages. Frontiers of Computer Science in China,2007,1(1):9-19.
[124] Qi Z., Fu C., Shi D., You J., Li M., Jin H., Pan Y., Xiao N., Sun J. Membrane Calculus: A FormalMethod for Grid Transactions. In: Grid and Cooperative Computing(GCC2004), LNCS3251:Springer Berlin/Heidelberg,2004.73-80.
[125] Ho Y.-C., Pepyne D. L. Simple Explanation of the No Free Lunch Theorem of Optimization.Journal Cybernetics and Systems Analysis,2002,38(2):292-298.
[126] Cao J.-W., Zhang F., Xu K., Liu L.-C., Wu C. Formal Verification of Temporal Properties forReduced Overhead in Grid Scientific Workflows. Journal of Computer Science andTechnology,26(6):1017-1030.
[127] Ye C., Cheung S. C., Chan W. K., Xu C. Atomicity Analysis of Service Composition acrossOrganizations. IEEE Transactions on Software Engineering,2009,35(1):2-28.
[128] Srinivasan K., Malu P. G., Moakley G. Automatic Multibusiness Transactions. IEEE InternetComputing,2003,7(3):66-73.
[129] Roberts J., Collier T., Malu P., Srinivasan K. Tentative Hold Protocol Part2: TechnicalSpecification.2001. http://www.w3.org/TR/tenthold-2/.
[130] Park J., Choi K.-S. An adaptive coordination framework for fast atomic multi-businesstransactions using web services. Decision Support Systems,2006,42(3):1959-1973.
[131] Limthanmaphon B., Zhang Y. Web service composition transaction management. In: K.-D.Schewe, H. Williams, eds. Proc. of the15th Australasian database conference (ADC2004).Sydney: Australian Computer Society, Inc.,2004.171-179.
[132] Younas M., Li Y., Lo C.-C. An Efficient Transaction Commit Protocol for Composite WebServices. In: Proc. of the20th International Conference on Advanced Information Networkingand Applications (AINA2006). Washington, D. C.: IEEE Computer Society,2006.591-596.
[133] Gray J., Lamport L. Consensus on transaction commit. ACM Transactions on Database Systems2006,31(1):133-160.
[134]林惠民,张文辉.模型检测:理论、方法与应用.电子学报,2002,30(12A):1907-1912.
[135] Clarke E. M., Grumberg O., Long D. E. Model checking and abstraction. ACM Transactions onProgramming Languages and Systems,1994,16(5):1512-1542.
[136] Grumberg O., Long D. E. Model checking and modular verification. ACM Transactions onProgramming Languages and Systems,1994,16(3):843-871.
[137]文艳军,王戟,齐治昌.并发反应式系统的组合模型检验与组合精化检验.软件学报,2007,18(6):1270-1281.
[138] Berger M., Honda K. The Two-Phase Commitment Protocol in an Extended Pi-Calculus.Electronic Notes in Theoretical Computer Science,2003,39(1):21-46.
[139] Bocchi L., Laneve C., Zavattaro G. A calculus for long-running transactions. In: E. Najm, U.Nestmann, P. Stevens, eds. Proc. of the6th FMOODS. Springer-Verlag Berlin,2003.124-138.
[140] Ripon S. H. Process algebraic support for web service composition. ACM SIGSOFT SoftwareEngineering Notes,35(2):1-7.
[141] Tsai W. T., Malek M., Chen Y., Bastani F. Perspectives on Service-Oriented Computing andService-Oriented System Engineering. In: Proc. of the Second IEEE International Symposiumon Service-Oriented System Engineering (SOSE2006). IEEE Computer Society,2006.3-10.
[142] W3C. Web Services Policy1.5-Framework.2007. http://www.w3.org/TR/2007/REC-ws-policy-20070904/.
[143]蔡维德,白晓颖,陈以农.浅谈深析面向服务的软件工程.北京:清华大学出版社,2008.41-108.
[144] Parr T. The Definitive ANTLR Reference: Building Domain-Specific Languages. Lewisville:Pragmatic Bookshelf,2007.
[145] The GUI edition for NuSMV2(gNuSMV).2002. http://nusmv.fbk.eu/gnusmv/.
[146] Cleaveland R., Sims S. The NCSU Concurrency Workbench. In: Proceedings of the8thInternational Conference on Computer Aided Verification(CAV '96). Springer-Verlag,1996.394-397.