服务计算中接口模型与构件设计的研究
|
摘要
面向服务计算(Service-Oriented Computing,SOC)是一种新的计算范型,SOC在流程描述、数据管理以及分布式计算中间件技术的基础上,提出以服务作为构建软件的基本单元。SOC希望通过统一的技术规范,来达到网络资源的充分利用和共享,从而提高IT企业应对需求的能力和工作效率。
服务接口是SOC中服务使用者关于一个服务所能够得到的唯一信息,准确而且充分的服务接口描述是保证SOC中服务查找、服务组合等关键操作质量的重要因素。因此,如何保证接口描述的准确性,如何在服务接口描述中包含多方面的服务信息成为SOC中的关键问题。形式化方法基于严格的数学理论来提供系统的描述和分析方法,不仅能够消除系统建模过程中的不准确或歧义性,而且还能通过形式化验证来保证系统的正确性,提高系统的质量。本文希望通过研究形式化的服务接口模型及验证方法,来保证服务接口的准确性。
事务是SOC中保证系统正确性和一致性非常重要的手段,SOC中的事务往往执行时间较长,需要与不同的服务提供组织协商完成,与传统事务相比,SOC中的事务对原子性和隔离性的要求相对松弛,因此SOC中一般使用长事务模型来完成具备事务要求的任务。本文针对具备长事务特征服务的接口描述,在Beyer等人提出的Web服务接口理论的基础上,提出了支持长事务行为特征描述的多层接口模型,能够分别在特征、会话和协议三个层次描述支持后向恢复长事务机制的服务在接口层面的动作引发关系。在每层接口模型的基础上,给出了基于接口的服务相容性和可替换性的检查方法。此外,为了保证服务接口的正确性,分别在三个层次给出了服务接口关键性质的规约方法和相应的验证方法。
为了支持日益复杂的业务逻辑,出现了更加灵活的长事务模型,并且在目前主流的服务编制语言中都得到了体现。针对目前长事务模型中的前向恢复、事务嵌套以及可订制错误处理这些特征,本文提出了扩展协议接口来描述具备这些特征的服务接口。基于时序逻辑,给出了一般化的协议接口关键性质的规约方法,通过扩展协议接口的操作语义,采用模型检验这种形式化技术来验证扩展协议接口是否满足协议规约。为了应用扩展协议接口及验证方法,本文针对使用Web服务业务流程执行语言(BPEL)实现的服务,给出了从BPEL程序中提取扩展协议接口的方法,并使用验证方法对提取的扩展协议接口进行验证。在扩展协议接口、提取方法以及验证方法基础上,给出了它们在BPEL程序基本开发过程中的应用方式,从而可以在开发过程中验证BPEL程序,提高使用BPEL实现服务的质量。
服务构件作为提供服务的计算实体,是SOC中服务提供方在服务开发过程中需要构建的主要单元。如何在开发过程中设计服务构件并保证服务构件的可靠性是提高服务质量、保证面向服务系统正确性的关键问题。与服务接口类似,本文希望通过研究形式化的服务构件建模技术以及精化方法,并在目前主流的模型驱动以及形式化验证技术基础上,寻求严格的服务构件设计方法,来提高服务构件的可靠性。
本文在何积丰等人提出的构件以及对象精化理论的基础上,针对目前SOC中服务的异常行为,提出了支持异常信息描述的接口契约模型,可以支持服务接口的功能规约、服务使用方式以及异常信息多个方面的描述,并给出了不同方面行为的一致性条件,以及接口契约的数据精化方法。针对服务构件实现层面的事务特征,提出了支持补偿恢复机制的服务构件实现模型,并给出了服务构件相容性的定义。针对具备事务特征的应用,提出了支持后向恢复长事务描述的进程构件模型,用于服务构件之间的复杂组合。服务构件理论为服务构件的设计提供了理论基础,支持从接口契约到构件层面的精化,为进一步的应用形式化验证技术提供了前提。
在服务构件理论的基础上,本文研究了严格的服务构件设计方法,受关注点分离(Separation of Concerns)设计思想启发,在现有模型驱动、面向对象以及面向构件理论和技术的基础上,提出了迭代以及增量式的模型驱动的服务构件设计方法,其中包括需求建模、功能设计、逻辑构件设计以及详细设计四个阶段,在每个阶段使用服务构件理论中提供的建模元素对服务构件进行建模,基于精化理论给出了服务构件设计过程中的精化方法,同时在不同的阶段使用相应的形式化验证技术保证系统模型的正确性和一致性,从而提高了服务构件的可靠性。
本文最后设计并实现了接口模型的检查工具,可以对文本格式的多层接口描述进行检查和验证,同时把扩展协议接口的验证嵌入到开源的BPEL设计工具中,可以在BPEL设计过程中对其进行验证。此外,本文还设计并实现了服务构件设计工具原型,支持服务构件设计过程中的图形建模、静态和动态一致性检查、基于文本模型的自动精化等主要设计活动。
Service-Oriented Computing (SOC) is a new computing paradigm, which isevolved from the techniques of process description, data management and distrib-uted computing middleware. In SOC, service is the basic unit for building software.Through unified technical specifications, SOC hopes to maximally utilize and sharethe network accessible resources.
A service interface is the only information that the users of a service in SOCcan get about the service. Accuracy and su?ciency of the information in serviceinterfaces are very important to the key operations in SOC such as service discoveryand service composition. How to ensure the accuracy of an interface and incorpo-rate more information in it are critical issues in SOC. Formal Methods provide themethods of system specification and analysis based on the rigorous mathematicaltheories. By using the theories and techniques in Formal Methods, we can not onlyeliminate the inaccuracy and ambiguity in the system modeling process, but alsoensure the correctness of a system by formal verification to improve the system qual-ity. This thesis tends to ensure the accuracy of service interfaces by studying formalservice interface models and their verification methods.
Transaction is a very important method to ensure the correctness and consis-tency of a system in SOC. The transactions in SOC usually last for a long time, andneed to negotiate with di?erent organizations that provide services. The require-ments of atomicity and isolation in the transactions in SOC are relaxed comparedto those of the traditional transaction. Long Running Transaction (LRT) is oftenused in SOC to accomplish the tasks with transaction requirements. Based on theexisting Web Service interface theory by Beyer et al., we propose a multi-level inter-face model for describing the interfaces of services having LRT features. The actioncausality relation of the interface representing a service, in which there are LRTs us-ing backward recovery, can be specified by using the interface model on three levels,i.e., signature, conversation and protocol. The methods for checking compatibilityand substitutivity relations of services based on interfaces are proposed with respectto our interface model. In addition, we present the specification and verification methods for critical properties on each interface level to ensure the correctness ofservice interfaces.
To cope with the increasing complexity of business logic, some more ?exibleLRT models appear, and many are supported by the current de factor service or-chestration languages. A formalism, called extended protocol interface, is proposedto support describing the interfaces of services that have LRT features of forward re-covery, nested transaction and user-defined fault handing. The general specificationmethod for critical properties of protocol interface is presented based on temporallogic. Through the operational semantics of the extended protocol interface, we canverify the satisfaction of an extended protocol interface to a protocol specification byusing model checking technique. To apply the extended protocol interface and theverification method to the services implemented with Web Service Business ProcessExecution Language (BPEL), this thesis presents a method for extracting an ex-tended protocol interface from a BPEL program, and uses the verification methodto verify the extracted extended protocol interface. Based on the interface model,the extraction method and the verification method, we give their usages in the basicBPEL development process for verifying BPEL program to improve the quality ofservices implemented with BPEL.
As the computing entity providing services, service component is the main unitto build in the service development process for the service providers in SOC. How todesign service components and ensure their correctness are critical issues to improvethe service quality and ensure the correctness of the system in SOC. Similar tothe service interface, this thesis tries to study the formal modeling and refinementtechniques of service component, and find the rigorous design method for servicecomponent based on the current model driven and formal verification techniques toimprove the system reliability.
Based the refinement theory for component and object systems by He Jifenget al., we propose an interface contract model supporting the description of exceptioninformation with respect to the exception behavior in SOC. The interface contractmodel can contain the interface information of function specification, service invo-cation protocols and exceptions. In addition, the consistency conditions betweendi?erent aspects and the data refinement method of an interface contract are given. To support the transaction feature in the implementation of service component, wepropose a service component implementation model supporting compensation basedrecovery mechanism, and the compatibility between service components is defined.Considering the application with transaction features, we present a process compo-nent model supporting LRT using backward recovery for the complex compositionof service components. The theory of service component provides a theoretical basefor the design of service component. The refinement from service interface contractto service component is supported, and the formal service component models givethe promise for the application of formal verification techniques.
By using the service component theory, this thesis studies the rigorous designmethod for service component. Aspired by the ideas of“Separation of Concerns”, wepropose an iterative and incremental model driven service component design methodbased on the current model driven, object-oriented and component-oriented theoriesand techniques. The design method contains four stages, i.e., requirement modeling,function design, logic component design and detailed design, and the modeling ele-ments in the service component theory are used in each of these stages. To improvethe service component reliability, the designer can not only use the refinement the-ory based refinement method in the design process, but also the formal verificationtechniques in the appropriate stages to ensure the correctness and consistency of thesystem models.
We design and implement an interface checking tool, which can check and verifythe textual interface models, and the verification tool for the extended protocol in-terface is integrated into an open source BPEL design tool to verify BPEL programsduring the design process. In addition, we design and implement a prototype of thetool for service component design, which supports the main design activities in thedesign process such as graphical modeling, static and dynamic consistency checkingand textual model-based automatic refinement.
服务接口是SOC中服务使用者关于一个服务所能够得到的唯一信息,准确而且充分的服务接口描述是保证SOC中服务查找、服务组合等关键操作质量的重要因素。因此,如何保证接口描述的准确性,如何在服务接口描述中包含多方面的服务信息成为SOC中的关键问题。形式化方法基于严格的数学理论来提供系统的描述和分析方法,不仅能够消除系统建模过程中的不准确或歧义性,而且还能通过形式化验证来保证系统的正确性,提高系统的质量。本文希望通过研究形式化的服务接口模型及验证方法,来保证服务接口的准确性。
事务是SOC中保证系统正确性和一致性非常重要的手段,SOC中的事务往往执行时间较长,需要与不同的服务提供组织协商完成,与传统事务相比,SOC中的事务对原子性和隔离性的要求相对松弛,因此SOC中一般使用长事务模型来完成具备事务要求的任务。本文针对具备长事务特征服务的接口描述,在Beyer等人提出的Web服务接口理论的基础上,提出了支持长事务行为特征描述的多层接口模型,能够分别在特征、会话和协议三个层次描述支持后向恢复长事务机制的服务在接口层面的动作引发关系。在每层接口模型的基础上,给出了基于接口的服务相容性和可替换性的检查方法。此外,为了保证服务接口的正确性,分别在三个层次给出了服务接口关键性质的规约方法和相应的验证方法。
为了支持日益复杂的业务逻辑,出现了更加灵活的长事务模型,并且在目前主流的服务编制语言中都得到了体现。针对目前长事务模型中的前向恢复、事务嵌套以及可订制错误处理这些特征,本文提出了扩展协议接口来描述具备这些特征的服务接口。基于时序逻辑,给出了一般化的协议接口关键性质的规约方法,通过扩展协议接口的操作语义,采用模型检验这种形式化技术来验证扩展协议接口是否满足协议规约。为了应用扩展协议接口及验证方法,本文针对使用Web服务业务流程执行语言(BPEL)实现的服务,给出了从BPEL程序中提取扩展协议接口的方法,并使用验证方法对提取的扩展协议接口进行验证。在扩展协议接口、提取方法以及验证方法基础上,给出了它们在BPEL程序基本开发过程中的应用方式,从而可以在开发过程中验证BPEL程序,提高使用BPEL实现服务的质量。
服务构件作为提供服务的计算实体,是SOC中服务提供方在服务开发过程中需要构建的主要单元。如何在开发过程中设计服务构件并保证服务构件的可靠性是提高服务质量、保证面向服务系统正确性的关键问题。与服务接口类似,本文希望通过研究形式化的服务构件建模技术以及精化方法,并在目前主流的模型驱动以及形式化验证技术基础上,寻求严格的服务构件设计方法,来提高服务构件的可靠性。
本文在何积丰等人提出的构件以及对象精化理论的基础上,针对目前SOC中服务的异常行为,提出了支持异常信息描述的接口契约模型,可以支持服务接口的功能规约、服务使用方式以及异常信息多个方面的描述,并给出了不同方面行为的一致性条件,以及接口契约的数据精化方法。针对服务构件实现层面的事务特征,提出了支持补偿恢复机制的服务构件实现模型,并给出了服务构件相容性的定义。针对具备事务特征的应用,提出了支持后向恢复长事务描述的进程构件模型,用于服务构件之间的复杂组合。服务构件理论为服务构件的设计提供了理论基础,支持从接口契约到构件层面的精化,为进一步的应用形式化验证技术提供了前提。
在服务构件理论的基础上,本文研究了严格的服务构件设计方法,受关注点分离(Separation of Concerns)设计思想启发,在现有模型驱动、面向对象以及面向构件理论和技术的基础上,提出了迭代以及增量式的模型驱动的服务构件设计方法,其中包括需求建模、功能设计、逻辑构件设计以及详细设计四个阶段,在每个阶段使用服务构件理论中提供的建模元素对服务构件进行建模,基于精化理论给出了服务构件设计过程中的精化方法,同时在不同的阶段使用相应的形式化验证技术保证系统模型的正确性和一致性,从而提高了服务构件的可靠性。
本文最后设计并实现了接口模型的检查工具,可以对文本格式的多层接口描述进行检查和验证,同时把扩展协议接口的验证嵌入到开源的BPEL设计工具中,可以在BPEL设计过程中对其进行验证。此外,本文还设计并实现了服务构件设计工具原型,支持服务构件设计过程中的图形建模、静态和动态一致性检查、基于文本模型的自动精化等主要设计活动。
Service-Oriented Computing (SOC) is a new computing paradigm, which isevolved from the techniques of process description, data management and distrib-uted computing middleware. In SOC, service is the basic unit for building software.Through unified technical specifications, SOC hopes to maximally utilize and sharethe network accessible resources.
A service interface is the only information that the users of a service in SOCcan get about the service. Accuracy and su?ciency of the information in serviceinterfaces are very important to the key operations in SOC such as service discoveryand service composition. How to ensure the accuracy of an interface and incorpo-rate more information in it are critical issues in SOC. Formal Methods provide themethods of system specification and analysis based on the rigorous mathematicaltheories. By using the theories and techniques in Formal Methods, we can not onlyeliminate the inaccuracy and ambiguity in the system modeling process, but alsoensure the correctness of a system by formal verification to improve the system qual-ity. This thesis tends to ensure the accuracy of service interfaces by studying formalservice interface models and their verification methods.
Transaction is a very important method to ensure the correctness and consis-tency of a system in SOC. The transactions in SOC usually last for a long time, andneed to negotiate with di?erent organizations that provide services. The require-ments of atomicity and isolation in the transactions in SOC are relaxed comparedto those of the traditional transaction. Long Running Transaction (LRT) is oftenused in SOC to accomplish the tasks with transaction requirements. Based on theexisting Web Service interface theory by Beyer et al., we propose a multi-level inter-face model for describing the interfaces of services having LRT features. The actioncausality relation of the interface representing a service, in which there are LRTs us-ing backward recovery, can be specified by using the interface model on three levels,i.e., signature, conversation and protocol. The methods for checking compatibilityand substitutivity relations of services based on interfaces are proposed with respectto our interface model. In addition, we present the specification and verification methods for critical properties on each interface level to ensure the correctness ofservice interfaces.
To cope with the increasing complexity of business logic, some more ?exibleLRT models appear, and many are supported by the current de factor service or-chestration languages. A formalism, called extended protocol interface, is proposedto support describing the interfaces of services that have LRT features of forward re-covery, nested transaction and user-defined fault handing. The general specificationmethod for critical properties of protocol interface is presented based on temporallogic. Through the operational semantics of the extended protocol interface, we canverify the satisfaction of an extended protocol interface to a protocol specification byusing model checking technique. To apply the extended protocol interface and theverification method to the services implemented with Web Service Business ProcessExecution Language (BPEL), this thesis presents a method for extracting an ex-tended protocol interface from a BPEL program, and uses the verification methodto verify the extracted extended protocol interface. Based on the interface model,the extraction method and the verification method, we give their usages in the basicBPEL development process for verifying BPEL program to improve the quality ofservices implemented with BPEL.
As the computing entity providing services, service component is the main unitto build in the service development process for the service providers in SOC. How todesign service components and ensure their correctness are critical issues to improvethe service quality and ensure the correctness of the system in SOC. Similar tothe service interface, this thesis tries to study the formal modeling and refinementtechniques of service component, and find the rigorous design method for servicecomponent based on the current model driven and formal verification techniques toimprove the system reliability.
Based the refinement theory for component and object systems by He Jifenget al., we propose an interface contract model supporting the description of exceptioninformation with respect to the exception behavior in SOC. The interface contractmodel can contain the interface information of function specification, service invo-cation protocols and exceptions. In addition, the consistency conditions betweendi?erent aspects and the data refinement method of an interface contract are given. To support the transaction feature in the implementation of service component, wepropose a service component implementation model supporting compensation basedrecovery mechanism, and the compatibility between service components is defined.Considering the application with transaction features, we present a process compo-nent model supporting LRT using backward recovery for the complex compositionof service components. The theory of service component provides a theoretical basefor the design of service component. The refinement from service interface contractto service component is supported, and the formal service component models givethe promise for the application of formal verification techniques.
By using the service component theory, this thesis studies the rigorous designmethod for service component. Aspired by the ideas of“Separation of Concerns”, wepropose an iterative and incremental model driven service component design methodbased on the current model driven, object-oriented and component-oriented theoriesand techniques. The design method contains four stages, i.e., requirement modeling,function design, logic component design and detailed design, and the modeling ele-ments in the service component theory are used in each of these stages. To improvethe service component reliability, the designer can not only use the refinement the-ory based refinement method in the design process, but also the formal verificationtechniques in the appropriate stages to ensure the correctness and consistency of thesystem models.
We design and implement an interface checking tool, which can check and verifythe textual interface models, and the verification tool for the extended protocol in-terface is integrated into an open source BPEL design tool to verify BPEL programsduring the design process. In addition, we design and implement a prototype of thetool for service component design, which supports the main design activities in thedesign process such as graphical modeling, static and dynamic consistency checkingand textual model-based automatic refinement.
引文
[1]中国大百科全书, 1986
[2]杨芙清.软件工程技术发展思索.软件学报. 2005, 16(1):1–7
[3] Mike P. Papazoglou, Paolo Traverso, Schahram Dustdar, Frank Leymann. Service-Oriented Computing: a Research Roadmap. Int J Cooperative Inf Syst. 2008,17(2):223–255
[4] Thomas Erl. Service-Oriented Architecture: Concepts, Technology, and Design.Upper Saddle River, NJ, USA: Prentice Hall PTR, 2005
[5] Christopher H. Lovelock, Jochen Wirtz. Services Marketing. Prentice Hall Profes-sional Technical Reference, 2007, 6th edn.
[6] Humberto Cervantes, Richard S. Hall. Service-Oriented Software System Engineer-ing: Challenges and Practices, Idea Group Publishing, 2005. 1–47
[7] Mark Turner, David Budgen, Pearl Brereton. Turning Software into a Service. IEEEComputer. 2003, 36(10):38–44
[8] Roy W. Schulte, Yefim V. Natisy.“Service Oriented”Architectures, Part 1 and 2.Garter Research Note SPA-401-068 and SPA-401-069, 1996
[9] Mark Endrei, Jenny Ang, Ali Arsanjani, Sook Chua, Philippe Comte, Pal Krog-dahl, Min Luo, Tony Newling. Patterns: Service-Oriented Architecture and WebServicece. IBM Redbooks, 2004
[10] D. Stratton. The OMG CORBA Trader Service. Tech. rep., School of InformationTechnology and Mathematical Sciences, University of Ballarat, Australia, 1998
[11] Inc. Sun Microsystems. Extensible Runtime Containment and Services Protocol forJavaBeans, 1998
[12] Ken Arnold, Robert Schei?er, Jim Waldo, Bryan O’Sullivan, Ann Wollrath. JiniSpecification. Addison-Wesley Longman Publishing Co., Inc., 1999
[13] The OSGi Alliance. OSGi Service Platform Specification, 2007. Release 4, URLhttp://www.osgi.org/Release4/Download
[14] David Booth, Hugo Haas, Francis Mccabe, Eric Newcomer, Michael Champion,Chris Ferris, David Orchard. Web Services Architecture. Tech. rep., World WideWeb Consortium, February 2004. URL http://www.w3.org/TR/ws-arch/
[15] Alexandre Alves, Assaf Arkin, Sid Askary, Ben Bloch, Francisco Curbera, YaronGoland, Neelakantan Kartha, Sterling, Dieter K¨onig, Vinkesh Mehta, Satish Thatte,Danny van der Rijn, Prasad Yendluri, Alex Yiu. Web Services Business ProcessExecution Language Version 2.0. OASIS Committee Draft, May 2006
[16] Rania Khalaf, Nirmal Mukhi, Sanjiva Weerawarana. Service-Oriented Compositionin BPEL4WS. WWW (Alternate Paper Tracks). 2003
[17] Wil M. P. van der Aalst, Marlon Dumas, Arthur H. M. ter Hofstede. Web Ser-vice Composition Languages: Old Wine in New Bottles? EUROMICRO. IEEEComputer Society, 2003, 298–307
[18] Petia Wohed, Wil M. P. van der Aalst, Marlon Dumas, Arthur H. M. ter Hofstede.Analysis of Web Services Composition Languages: The Case of BPEL4WS. Il-Yeol Song, Stephen W. Liddle, Tok Wang Ling, Peter Scheuermann, (Editors) ER.Springer, 2003, vol. 2813 of Lecture Notes in Computer Science, 200–215
[19] Nickolas Kavantzas, David Burdett, Greg Ritzinger, Tony Fletcher, Yves Lafon,Charlton Barreto. Web Services Choreography Description Language Version 1.0.World Wide Web Consortium, Candidate Recommandation CR-ws-cdl-10-20051109,nov 2005. URL http://www.w3.org/TR/2005/CR-ws-cdl-10-20051109
[20] Luc Clement, Andrew Hately, Claus von Riegen, Tony Rogers. UDDIVersion 3.0.2. Organization for the Advancement of Structured Informa-tion Standards, UDDI Spec Technical Committee Draft, oct 2004. URLhttp://uddi.org/pubs/uddi-v3.0.2-20041019.htm
[21] Asir S. Vedamuthu, David Orchard, Frederick Hirsch, Maryann Hondo,Prasad Yendluri, Toufic Boubez, U¨mit Yalc??nalp. Web Services Pol-icy 1.5—Guidelines for Policy Assertion Authors. World Wide WebConsortium, Note NOTE-ws-policy-guidelines-20071112, nov 2007. URLhttp://www.w3.org/TR/2007/NOTE-ws-policy-guidelines-20071112
[22] OASIS WSS TC. WS-Security Core Specification 1.1, Nov 2006. URLhttp://www.oasis-open.org/committees/tc home.php?wg abbrev=wss
[23] William Cox, Felipe Cabrera, George Copeland, Tom Freund, JohannesKlein, Tony Storey, Satish Thatte. Web Services Transactions specifications.IBM, BEA Systems, Microsoft, Arjuna, Hitachi, IONA, Aug 2005. URLhttp://www.ibm.com/developerworks/library/specification/ws-tx/
[24] DMTF open standards. Web Services for Management (WS-Management), 2008.URL http://www.dmtf.org/standards/wsman/
[25] Ian Sommerville. Software Engineering. Addison Wesley, 2006, 8th edn.
[26] Mike P. Papazoglou, Paolo Traverso, Schahram Dustdar, Frank Leymann. Service-Oriented Computing: State of the Art and Research Challenges. IEEE Computer.2007, 40(11):38–45
[27]岳昆,王晓玲,周傲英. Web服务核心支撑技术:研究综述.软件学报. 2004,15(3):428 442
[28] Richard Hull, Michael Benedikt, Vassilis Christophides, Jianwen Su. E-services: alook behind the curtain. PODS. ACM, 2003, 1–14
[29] Hongbing Wang, Joshua Zhexue Huang, Yuzhong Qu, Junyuan Xie. Web services:problems and future directions. J Web Sem. 2004, 1(3):309–320
[30] Richard Hull, Jianwen Su. Tools for composite web services: a short overview.SIGMOD Record. 2005, 34(2):86–95
[31] Schahram Dustdar, Wolfgang Schreiner. A survey on web services composition.IJWGS. 2005, 1(1):1–30
[32] B. Srivastava, J. Koehler. Web Service Composition, Current Solutions and OpenProblems. Workshop on Planning for Web Services (ICAPS). 2003
[33] Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger. Web service interfaces.Ellis and Hagino [184], 148–159
[34] Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger. An Interface Formalismfor Web Services. Proceedings of the First International Workshop on Foundationsof Interface Technologies (FIT 2005, San Francisco, CA, August 21). 2005. URLhttp://infoscience.epfl.ch/search?recid=114605&ln=en
[35] Jifeng He, Xiaoshan Li, Zhiming Liu. A Theory of Reactive Components. ElectrNotes Theor Comput Sci. 2006, 160:173–195
[36] Jifeng He, Zhiming Liu, Xiaoshan Li. rCOS: A refinement calculus of object sys-tems. Theor Comput Sci. 2006, 365(1-2):109–142. UNU-IIST TR 322, URLhttp://rcos.iist.unu.edu/publications/TCSpreprint.pdf
[37] Jia Zhang, Jen-Yao Chung, Carl K. Chang, Seongwoon Kim. WS-Net: A Petri-netBased Specification Model for Web Services. ICWS [185], 420–427
[38] Jinghai Rao, Peep Ku¨ngas, Mihhail Matskin. Application of Linear Logic to WebService Composition. Liang-Jie Zhang, (Editor) ICWS. CSREA Press, 2003, 3–10
[39] Jinghai Rao, Peep Ku¨ngas, Mihhail Matskin. Logic-based Web Services Composi-tion: From Service Description to Process Model. ICWS [185], 446–453
[40] Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Mas-simo Mecella. Automatic Composition of E-services That Export Their Behavior.Maria E. Orlowska, Sanjiva Weerawarana, Mike P. Papazoglou, Jian Yang, (Editors)ICSOC. Springer, 2003, vol. 2910 of Lecture Notes in Computer Science, 43–58
[41] Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo, Richard Hull, MassimoMecella. Automatic Composition of Web Services in Colombo. Andrea Cal`?, DiegoCalvanese, Enrico Franconi, Maurizio Lenzerini, Letizia Tanca, (Editors) SEBD.2005, 8–15
[42] Xiang Fu, Tevfik Bultan, Jianwen Su. Analysis of interacting BPEL web services.Stuart I. Feldman, Mike Uretsky, Marc Najork, Craig E. Wills, (Editors) WWW.ACM, 2004, 621–630
[43] Raman Kazhamiakin, Marco Pistore. A Parametric Communication Model for theVerification of BPEL4WS Compositions. Bravetti et al. [186], 318–332
[44] Aysu Betin-Can, Tevfik Bultan, Xiang Fu. Design for verification for asynchronouslycommunicating Web services. Ellis and Hagino [184], 750–759
[45] Raman Kazhamiakin, Marco Pistore, Luca Santuari. Analysis of communicationmodels in web service compositions. Les Carr, David De Roure, Arun Iyengar,Carole A. Goble, Michael Dahlin, (Editors) WWW. ACM, 2006, 267–276
[46] Aysu Betin-Can, Tevfik Bultan. Verifiable Web Services with Hierarchical Interfaces.ICWS [187], 85–94
[47] Daniel Brand, Pitro Zafiropulo. On Communicating Finite-State Machines. J ACM.1983, 30(2):323–342
[48] Wenfei Fan, Floris Geerts, Wouter Gelade, Frank Neven, Antonella Poggi. Com-plexity and composition of synthesized web services. Maurizio Lenzerini, DomenicoLembo, (Editors) PODS. ACM, 2008, 231–240
[49] Rachid Hamadi, Boualem Benatallah. A Petri Net-based Model for Web ServiceComposition. Klaus-Dieter Schewe, Xiaofang Zhou, (Editors) ADC. AustralianComputer Society, 2003, vol. 17 of CRPIT, 191–200
[50] Zhihong Ren, Jiannong Cao, Alvin T. S. Chan, Jing Li. Toward a Formal Approachto Composite Web Service Construction and Automation. ICPP. IEEE ComputerSociety, 2003, 436–443
[51] Boualem Benatallah, Fabio Casati, Farouk Toumani, Rachid Hamadi. ConceptualModeling of Web Service Conversations. Johann Eder, Michele Missiko?, (Editors)CAiSE. Springer, 2003, vol. 2681 of Lecture Notes in Computer Science, 449–467
[52] Daniela Berardi, Fabio De Rosa, Luca De Santis, Massimo Mecella. Finite StateAutomata As Conceptual Model For E-Services. J Integr Des Process Sci. 2004,8(2):105–121
[53] Rajeev Alur, David L. Dill. A Theory of Timed Automata. Theor Comput Sci.1994, 126(2):183–235
[54] Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo, Richard Hull, MassimoMecella. Automatic Composition of Transition-based Semantic Web Services withMessaging. Klemens B¨ohm, Christian S. Jensen, Laura M. Haas, Martin L. Kersten,Per-A?ke Larson, Beng Chin Ooi, (Editors) VLDB. ACM, 2005, 613–624
[55] Alin Deutsch, Liying Sui, Victor Vianu. Specification and verification of data-drivenWeb applications. J Comput Syst Sci. 2007, 73(3):442–474
[56] Jing Liu, Jifeng He, Zhiming Liu. A strategy for service realization in service-oriented design. Science in China Series F: Information Sciences. 2006, 49(6):864–884
[57] C.A.R. Hoare, He Jifeng. Unifying Theories of Programming. Prentice Hall, 1998
[58] Chris Peltz. Web Services Orchestration and Choreography. IEEE Computer. 2003,36(10):46–52
[59] Roozbeh Farahbod, Uwe Gl¨asser, Mona Vajihollahi. Specification and Validationof the Business Process Execution Language for Web Services. Wolf Zimmermann,Bernhard Thalheim, (Editors) Abstract State Machines. Springer, 2004, vol. 3052of Lecture Notes in Computer Science, 78–94
[60] Dirk Fahland. Complete Abstract Operational Semantics for the Web Service Busi-ness Process Execution Languages. Informatik-Berichte 190, Humboldt-Universita¨tzu Berlin, 2005
[61] Andreas Wombacher, Peter Fankhauser, Erich J. Neuhold. Transforming BPEL intoAnnotated Deterministic Finite State Automata for Service Discovery. ICWS [185],316–323
[62] M. Koshkina, F. van Breugel. Verification of Business Processes for Web Ser-vices. Technical report CS-2003-11, York University, Oct. 2003. Available from:http://www.cs.yorku.ca/techreports/2003/
[63] Javier C′amara, Carlos Canal, Javier Cubo, Antonio Vallecillo. Formalizing WS-BPEL Business Processes Using Process Algebra. Electr Notes Theor Comput Sci.2006, 154(1):159–173
[64] Howard Foster, Sebasti′an Uchitel, Je? Magee, Je? Kramer. Model-based Verificationof Web Service Compositions. ASE. IEEE Computer Society, 2003, 152–163
[65] Roberto Lucchi, Manuel Mazzara. A pi-calculus based semantics for WS-BPEL. JLog Algebr Program. 2007, 70(1):96–118
[66] Andrea Ferrara. Web Services: A Process Algebra Approach. CoRR. 2004,cs.AI/0406055
[67] R. Milner. A Calculus of Communicating Systems. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1982
[68] Franck van Breugel, Mariya Koshkina. Dead-Path-Elimination in BPEL4WS.ACSD. IEEE Computer Society, 2005, 192–201
[69] Robin Milner. Communicating and mobile systems: theπ-calculus. New York, NY,USA: Cambridge University Press, 1999
[70] T. Bolognesi, E. Brinksma. Introduction to the ISO specification language LOTOS.Comput Netw ISDN Syst. 1987, 14(1):25–59
[71] YanPing Yang, QingPing Tan, JinShan Yu, Feng Liu. Transformation BPEL toCP-Nets for Verifying Web Services Composition. NWESP’05: Proceedings of theInternational Conference on Next Generation Web Services Practices. Washington,DC, USA: IEEE Computer Society, 2005, 137
[72] W.M.P. van der Aalst H.M.W. Verbeek. Analyzing BPEL processes using Petrinets. Proceedings of 2nd International Workshop on Applications of Petri Nets toCoordination, Work?ow and Business Process Management. 2005
[73] Chun Ouyang, Eric Verbeek, Wil M. P. van der Aalst, Stephan Breutel, MarlonDumas, Arthur H. M. ter Hofstede. Formal semantics and analysis of control ?owin WS-BPEL. Sci Comput Program. 2007, 67(2-3):162–198
[74] Hongli Yang, Xiangpeng Zhao, Zongyan Qiu, Geguang Pu, Shuling Wang. A FormalModel forWeb Service Choreography Description Language (WS-CDL). ICWS’06:Proceedings of the IEEE International Conference on Web Services. Washington,DC, USA: IEEE Computer Society, 2006, 893–894
[75] Roberto Gorrieri, Claudio Guidi, Roberto Lucchi. Reasoning About InteractionPatterns in Choreography. Bravetti et al. [186], 333–348
[76] Antonio Brogi, Carlos Canal, Ernesto Pimentel, Antonio Vallecillo. FormalizingWeb Service Choreographies. Electr Notes Theor Comput Sci. 2004, 105:73–94
[77] James E. Johnson, David E. Langworthy, Leslie Lamport, Friedrich H. Vogt. Formalspecification of a Web services protocol. J Log Algebr Program. 2007, 70(1):34–52
[78] Zongyan Qiu, Shuling Wang, Geguang Pu, Xiangpeng Zhao. Semantics ofBPEL4WS-Like Fault and Compensation Handling. John Fitzgerald, Ian J. Hayes,Andrzej Tarlecki, (Editors) FM. Springer, 2005, vol. 3582 of Lecture Notes in Com-puter Science, 350–365
[79] Michael J. Butler, Carla Ferreira, Muan Yong Ng. Precise Modelling of Compensat-ing Business Transactions and its Application to BPEL. J UCS. 2005, 11(5):712–743
[80] Geguang Pu, Huibiao Zhu, Zongyan Qiu, Shuling Wang, Xiangpeng Zhao, JifengHe. Theoretical Foundations of Scope-Based Compensable Flow Language for WebService. FMOODS. 2006, 251–266
[81] Roberto Bruni, Hern′an C. Melgratti, Ugo Montanari. Theoretical foundations forcompensations in ?ow composition languages. Jens Palsberg, Mart′?n Abadi, (Edi-tors) POPL. ACM, 2005, 209–220
[82] Luciano Baresi, Reiko Heckel, Sebastian Th¨one, D′aniel Varr′o. Modeling and val-idation of service-oriented architectures: application vs. style. ESEC / SIGSOFTFSE. 2003, 68–77
[83] Juanjuan Jiang, Tarja Syst¨a. UML-Based Modeling and Validity Checking of WebService Descriptions. ICWS [187], 453–460
[84] Piyush Maheshwari, Sharon Si-Long Tam. Events-Based Exception Handling inSupply Chain Management using Web Services. AICT/ICIW. IEEE Computer So-ciety, 2006, 151
[85] Marco Pistore, Paolo Traverso, Piergiorgio Bertoli, Annapaola Marconi. AutomatedSynthesis of Composite BPEL4WS Web Services. ICWS [187], 293–301
[86] Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri.NUSMV: A New Symbolic Model Checker. STTT. 2000, 2(4):410–425
[87] P. Bertoli, A. Cimatti, M. Pistore, M. Roveri, P. Traverso. MBP: a Model BasedPlanner. Proc of the IJCAI’01 Workshop on Planning under Uncertainty and In-complete Information. 2001
[88] Ziyang Duan, Arthur J. Bernstein, Philip M. Lewis, Shiyong Lu. Semantics BasedVerification and Synthesis of BPEL4WS Abstract Processes. ICWS [185], 734–737
[89] C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Commun ACM.1969, 12(10):576–580
[90] Gerard J. Holzmann. The Model Checker SPIN. IEEE Trans Software Eng. 1997,23(5):279–295
[91] Howard Foster, Sebasti′an Uchitel, Je? Magee, Je? Kramer. Compatibility Verifica-tion for Web Service Choreography. ICWS [185], 738–741
[92] Gwen Salau¨n, Lucas Bordeaux, Marco Schaerf. Describing and Reasoning on WebServices using Process Algebra. ICWS [185], 43–50
[93] Srini Narayanan, Sheila A. McIlraith. Simulation, verification and automated com-position of web services. WWW. 2002, 77–88
[94] Xiaochuan Yi, Krys Kochut. A CP-nets-based Design and Verification Frameworkfor Web Services Composition. ICWS [185], 756–760
[95] Mark H. Burstein, Jerry R. Hobbs, Ora Lassila, David L. Martin, Drew V. Mc-Dermott, Sheila A. McIlraith, Srini Narayanan, Massimo Paolucci, Terry R. Payne,Katia P. Sycara. DAML-S: Web Service Description for the Semantic Web. IanHorrocks, James A. Hendler, (Editors) International Semantic Web Conference.Springer, 2002, vol. 2342 of Lecture Notes in Computer Science, 348–363
[96] Yanping Yang, QingPing Tan, Yong Xiao, Jinshan Yu, Feng Liu. Verifying Web Ser-vices Composition: A Transformation-Based Approach. PDCAT. IEEE ComputerSociety, 2005, 546–548
[97] Yuhong Yan, Marie-Odile Cordier, Yannick Pencol′e, Alban Grastien. MonitoringWeb Service Networks in a Model-based Approach. ECOWS. IEEE Computer So-ciety, 2005, 192–203
[98] Geguang Pu, Xiangpeng Zhao, Shuling Wang, Zongyan Qiu. Towards the Semanticsand Verification of BPEL4WS. Electr Notes Theor Comput Sci. 2006, 151(2):33–52
[99] Gregorio D′?az, Juan Jos′e Pardo, Mar′?a-Emilia Cambronero, Valentin Valero, Fer-nando Cuartero. Verification of Web Services with Timed Automata. Electr NotesTheor Comput Sci. 2006, 157(2):19–34
[100] K.G. Larsen, P. Pettersson, W. Yi. UPPAAL in a Nutshell. STTT. 1997, 1(1-2):134–152
[101] Shin Nakajima. Model-Checking Verification for Reliable Web Service. OOPSLA2002 Workshop on Object-Oriented Web Services. 2002
[102] F. Leymann. Web Services Flow Language (WSFL). IBM Corp. 2001
[103] Wei-Tek Tsai, Yinong Chen, Raymond A. Paul, Ning Liao, Hai Huang. Cooperativeand Group Testing in Verification of Dynamic Composite Web Services. COMPSACWorkshops. IEEE Computer Society, 2004, 170–173
[104] Wei-Tek Tsai, Raymond A. Paul, Zhibin Cao, Lian Yu, Akihiro Saimi, BingnanXiao. Verification of Web Services Using an Enhanced UDDI Server. WORDS.IEEE Computer Society, 2003, 131–138
[105] Hai Huang, Wei-Tek Tsai, Raymond A. Paul, Yinong Chen. Automated ModelChecking and Testing for Composite Web Services. ISORC. IEEE Computer Society,2005, 300–307
[106] Lerina Aversano, Marcello Bruno, Massimiliano Di Penta, Amedeo Falanga, RitaScognamiglio. Visualizing the Evolution of Web Services using Formal ConceptAnalysis. IWPSE. IEEE Computer Society, 2005, 57–60
[107] Olaf Zimmermann, Pal Krogdahl, Clive Gee. Elements ofService-Oriented Analysis and Design, June 2004. URLhttp://www.ibm.com/developerworks/webservices/library/ws-soad1/
[108] Olaf Zimmermann, Niklas Schlimm, Gu¨nter Waller, Marc Pestel. Analysis and De-sign Techniques for Service-Oriented Development and Integration. Armin B. Cre-mers, Rainer Manthey, Peter Martini, Volker Steinhage, (Editors) GI Jahrestagung(2). GI, 2005, vol. 68 of LNI, 606–611
[109] Ali Arsanjani, Shuvanker Ghosh, Abdul Allam, Tina Abdollah, SellaGanapathy, Kerrie Holley. SOMA: A method for developing service-oriented solutions. IBM Systems Journal. 2008, 47(3):377–396. URLhttp://www.research.ibm.com/journal/sj/473/arsanjani.pdf
[110] Liang-Jie Zhang, Nianjun Zhou, Yi-Min Chee, Ahamed Jalaldeen,Karthikeyan Ponnalagu, Renuka R. Sindhgatta, Ali Arsanjani, FaustaBernardini. SOMA-ME: A platform for the model-driven design ofSOA solutions. IBM Systems Journal. 2008, 47(3):397–413. URLhttp://www.research.ibm.com/journal/sj/473/zhang.pdf
[111] Mike P. Papazoglou, Willem-Jan van den Heuvel. Service-oriented design and de-velopment methodology. Int J Web Eng Technol. 2006, 2(4):412–442
[112] Christian Emig, Karsten Krutz, Stefan Link, Christof Momm, Sebas-tian Abeck. Model-Driven Development of SOA Services, 2007. URLhttp://digbib.ubka.uni-karlsruhe.de/volltexte/1000008043
[113] J. K. Strosnider, P. Nandi, S. Kumaran, S. Ghosh, A. Arsanjani. Model-driven synthesis of SOA solutions. IBM Systems Journal. 2008, 47. URLhttp://www.research.ibm.com/journal/sj/473/strosnider.html
[114] Uwe Zdun, Schahram Dustdar. Model-driven and pattern-based integration ofprocess-driven SOA models. International Journal of Business Process Integrationand Management. 2007, 2(2):109–119
[115] Olaf Zimmermann, Uwe Zdun, Thomas Gschwind, Frank Leymann. CombiningPattern Languages and Reusable Architectural Decision Models into a Comprehen-sive and Comprehensible Design Method. WICSA. IEEE Computer Society, 2008,157–166
[116] Ateret Anaby-Tavor, David Amid, Aviad Sela, Amit Fisher, Kuo Zhang, Ou Tie Jun.Towards a Model Driven Service Engineering Process. SERVICES’08: Proceedingsof the 2008 IEEE Congress on Services - Part I. Washington, DC, USA: IEEEComputer Society, 2008, 503–510
[117] Olaf Zimmermann, Jana Koehler, Leymann Frank. Architectural Decision Modelsas Micro-Methodology for Service-Oriented Analysis and Design. Daniel Lu¨bke,(Editor) Proceedings of the Workshop on Software Engineering Methods for Service-oriented Architecture 2007 (SEMSOA 2007), Hannover, Germany. 2007, 46–60
[118] Remco M. Dijkman, Marlon Dumas. Service-Oriented Design: A Multi-ViewpointApproach. Int J Cooperative Inf Syst. 2004, 13(4):337–368
[119] Aliaksei Yanchuk, Alexander Ivanyukovich, Maurizio Marchese. A Lightweight For-mal Framework for Service-Oriented Applications Design. Boualem Benatallah,Fabio Casati, Paolo Traverso, (Editors) ICSOC. Springer, 2005, vol. 3826 of LectureNotes in Computer Science, 545–551
[120] Nikola Milanovic. Service Engineering Design Patterns. Elisabetta Di Nitto, RobertJ. Hall, Jun Han, Yanbo Han, Andrea Polini, Kurt Sandkuhl, Andrea Zisman,(Editors) SOSE. IEEE Computer Society, 2006, 19–26
[121] Ervin Ramollari, Dimitris Dranidis, Anthony J. H. Simons. A Survey of ServiceOriented Development Methodologies. Proceedings of the 2nd European YoungResearchers Workshop on Service Oriented Computing. 2007
[122] Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda, Cristina VideiraLopes, Jean-Marc Loingtier, John Irwin. Aspect-Oriented Programming. ECOOP.1997, 220–242
[123] Nancy A. Lynch, Mark R. Tuttle. An introduction to input/output automata. CWIQuarterly. 1989, 2:219–246
[124] Luca de Alfaro, Thomas A. Henzinger. Interface automata. ESEC / SIGSOFT FSE.2001, 109–120
[125] Benjamin C. Pierce. Types and programming languages. Cambridge, MA, USA:MIT Press, 2002
[126] Luca de Alfaro, Thomas A. Henzinger, Mari¨elle Stoelinga. Timed Interfaces. AlbertoL. Sangiovanni-Vincentelli, Joseph Sifakis, (Editors) EMSOFT. Springer, 2002, vol.2491 of Lecture Notes in Computer Science, 108–122
[127] Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Mari¨elle Stoelinga.Resource Interfaces. Rajeev Alur, Insup Lee, (Editors) EMSOFT. Springer, 2003,vol. 2855 of Lecture Notes in Computer Science, 117–133
[128] Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976
[129] Jos C. M. Baeten. A brief history of process algebra. Theor Comput Sci. 2005,335(2-3):131–146
[130] C. A. R. Hoare. Communicating sequential processes. Upper Saddle River, NJ,USA: Prentice-Hall, Inc., 1985
[131] R. Milner. A Calculus of Communicating Systems. Springer, 1980
[132] Jan A. Bergstra, Jan Willem Klop. Process Algebra for Synchronous Communica-tion. Information and Control. 1984, 60(1-3):109–137
[133] Benjamin C. Pierce. Foundational Calculi for Programming Languages. Allen B.Tucker, (Editor) Handbook of Computer Science and Engineering, CRC Press, 1996
[134] C. A. R. Hoare. Communicating Sequential Processes. Commun ACM. 1978,21(8):666–677
[135] A. W. Roscoe. The Theory and Practice of Concurrency. Upper Saddle River, NJ,USA: Prentice Hall PTR, 1997
[136] Michael J. Butler, C. A. R. Hoare, Carla Ferreira. A Trace Semantics for Long-Running Transactions. Ali E. Abdallah, Cli? B. Jones, Je? W. Sanders, (Editors)25 Years Communicating Sequential Processes. Springer, 2004, vol. 3525 of LectureNotes in Computer Science, 133–150
[137] Hector Garcia-Molina, Kenneth Salem. Sagas. Umeshwar Dayal, Irving L. Traiger,(Editors) SIGMOD Conference. ACM Press, 1987, 249–259
[138] Michael J. Butler, Shamim Ripon. Executable Semantics for Compensating CSP.Bravetti et al. [186], 243–256
[139] S. Ripon, M. Butler. Relating Semantic Models of Compensating CSP. Tech. rep.,University of Southampton, 2006
[140]陈振邦,王戟,齐治昌.补偿通信顺序进程的扩展及失败发散语义.计算机工程与科学
[141] Michael R. A. Huth, Mark D. Ryan. Logic in Computer Science: Modelling andReasoning about Systems. Cambridge, England: Cambridge University Press, 2000
[142] Edmund M. Clarke, Orna Grumberg, Doron Peled. Model Checking. MIT Press,1999. URL http://www.worldcat.org/oclc/40675218
[143] David A. Du?y. Principles of automated theorem proving. New York, NY, USA:John Wiley & Sons, Inc., 1991
[144] Amir Pnueli. The Temporal Logic of Programs. FOCS. IEEE, 1977, 46–57
[145] G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003
[146] Mark C. Little. Transactions and Web services. Commun ACM. 2003, 46(10):49–54
[147] Jim Gray, Andreas Reuter. Transaction Processing: Concepts and Techniques.Morgan Kaufmann, 1993
[148] S. Thatte. XLANG Web Services for Business Process Design, 2001
[149] David Lowe, Xin Chen, Todd Mondor, Tomislav Rus, Ned Rynearson, Steve Wright,Tom Xu. BizTalk Server: The Complete Reference with Cdrom. McGraw-HillProfessional, 2001
[150] Business Process Execution Language for Web Services Java Run Time (BPWS4J).http://www.alphaworks.ibm.com/tech/bpws4j, 2002
[151] Robert Meolic, Tatjana Kapus, Zmago Brezoˇcnik. Verification of concurrent sys-tems using ACTL. M. H. Hamza, (Editor) Applied informatics: proceedings of theIASTED international conference AI’2000, Innsbruck, Austria. Anaheim, Calgary,Zürich: IASTED/ACTA Press, 2000, 663–669
[152] Mark Reynolds. The complexity of the temporal logic with”until”over generallinear time. J Comput Syst Sci. 2003, 66(2):393–426
[153] Homepage of EST, 2006. URL http://lms.unimb.si/EST/
[154] Assaf Arkin, Sid Askary, Scott Fordin, Wolfgang Jekeli, Kohsuke Kawaguchi, Ste-fano Pogliani, Karsten Riemer, Susan Struble, Pal Takacsi-Nagy, Ivana Trickovic,Sinisa Zimek. Web Service Choreography Interface 1.0. Tech. rep., BEA Systems,Intalio, SAP, and Sun Microsystems, 2001. URL http://www.w3.org/TR/wsci/
[155] Mark Burstein, Jerry Hobbs, Ora Lassila, Drew Mcdermott, Sheila Mcilraith, SriniNarayanan, Massimo Paolucci, Bijan Parsia, Terry Payne, Evren Sirin, Naveen Srini-vasan, Katia Sycara. OWL-S: Semantic Markup for Web Services. Website, Novem-ber 2004. URL http://www.w3.org/Submission/2004/SUBM-OWL-S-20041122/
[156] Xin Chen, Jifeng He, Zhiming Liu, Naijun Zhan. A Model of Component-BasedProgramming. Farhad Arbab, Marjan Sirjani, (Editors) International Sympo-sium on Fundamentals of Software Engineering (FSEN 2007). Springer, 2007, vol.4767 of Lecture Notes in Computer Science, 191–206. UNU-IIST TR 350, URLhttp://www.iist.unu.edu/newrh/III/1/docs/techreports/report350.pdf
[157] Anatoliy Gorbenko, Alexander Romanovsky, Vyacheslav Kharchenko, AlexeyMikhaylichenko. Experimenting with exception propagation mechanisms in service-oriented architecture. WEH’08: Proceedings of the 4th international workshop onException handling. New York, NY, USA: ACM, 2008, 1–7
[158] Jifeng He. UTP Semantics for Web Services. Jim Davies, Jeremy Gibbons, (Editors)IFM. Springer, 2007, vol. 4591 of Lecture Notes in Computer Science, 353–372
[159] P. Chalin, J. R. Kiniry, G. T. Leavens, E. Poll. Beyond Assertions: AdvancedSpecification and Verification with JML and ESC/Java2. Formal Methods for Com-ponents and Objects (FMCO) 2005, Revised Lectures. Springer, 2006, vol. 4111 ofLecture Notes in Computer Science, 342–363
[160] SRI. PVS Specification and Verification System. http://pvs.csl.sri.com
[161] G.T. Leavens. JML’s rich, inherited specification for behavioural subtypes. Z. Liu,J. He, (Editors) Proc. 8th Intl. Conf. on Formal Engineering Methods (ICFEM’06).Springer, 2006, vol. 4260 of Lecture Notes in Computer Science
[162] B. Meyer. Applying“Design by Contract”. Computer. 1992, 25(10):40–51
[163] R.-J.J. Back, J. von Wright. Refinement Calculus: A Systematic Introduction.Graduate Texts in Computer Science, Springer, 1998
[164] Andreas Rausch, Ralf Reussner, Ra?aela Mirandola, Frantisek Plasil, (Editors). TheCommon Component Modeling Example: Comparing Software Component Models[result from the Dagstuhl research seminar for CoCoME, August 1-3, 2007], vol.5153 of Lecture Notes in Computer Science. Springer, 2008
[165] Ted Husted, Vincent Massol. JUnit in Action. Manning Publications Co., 2003
[166] M. Fowler, K. Beck, J. Brant, W. Opdyke, D. Roberts. Refactoring: Improving theDesign of Existing Code. Addison-Wesley, 1999
[167] W.W. Eckerson, et al. Three Tier Client/Server Architecture: Achieving Scalabil-ity, Performance and E?ciency in Client Server Applications. Open InformationSystems. 1995, 10(1):3
[168] B. Meyer. Ei?el: The Language. Prentice Hall, 1992
[169] A. Cavalcanti, A. Sampaio, J. Woodcock. A Refinement Strategy for Circus. FormalAspects of Computing. 2003, 15(2-3):146–181
[170] B.P. Mahony, J.S. Dong. Deep Semantic Links of TCSP and Object-Z: TCOZApproach. Formal Aspects of Computing. 2002, 3(2):146–160
[171] M. M¨oller, E-R. Olderog, H. Rasch, H. Wehrheim. Linking CSP-OZ with UML andJava: A Case Study. Proc. Integrated Formal Methods (IFM’04). Lecture Notes inComputer Science 2999. Springer, 2004
[172] Manuel Clavel, Francisco Dur′an, Steven Eker, Patrick Lincoln, Narciso Mart′?-Oliet,Jos′e Meseguer, Carolyn L. Talcott. All About Maude—A High-Performance Log-ical Framework. How to Specify, Program and Verify Systems in Rewriting Logic,vol. 4350 of Lecture Notes in Computer Science. Springer, 2007
[173] The Eclipse Development Platform. http://www.eclipse.org
[174] EMF-based implementation of the Unified Modeling Language.www.eclipse.org/uml2/, 2008
[175] Frank Budinsky, Stephen A. Brodsky, Ed Merks. Eclipse Modeling Framework.Pearson Education, 2003
[176] Topcased—Open Source Engineering Workshop. http://topcased.org
[177] Eclipse BPEL. http://www.eclipse.org/bpel/, 2007
[178] Terence Parr. The Definitive ANTLR Reference: Building Domain-Specific Lan-guages. Raleigh: The Pragmatic Bookshelf, 2007
[179] Sun Microsystems. Java Native Interface Specification.http://javasuncom/j2se/150/docs/guide/jni/spec/jniTOChtml. 2003. URLhttp://java.sun.com/j2se/1.5.0/docs/guide/jni/spec/jniTOC.html
[180] Markus V¨olter et al. Open Architecture Ware, 2008. URLhttp://www.openarchitectureware.org
[181]董威.面向UML的模型检验研究. Ph.D. thesis,国防科学技术大学, 2002
[182] Nad`ege Pontisso, David Chemouil. TOPCASED Combining Formal Methods withModel-Driven Engineering. ASE. IEEE Computer Society, 2006, 359–360
[183] Michael N. Huhns, Munindar P. Singh, Mark H. Burstein, Keith S. Decker, Ed-mund H. Durfee, Timothy W. Finin, Les Gasser, Hrishikesh J. Goradia, Nicholas R.Jennings, Kiran Lakkaraju, Hideyuki Nakashima, H. Van Dyke Parunak, Je?rey S.Rosenschein, Alicia Ruvinsky, Gita Sukthankar, Samarth Swarup, Katia P. Sycara,Milind Tambe, Thomas Wagner, Rosa Laura Zavala Gutierrez. Research Direc-tions for Service-Oriented Multiagent Systems. IEEE Internet Computing. 2005,9(6):65–70
[184] Allan Ellis, Tatsuya Hagino, (Editors). Proceedings of the 14th international con-ference on World Wide Web, WWW 2005, Chiba, Japan, May 10-14, 2005. ACM,2005
[185] Proceedings of the IEEE International Conference on Web Services (ICWS’04), June6-9, 2004, San Diego, California, USA. IEEE Computer Society, 2004
[186] Mario Bravetti, Le¨?la Kloul, Gianluigi Zavattaro, (Editors). Formal Techniquesfor Computer Systems and Business Processes, European Performance EngineeringWorkshop, EPEW 2005 and International Workshop on Web Services and FormalMethods, WS-FM 2005, Versailles, France, September 1-3, 2005, Proceedings, vol.3670 of Lecture Notes in Computer Science. Springer, 2005
[187] 2005 IEEE International Conference on Web Services (ICWS 2005), 11-15 July 2005,Orlando, FL, USA. IEEE Computer Society, 2005
[2]杨芙清.软件工程技术发展思索.软件学报. 2005, 16(1):1–7
[3] Mike P. Papazoglou, Paolo Traverso, Schahram Dustdar, Frank Leymann. Service-Oriented Computing: a Research Roadmap. Int J Cooperative Inf Syst. 2008,17(2):223–255
[4] Thomas Erl. Service-Oriented Architecture: Concepts, Technology, and Design.Upper Saddle River, NJ, USA: Prentice Hall PTR, 2005
[5] Christopher H. Lovelock, Jochen Wirtz. Services Marketing. Prentice Hall Profes-sional Technical Reference, 2007, 6th edn.
[6] Humberto Cervantes, Richard S. Hall. Service-Oriented Software System Engineer-ing: Challenges and Practices, Idea Group Publishing, 2005. 1–47
[7] Mark Turner, David Budgen, Pearl Brereton. Turning Software into a Service. IEEEComputer. 2003, 36(10):38–44
[8] Roy W. Schulte, Yefim V. Natisy.“Service Oriented”Architectures, Part 1 and 2.Garter Research Note SPA-401-068 and SPA-401-069, 1996
[9] Mark Endrei, Jenny Ang, Ali Arsanjani, Sook Chua, Philippe Comte, Pal Krog-dahl, Min Luo, Tony Newling. Patterns: Service-Oriented Architecture and WebServicece. IBM Redbooks, 2004
[10] D. Stratton. The OMG CORBA Trader Service. Tech. rep., School of InformationTechnology and Mathematical Sciences, University of Ballarat, Australia, 1998
[11] Inc. Sun Microsystems. Extensible Runtime Containment and Services Protocol forJavaBeans, 1998
[12] Ken Arnold, Robert Schei?er, Jim Waldo, Bryan O’Sullivan, Ann Wollrath. JiniSpecification. Addison-Wesley Longman Publishing Co., Inc., 1999
[13] The OSGi Alliance. OSGi Service Platform Specification, 2007. Release 4, URLhttp://www.osgi.org/Release4/Download
[14] David Booth, Hugo Haas, Francis Mccabe, Eric Newcomer, Michael Champion,Chris Ferris, David Orchard. Web Services Architecture. Tech. rep., World WideWeb Consortium, February 2004. URL http://www.w3.org/TR/ws-arch/
[15] Alexandre Alves, Assaf Arkin, Sid Askary, Ben Bloch, Francisco Curbera, YaronGoland, Neelakantan Kartha, Sterling, Dieter K¨onig, Vinkesh Mehta, Satish Thatte,Danny van der Rijn, Prasad Yendluri, Alex Yiu. Web Services Business ProcessExecution Language Version 2.0. OASIS Committee Draft, May 2006
[16] Rania Khalaf, Nirmal Mukhi, Sanjiva Weerawarana. Service-Oriented Compositionin BPEL4WS. WWW (Alternate Paper Tracks). 2003
[17] Wil M. P. van der Aalst, Marlon Dumas, Arthur H. M. ter Hofstede. Web Ser-vice Composition Languages: Old Wine in New Bottles? EUROMICRO. IEEEComputer Society, 2003, 298–307
[18] Petia Wohed, Wil M. P. van der Aalst, Marlon Dumas, Arthur H. M. ter Hofstede.Analysis of Web Services Composition Languages: The Case of BPEL4WS. Il-Yeol Song, Stephen W. Liddle, Tok Wang Ling, Peter Scheuermann, (Editors) ER.Springer, 2003, vol. 2813 of Lecture Notes in Computer Science, 200–215
[19] Nickolas Kavantzas, David Burdett, Greg Ritzinger, Tony Fletcher, Yves Lafon,Charlton Barreto. Web Services Choreography Description Language Version 1.0.World Wide Web Consortium, Candidate Recommandation CR-ws-cdl-10-20051109,nov 2005. URL http://www.w3.org/TR/2005/CR-ws-cdl-10-20051109
[20] Luc Clement, Andrew Hately, Claus von Riegen, Tony Rogers. UDDIVersion 3.0.2. Organization for the Advancement of Structured Informa-tion Standards, UDDI Spec Technical Committee Draft, oct 2004. URLhttp://uddi.org/pubs/uddi-v3.0.2-20041019.htm
[21] Asir S. Vedamuthu, David Orchard, Frederick Hirsch, Maryann Hondo,Prasad Yendluri, Toufic Boubez, U¨mit Yalc??nalp. Web Services Pol-icy 1.5—Guidelines for Policy Assertion Authors. World Wide WebConsortium, Note NOTE-ws-policy-guidelines-20071112, nov 2007. URLhttp://www.w3.org/TR/2007/NOTE-ws-policy-guidelines-20071112
[22] OASIS WSS TC. WS-Security Core Specification 1.1, Nov 2006. URLhttp://www.oasis-open.org/committees/tc home.php?wg abbrev=wss
[23] William Cox, Felipe Cabrera, George Copeland, Tom Freund, JohannesKlein, Tony Storey, Satish Thatte. Web Services Transactions specifications.IBM, BEA Systems, Microsoft, Arjuna, Hitachi, IONA, Aug 2005. URLhttp://www.ibm.com/developerworks/library/specification/ws-tx/
[24] DMTF open standards. Web Services for Management (WS-Management), 2008.URL http://www.dmtf.org/standards/wsman/
[25] Ian Sommerville. Software Engineering. Addison Wesley, 2006, 8th edn.
[26] Mike P. Papazoglou, Paolo Traverso, Schahram Dustdar, Frank Leymann. Service-Oriented Computing: State of the Art and Research Challenges. IEEE Computer.2007, 40(11):38–45
[27]岳昆,王晓玲,周傲英. Web服务核心支撑技术:研究综述.软件学报. 2004,15(3):428 442
[28] Richard Hull, Michael Benedikt, Vassilis Christophides, Jianwen Su. E-services: alook behind the curtain. PODS. ACM, 2003, 1–14
[29] Hongbing Wang, Joshua Zhexue Huang, Yuzhong Qu, Junyuan Xie. Web services:problems and future directions. J Web Sem. 2004, 1(3):309–320
[30] Richard Hull, Jianwen Su. Tools for composite web services: a short overview.SIGMOD Record. 2005, 34(2):86–95
[31] Schahram Dustdar, Wolfgang Schreiner. A survey on web services composition.IJWGS. 2005, 1(1):1–30
[32] B. Srivastava, J. Koehler. Web Service Composition, Current Solutions and OpenProblems. Workshop on Planning for Web Services (ICAPS). 2003
[33] Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger. Web service interfaces.Ellis and Hagino [184], 148–159
[34] Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger. An Interface Formalismfor Web Services. Proceedings of the First International Workshop on Foundationsof Interface Technologies (FIT 2005, San Francisco, CA, August 21). 2005. URLhttp://infoscience.epfl.ch/search?recid=114605&ln=en
[35] Jifeng He, Xiaoshan Li, Zhiming Liu. A Theory of Reactive Components. ElectrNotes Theor Comput Sci. 2006, 160:173–195
[36] Jifeng He, Zhiming Liu, Xiaoshan Li. rCOS: A refinement calculus of object sys-tems. Theor Comput Sci. 2006, 365(1-2):109–142. UNU-IIST TR 322, URLhttp://rcos.iist.unu.edu/publications/TCSpreprint.pdf
[37] Jia Zhang, Jen-Yao Chung, Carl K. Chang, Seongwoon Kim. WS-Net: A Petri-netBased Specification Model for Web Services. ICWS [185], 420–427
[38] Jinghai Rao, Peep Ku¨ngas, Mihhail Matskin. Application of Linear Logic to WebService Composition. Liang-Jie Zhang, (Editor) ICWS. CSREA Press, 2003, 3–10
[39] Jinghai Rao, Peep Ku¨ngas, Mihhail Matskin. Logic-based Web Services Composi-tion: From Service Description to Process Model. ICWS [185], 446–453
[40] Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Mas-simo Mecella. Automatic Composition of E-services That Export Their Behavior.Maria E. Orlowska, Sanjiva Weerawarana, Mike P. Papazoglou, Jian Yang, (Editors)ICSOC. Springer, 2003, vol. 2910 of Lecture Notes in Computer Science, 43–58
[41] Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo, Richard Hull, MassimoMecella. Automatic Composition of Web Services in Colombo. Andrea Cal`?, DiegoCalvanese, Enrico Franconi, Maurizio Lenzerini, Letizia Tanca, (Editors) SEBD.2005, 8–15
[42] Xiang Fu, Tevfik Bultan, Jianwen Su. Analysis of interacting BPEL web services.Stuart I. Feldman, Mike Uretsky, Marc Najork, Craig E. Wills, (Editors) WWW.ACM, 2004, 621–630
[43] Raman Kazhamiakin, Marco Pistore. A Parametric Communication Model for theVerification of BPEL4WS Compositions. Bravetti et al. [186], 318–332
[44] Aysu Betin-Can, Tevfik Bultan, Xiang Fu. Design for verification for asynchronouslycommunicating Web services. Ellis and Hagino [184], 750–759
[45] Raman Kazhamiakin, Marco Pistore, Luca Santuari. Analysis of communicationmodels in web service compositions. Les Carr, David De Roure, Arun Iyengar,Carole A. Goble, Michael Dahlin, (Editors) WWW. ACM, 2006, 267–276
[46] Aysu Betin-Can, Tevfik Bultan. Verifiable Web Services with Hierarchical Interfaces.ICWS [187], 85–94
[47] Daniel Brand, Pitro Zafiropulo. On Communicating Finite-State Machines. J ACM.1983, 30(2):323–342
[48] Wenfei Fan, Floris Geerts, Wouter Gelade, Frank Neven, Antonella Poggi. Com-plexity and composition of synthesized web services. Maurizio Lenzerini, DomenicoLembo, (Editors) PODS. ACM, 2008, 231–240
[49] Rachid Hamadi, Boualem Benatallah. A Petri Net-based Model for Web ServiceComposition. Klaus-Dieter Schewe, Xiaofang Zhou, (Editors) ADC. AustralianComputer Society, 2003, vol. 17 of CRPIT, 191–200
[50] Zhihong Ren, Jiannong Cao, Alvin T. S. Chan, Jing Li. Toward a Formal Approachto Composite Web Service Construction and Automation. ICPP. IEEE ComputerSociety, 2003, 436–443
[51] Boualem Benatallah, Fabio Casati, Farouk Toumani, Rachid Hamadi. ConceptualModeling of Web Service Conversations. Johann Eder, Michele Missiko?, (Editors)CAiSE. Springer, 2003, vol. 2681 of Lecture Notes in Computer Science, 449–467
[52] Daniela Berardi, Fabio De Rosa, Luca De Santis, Massimo Mecella. Finite StateAutomata As Conceptual Model For E-Services. J Integr Des Process Sci. 2004,8(2):105–121
[53] Rajeev Alur, David L. Dill. A Theory of Timed Automata. Theor Comput Sci.1994, 126(2):183–235
[54] Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo, Richard Hull, MassimoMecella. Automatic Composition of Transition-based Semantic Web Services withMessaging. Klemens B¨ohm, Christian S. Jensen, Laura M. Haas, Martin L. Kersten,Per-A?ke Larson, Beng Chin Ooi, (Editors) VLDB. ACM, 2005, 613–624
[55] Alin Deutsch, Liying Sui, Victor Vianu. Specification and verification of data-drivenWeb applications. J Comput Syst Sci. 2007, 73(3):442–474
[56] Jing Liu, Jifeng He, Zhiming Liu. A strategy for service realization in service-oriented design. Science in China Series F: Information Sciences. 2006, 49(6):864–884
[57] C.A.R. Hoare, He Jifeng. Unifying Theories of Programming. Prentice Hall, 1998
[58] Chris Peltz. Web Services Orchestration and Choreography. IEEE Computer. 2003,36(10):46–52
[59] Roozbeh Farahbod, Uwe Gl¨asser, Mona Vajihollahi. Specification and Validationof the Business Process Execution Language for Web Services. Wolf Zimmermann,Bernhard Thalheim, (Editors) Abstract State Machines. Springer, 2004, vol. 3052of Lecture Notes in Computer Science, 78–94
[60] Dirk Fahland. Complete Abstract Operational Semantics for the Web Service Busi-ness Process Execution Languages. Informatik-Berichte 190, Humboldt-Universita¨tzu Berlin, 2005
[61] Andreas Wombacher, Peter Fankhauser, Erich J. Neuhold. Transforming BPEL intoAnnotated Deterministic Finite State Automata for Service Discovery. ICWS [185],316–323
[62] M. Koshkina, F. van Breugel. Verification of Business Processes for Web Ser-vices. Technical report CS-2003-11, York University, Oct. 2003. Available from:http://www.cs.yorku.ca/techreports/2003/
[63] Javier C′amara, Carlos Canal, Javier Cubo, Antonio Vallecillo. Formalizing WS-BPEL Business Processes Using Process Algebra. Electr Notes Theor Comput Sci.2006, 154(1):159–173
[64] Howard Foster, Sebasti′an Uchitel, Je? Magee, Je? Kramer. Model-based Verificationof Web Service Compositions. ASE. IEEE Computer Society, 2003, 152–163
[65] Roberto Lucchi, Manuel Mazzara. A pi-calculus based semantics for WS-BPEL. JLog Algebr Program. 2007, 70(1):96–118
[66] Andrea Ferrara. Web Services: A Process Algebra Approach. CoRR. 2004,cs.AI/0406055
[67] R. Milner. A Calculus of Communicating Systems. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1982
[68] Franck van Breugel, Mariya Koshkina. Dead-Path-Elimination in BPEL4WS.ACSD. IEEE Computer Society, 2005, 192–201
[69] Robin Milner. Communicating and mobile systems: theπ-calculus. New York, NY,USA: Cambridge University Press, 1999
[70] T. Bolognesi, E. Brinksma. Introduction to the ISO specification language LOTOS.Comput Netw ISDN Syst. 1987, 14(1):25–59
[71] YanPing Yang, QingPing Tan, JinShan Yu, Feng Liu. Transformation BPEL toCP-Nets for Verifying Web Services Composition. NWESP’05: Proceedings of theInternational Conference on Next Generation Web Services Practices. Washington,DC, USA: IEEE Computer Society, 2005, 137
[72] W.M.P. van der Aalst H.M.W. Verbeek. Analyzing BPEL processes using Petrinets. Proceedings of 2nd International Workshop on Applications of Petri Nets toCoordination, Work?ow and Business Process Management. 2005
[73] Chun Ouyang, Eric Verbeek, Wil M. P. van der Aalst, Stephan Breutel, MarlonDumas, Arthur H. M. ter Hofstede. Formal semantics and analysis of control ?owin WS-BPEL. Sci Comput Program. 2007, 67(2-3):162–198
[74] Hongli Yang, Xiangpeng Zhao, Zongyan Qiu, Geguang Pu, Shuling Wang. A FormalModel forWeb Service Choreography Description Language (WS-CDL). ICWS’06:Proceedings of the IEEE International Conference on Web Services. Washington,DC, USA: IEEE Computer Society, 2006, 893–894
[75] Roberto Gorrieri, Claudio Guidi, Roberto Lucchi. Reasoning About InteractionPatterns in Choreography. Bravetti et al. [186], 333–348
[76] Antonio Brogi, Carlos Canal, Ernesto Pimentel, Antonio Vallecillo. FormalizingWeb Service Choreographies. Electr Notes Theor Comput Sci. 2004, 105:73–94
[77] James E. Johnson, David E. Langworthy, Leslie Lamport, Friedrich H. Vogt. Formalspecification of a Web services protocol. J Log Algebr Program. 2007, 70(1):34–52
[78] Zongyan Qiu, Shuling Wang, Geguang Pu, Xiangpeng Zhao. Semantics ofBPEL4WS-Like Fault and Compensation Handling. John Fitzgerald, Ian J. Hayes,Andrzej Tarlecki, (Editors) FM. Springer, 2005, vol. 3582 of Lecture Notes in Com-puter Science, 350–365
[79] Michael J. Butler, Carla Ferreira, Muan Yong Ng. Precise Modelling of Compensat-ing Business Transactions and its Application to BPEL. J UCS. 2005, 11(5):712–743
[80] Geguang Pu, Huibiao Zhu, Zongyan Qiu, Shuling Wang, Xiangpeng Zhao, JifengHe. Theoretical Foundations of Scope-Based Compensable Flow Language for WebService. FMOODS. 2006, 251–266
[81] Roberto Bruni, Hern′an C. Melgratti, Ugo Montanari. Theoretical foundations forcompensations in ?ow composition languages. Jens Palsberg, Mart′?n Abadi, (Edi-tors) POPL. ACM, 2005, 209–220
[82] Luciano Baresi, Reiko Heckel, Sebastian Th¨one, D′aniel Varr′o. Modeling and val-idation of service-oriented architectures: application vs. style. ESEC / SIGSOFTFSE. 2003, 68–77
[83] Juanjuan Jiang, Tarja Syst¨a. UML-Based Modeling and Validity Checking of WebService Descriptions. ICWS [187], 453–460
[84] Piyush Maheshwari, Sharon Si-Long Tam. Events-Based Exception Handling inSupply Chain Management using Web Services. AICT/ICIW. IEEE Computer So-ciety, 2006, 151
[85] Marco Pistore, Paolo Traverso, Piergiorgio Bertoli, Annapaola Marconi. AutomatedSynthesis of Composite BPEL4WS Web Services. ICWS [187], 293–301
[86] Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri.NUSMV: A New Symbolic Model Checker. STTT. 2000, 2(4):410–425
[87] P. Bertoli, A. Cimatti, M. Pistore, M. Roveri, P. Traverso. MBP: a Model BasedPlanner. Proc of the IJCAI’01 Workshop on Planning under Uncertainty and In-complete Information. 2001
[88] Ziyang Duan, Arthur J. Bernstein, Philip M. Lewis, Shiyong Lu. Semantics BasedVerification and Synthesis of BPEL4WS Abstract Processes. ICWS [185], 734–737
[89] C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Commun ACM.1969, 12(10):576–580
[90] Gerard J. Holzmann. The Model Checker SPIN. IEEE Trans Software Eng. 1997,23(5):279–295
[91] Howard Foster, Sebasti′an Uchitel, Je? Magee, Je? Kramer. Compatibility Verifica-tion for Web Service Choreography. ICWS [185], 738–741
[92] Gwen Salau¨n, Lucas Bordeaux, Marco Schaerf. Describing and Reasoning on WebServices using Process Algebra. ICWS [185], 43–50
[93] Srini Narayanan, Sheila A. McIlraith. Simulation, verification and automated com-position of web services. WWW. 2002, 77–88
[94] Xiaochuan Yi, Krys Kochut. A CP-nets-based Design and Verification Frameworkfor Web Services Composition. ICWS [185], 756–760
[95] Mark H. Burstein, Jerry R. Hobbs, Ora Lassila, David L. Martin, Drew V. Mc-Dermott, Sheila A. McIlraith, Srini Narayanan, Massimo Paolucci, Terry R. Payne,Katia P. Sycara. DAML-S: Web Service Description for the Semantic Web. IanHorrocks, James A. Hendler, (Editors) International Semantic Web Conference.Springer, 2002, vol. 2342 of Lecture Notes in Computer Science, 348–363
[96] Yanping Yang, QingPing Tan, Yong Xiao, Jinshan Yu, Feng Liu. Verifying Web Ser-vices Composition: A Transformation-Based Approach. PDCAT. IEEE ComputerSociety, 2005, 546–548
[97] Yuhong Yan, Marie-Odile Cordier, Yannick Pencol′e, Alban Grastien. MonitoringWeb Service Networks in a Model-based Approach. ECOWS. IEEE Computer So-ciety, 2005, 192–203
[98] Geguang Pu, Xiangpeng Zhao, Shuling Wang, Zongyan Qiu. Towards the Semanticsand Verification of BPEL4WS. Electr Notes Theor Comput Sci. 2006, 151(2):33–52
[99] Gregorio D′?az, Juan Jos′e Pardo, Mar′?a-Emilia Cambronero, Valentin Valero, Fer-nando Cuartero. Verification of Web Services with Timed Automata. Electr NotesTheor Comput Sci. 2006, 157(2):19–34
[100] K.G. Larsen, P. Pettersson, W. Yi. UPPAAL in a Nutshell. STTT. 1997, 1(1-2):134–152
[101] Shin Nakajima. Model-Checking Verification for Reliable Web Service. OOPSLA2002 Workshop on Object-Oriented Web Services. 2002
[102] F. Leymann. Web Services Flow Language (WSFL). IBM Corp. 2001
[103] Wei-Tek Tsai, Yinong Chen, Raymond A. Paul, Ning Liao, Hai Huang. Cooperativeand Group Testing in Verification of Dynamic Composite Web Services. COMPSACWorkshops. IEEE Computer Society, 2004, 170–173
[104] Wei-Tek Tsai, Raymond A. Paul, Zhibin Cao, Lian Yu, Akihiro Saimi, BingnanXiao. Verification of Web Services Using an Enhanced UDDI Server. WORDS.IEEE Computer Society, 2003, 131–138
[105] Hai Huang, Wei-Tek Tsai, Raymond A. Paul, Yinong Chen. Automated ModelChecking and Testing for Composite Web Services. ISORC. IEEE Computer Society,2005, 300–307
[106] Lerina Aversano, Marcello Bruno, Massimiliano Di Penta, Amedeo Falanga, RitaScognamiglio. Visualizing the Evolution of Web Services using Formal ConceptAnalysis. IWPSE. IEEE Computer Society, 2005, 57–60
[107] Olaf Zimmermann, Pal Krogdahl, Clive Gee. Elements ofService-Oriented Analysis and Design, June 2004. URLhttp://www.ibm.com/developerworks/webservices/library/ws-soad1/
[108] Olaf Zimmermann, Niklas Schlimm, Gu¨nter Waller, Marc Pestel. Analysis and De-sign Techniques for Service-Oriented Development and Integration. Armin B. Cre-mers, Rainer Manthey, Peter Martini, Volker Steinhage, (Editors) GI Jahrestagung(2). GI, 2005, vol. 68 of LNI, 606–611
[109] Ali Arsanjani, Shuvanker Ghosh, Abdul Allam, Tina Abdollah, SellaGanapathy, Kerrie Holley. SOMA: A method for developing service-oriented solutions. IBM Systems Journal. 2008, 47(3):377–396. URLhttp://www.research.ibm.com/journal/sj/473/arsanjani.pdf
[110] Liang-Jie Zhang, Nianjun Zhou, Yi-Min Chee, Ahamed Jalaldeen,Karthikeyan Ponnalagu, Renuka R. Sindhgatta, Ali Arsanjani, FaustaBernardini. SOMA-ME: A platform for the model-driven design ofSOA solutions. IBM Systems Journal. 2008, 47(3):397–413. URLhttp://www.research.ibm.com/journal/sj/473/zhang.pdf
[111] Mike P. Papazoglou, Willem-Jan van den Heuvel. Service-oriented design and de-velopment methodology. Int J Web Eng Technol. 2006, 2(4):412–442
[112] Christian Emig, Karsten Krutz, Stefan Link, Christof Momm, Sebas-tian Abeck. Model-Driven Development of SOA Services, 2007. URLhttp://digbib.ubka.uni-karlsruhe.de/volltexte/1000008043
[113] J. K. Strosnider, P. Nandi, S. Kumaran, S. Ghosh, A. Arsanjani. Model-driven synthesis of SOA solutions. IBM Systems Journal. 2008, 47. URLhttp://www.research.ibm.com/journal/sj/473/strosnider.html
[114] Uwe Zdun, Schahram Dustdar. Model-driven and pattern-based integration ofprocess-driven SOA models. International Journal of Business Process Integrationand Management. 2007, 2(2):109–119
[115] Olaf Zimmermann, Uwe Zdun, Thomas Gschwind, Frank Leymann. CombiningPattern Languages and Reusable Architectural Decision Models into a Comprehen-sive and Comprehensible Design Method. WICSA. IEEE Computer Society, 2008,157–166
[116] Ateret Anaby-Tavor, David Amid, Aviad Sela, Amit Fisher, Kuo Zhang, Ou Tie Jun.Towards a Model Driven Service Engineering Process. SERVICES’08: Proceedingsof the 2008 IEEE Congress on Services - Part I. Washington, DC, USA: IEEEComputer Society, 2008, 503–510
[117] Olaf Zimmermann, Jana Koehler, Leymann Frank. Architectural Decision Modelsas Micro-Methodology for Service-Oriented Analysis and Design. Daniel Lu¨bke,(Editor) Proceedings of the Workshop on Software Engineering Methods for Service-oriented Architecture 2007 (SEMSOA 2007), Hannover, Germany. 2007, 46–60
[118] Remco M. Dijkman, Marlon Dumas. Service-Oriented Design: A Multi-ViewpointApproach. Int J Cooperative Inf Syst. 2004, 13(4):337–368
[119] Aliaksei Yanchuk, Alexander Ivanyukovich, Maurizio Marchese. A Lightweight For-mal Framework for Service-Oriented Applications Design. Boualem Benatallah,Fabio Casati, Paolo Traverso, (Editors) ICSOC. Springer, 2005, vol. 3826 of LectureNotes in Computer Science, 545–551
[120] Nikola Milanovic. Service Engineering Design Patterns. Elisabetta Di Nitto, RobertJ. Hall, Jun Han, Yanbo Han, Andrea Polini, Kurt Sandkuhl, Andrea Zisman,(Editors) SOSE. IEEE Computer Society, 2006, 19–26
[121] Ervin Ramollari, Dimitris Dranidis, Anthony J. H. Simons. A Survey of ServiceOriented Development Methodologies. Proceedings of the 2nd European YoungResearchers Workshop on Service Oriented Computing. 2007
[122] Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda, Cristina VideiraLopes, Jean-Marc Loingtier, John Irwin. Aspect-Oriented Programming. ECOOP.1997, 220–242
[123] Nancy A. Lynch, Mark R. Tuttle. An introduction to input/output automata. CWIQuarterly. 1989, 2:219–246
[124] Luca de Alfaro, Thomas A. Henzinger. Interface automata. ESEC / SIGSOFT FSE.2001, 109–120
[125] Benjamin C. Pierce. Types and programming languages. Cambridge, MA, USA:MIT Press, 2002
[126] Luca de Alfaro, Thomas A. Henzinger, Mari¨elle Stoelinga. Timed Interfaces. AlbertoL. Sangiovanni-Vincentelli, Joseph Sifakis, (Editors) EMSOFT. Springer, 2002, vol.2491 of Lecture Notes in Computer Science, 108–122
[127] Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Mari¨elle Stoelinga.Resource Interfaces. Rajeev Alur, Insup Lee, (Editors) EMSOFT. Springer, 2003,vol. 2855 of Lecture Notes in Computer Science, 117–133
[128] Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976
[129] Jos C. M. Baeten. A brief history of process algebra. Theor Comput Sci. 2005,335(2-3):131–146
[130] C. A. R. Hoare. Communicating sequential processes. Upper Saddle River, NJ,USA: Prentice-Hall, Inc., 1985
[131] R. Milner. A Calculus of Communicating Systems. Springer, 1980
[132] Jan A. Bergstra, Jan Willem Klop. Process Algebra for Synchronous Communica-tion. Information and Control. 1984, 60(1-3):109–137
[133] Benjamin C. Pierce. Foundational Calculi for Programming Languages. Allen B.Tucker, (Editor) Handbook of Computer Science and Engineering, CRC Press, 1996
[134] C. A. R. Hoare. Communicating Sequential Processes. Commun ACM. 1978,21(8):666–677
[135] A. W. Roscoe. The Theory and Practice of Concurrency. Upper Saddle River, NJ,USA: Prentice Hall PTR, 1997
[136] Michael J. Butler, C. A. R. Hoare, Carla Ferreira. A Trace Semantics for Long-Running Transactions. Ali E. Abdallah, Cli? B. Jones, Je? W. Sanders, (Editors)25 Years Communicating Sequential Processes. Springer, 2004, vol. 3525 of LectureNotes in Computer Science, 133–150
[137] Hector Garcia-Molina, Kenneth Salem. Sagas. Umeshwar Dayal, Irving L. Traiger,(Editors) SIGMOD Conference. ACM Press, 1987, 249–259
[138] Michael J. Butler, Shamim Ripon. Executable Semantics for Compensating CSP.Bravetti et al. [186], 243–256
[139] S. Ripon, M. Butler. Relating Semantic Models of Compensating CSP. Tech. rep.,University of Southampton, 2006
[140]陈振邦,王戟,齐治昌.补偿通信顺序进程的扩展及失败发散语义.计算机工程与科学
[141] Michael R. A. Huth, Mark D. Ryan. Logic in Computer Science: Modelling andReasoning about Systems. Cambridge, England: Cambridge University Press, 2000
[142] Edmund M. Clarke, Orna Grumberg, Doron Peled. Model Checking. MIT Press,1999. URL http://www.worldcat.org/oclc/40675218
[143] David A. Du?y. Principles of automated theorem proving. New York, NY, USA:John Wiley & Sons, Inc., 1991
[144] Amir Pnueli. The Temporal Logic of Programs. FOCS. IEEE, 1977, 46–57
[145] G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003
[146] Mark C. Little. Transactions and Web services. Commun ACM. 2003, 46(10):49–54
[147] Jim Gray, Andreas Reuter. Transaction Processing: Concepts and Techniques.Morgan Kaufmann, 1993
[148] S. Thatte. XLANG Web Services for Business Process Design, 2001
[149] David Lowe, Xin Chen, Todd Mondor, Tomislav Rus, Ned Rynearson, Steve Wright,Tom Xu. BizTalk Server: The Complete Reference with Cdrom. McGraw-HillProfessional, 2001
[150] Business Process Execution Language for Web Services Java Run Time (BPWS4J).http://www.alphaworks.ibm.com/tech/bpws4j, 2002
[151] Robert Meolic, Tatjana Kapus, Zmago Brezoˇcnik. Verification of concurrent sys-tems using ACTL. M. H. Hamza, (Editor) Applied informatics: proceedings of theIASTED international conference AI’2000, Innsbruck, Austria. Anaheim, Calgary,Zürich: IASTED/ACTA Press, 2000, 663–669
[152] Mark Reynolds. The complexity of the temporal logic with”until”over generallinear time. J Comput Syst Sci. 2003, 66(2):393–426
[153] Homepage of EST, 2006. URL http://lms.unimb.si/EST/
[154] Assaf Arkin, Sid Askary, Scott Fordin, Wolfgang Jekeli, Kohsuke Kawaguchi, Ste-fano Pogliani, Karsten Riemer, Susan Struble, Pal Takacsi-Nagy, Ivana Trickovic,Sinisa Zimek. Web Service Choreography Interface 1.0. Tech. rep., BEA Systems,Intalio, SAP, and Sun Microsystems, 2001. URL http://www.w3.org/TR/wsci/
[155] Mark Burstein, Jerry Hobbs, Ora Lassila, Drew Mcdermott, Sheila Mcilraith, SriniNarayanan, Massimo Paolucci, Bijan Parsia, Terry Payne, Evren Sirin, Naveen Srini-vasan, Katia Sycara. OWL-S: Semantic Markup for Web Services. Website, Novem-ber 2004. URL http://www.w3.org/Submission/2004/SUBM-OWL-S-20041122/
[156] Xin Chen, Jifeng He, Zhiming Liu, Naijun Zhan. A Model of Component-BasedProgramming. Farhad Arbab, Marjan Sirjani, (Editors) International Sympo-sium on Fundamentals of Software Engineering (FSEN 2007). Springer, 2007, vol.4767 of Lecture Notes in Computer Science, 191–206. UNU-IIST TR 350, URLhttp://www.iist.unu.edu/newrh/III/1/docs/techreports/report350.pdf
[157] Anatoliy Gorbenko, Alexander Romanovsky, Vyacheslav Kharchenko, AlexeyMikhaylichenko. Experimenting with exception propagation mechanisms in service-oriented architecture. WEH’08: Proceedings of the 4th international workshop onException handling. New York, NY, USA: ACM, 2008, 1–7
[158] Jifeng He. UTP Semantics for Web Services. Jim Davies, Jeremy Gibbons, (Editors)IFM. Springer, 2007, vol. 4591 of Lecture Notes in Computer Science, 353–372
[159] P. Chalin, J. R. Kiniry, G. T. Leavens, E. Poll. Beyond Assertions: AdvancedSpecification and Verification with JML and ESC/Java2. Formal Methods for Com-ponents and Objects (FMCO) 2005, Revised Lectures. Springer, 2006, vol. 4111 ofLecture Notes in Computer Science, 342–363
[160] SRI. PVS Specification and Verification System. http://pvs.csl.sri.com
[161] G.T. Leavens. JML’s rich, inherited specification for behavioural subtypes. Z. Liu,J. He, (Editors) Proc. 8th Intl. Conf. on Formal Engineering Methods (ICFEM’06).Springer, 2006, vol. 4260 of Lecture Notes in Computer Science
[162] B. Meyer. Applying“Design by Contract”. Computer. 1992, 25(10):40–51
[163] R.-J.J. Back, J. von Wright. Refinement Calculus: A Systematic Introduction.Graduate Texts in Computer Science, Springer, 1998
[164] Andreas Rausch, Ralf Reussner, Ra?aela Mirandola, Frantisek Plasil, (Editors). TheCommon Component Modeling Example: Comparing Software Component Models[result from the Dagstuhl research seminar for CoCoME, August 1-3, 2007], vol.5153 of Lecture Notes in Computer Science. Springer, 2008
[165] Ted Husted, Vincent Massol. JUnit in Action. Manning Publications Co., 2003
[166] M. Fowler, K. Beck, J. Brant, W. Opdyke, D. Roberts. Refactoring: Improving theDesign of Existing Code. Addison-Wesley, 1999
[167] W.W. Eckerson, et al. Three Tier Client/Server Architecture: Achieving Scalabil-ity, Performance and E?ciency in Client Server Applications. Open InformationSystems. 1995, 10(1):3
[168] B. Meyer. Ei?el: The Language. Prentice Hall, 1992
[169] A. Cavalcanti, A. Sampaio, J. Woodcock. A Refinement Strategy for Circus. FormalAspects of Computing. 2003, 15(2-3):146–181
[170] B.P. Mahony, J.S. Dong. Deep Semantic Links of TCSP and Object-Z: TCOZApproach. Formal Aspects of Computing. 2002, 3(2):146–160
[171] M. M¨oller, E-R. Olderog, H. Rasch, H. Wehrheim. Linking CSP-OZ with UML andJava: A Case Study. Proc. Integrated Formal Methods (IFM’04). Lecture Notes inComputer Science 2999. Springer, 2004
[172] Manuel Clavel, Francisco Dur′an, Steven Eker, Patrick Lincoln, Narciso Mart′?-Oliet,Jos′e Meseguer, Carolyn L. Talcott. All About Maude—A High-Performance Log-ical Framework. How to Specify, Program and Verify Systems in Rewriting Logic,vol. 4350 of Lecture Notes in Computer Science. Springer, 2007
[173] The Eclipse Development Platform. http://www.eclipse.org
[174] EMF-based implementation of the Unified Modeling Language.www.eclipse.org/uml2/, 2008
[175] Frank Budinsky, Stephen A. Brodsky, Ed Merks. Eclipse Modeling Framework.Pearson Education, 2003
[176] Topcased—Open Source Engineering Workshop. http://topcased.org
[177] Eclipse BPEL. http://www.eclipse.org/bpel/, 2007
[178] Terence Parr. The Definitive ANTLR Reference: Building Domain-Specific Lan-guages. Raleigh: The Pragmatic Bookshelf, 2007
[179] Sun Microsystems. Java Native Interface Specification.http://javasuncom/j2se/150/docs/guide/jni/spec/jniTOChtml. 2003. URLhttp://java.sun.com/j2se/1.5.0/docs/guide/jni/spec/jniTOC.html
[180] Markus V¨olter et al. Open Architecture Ware, 2008. URLhttp://www.openarchitectureware.org
[181]董威.面向UML的模型检验研究. Ph.D. thesis,国防科学技术大学, 2002
[182] Nad`ege Pontisso, David Chemouil. TOPCASED Combining Formal Methods withModel-Driven Engineering. ASE. IEEE Computer Society, 2006, 359–360
[183] Michael N. Huhns, Munindar P. Singh, Mark H. Burstein, Keith S. Decker, Ed-mund H. Durfee, Timothy W. Finin, Les Gasser, Hrishikesh J. Goradia, Nicholas R.Jennings, Kiran Lakkaraju, Hideyuki Nakashima, H. Van Dyke Parunak, Je?rey S.Rosenschein, Alicia Ruvinsky, Gita Sukthankar, Samarth Swarup, Katia P. Sycara,Milind Tambe, Thomas Wagner, Rosa Laura Zavala Gutierrez. Research Direc-tions for Service-Oriented Multiagent Systems. IEEE Internet Computing. 2005,9(6):65–70
[184] Allan Ellis, Tatsuya Hagino, (Editors). Proceedings of the 14th international con-ference on World Wide Web, WWW 2005, Chiba, Japan, May 10-14, 2005. ACM,2005
[185] Proceedings of the IEEE International Conference on Web Services (ICWS’04), June6-9, 2004, San Diego, California, USA. IEEE Computer Society, 2004
[186] Mario Bravetti, Le¨?la Kloul, Gianluigi Zavattaro, (Editors). Formal Techniquesfor Computer Systems and Business Processes, European Performance EngineeringWorkshop, EPEW 2005 and International Workshop on Web Services and FormalMethods, WS-FM 2005, Versailles, France, September 1-3, 2005, Proceedings, vol.3670 of Lecture Notes in Computer Science. Springer, 2005
[187] 2005 IEEE International Conference on Web Services (ICWS 2005), 11-15 July 2005,Orlando, FL, USA. IEEE Computer Society, 2005