用户名: 密码: 验证码:
服务组合的形式化检验与QoS感知的服务组合方法研究
详细信息    本馆镜像全文|  推荐本文 |  |   获取CNKI官网全文
摘要
基于Web服务组合的软件服务协同技术已成为构造开放网络的动态协作、按需组合的服务交互环境的关键支撑技术。在实际的复杂应用环境中,如何基于语法和语义的正确性检验剔除服务组合的不良程序行为,以及如何确保贯穿服务组合生命周期的QoS质量成为制约服务组合应用的两个具有挑战性的关键问题。
     为实现动态的跨企业业务协作与集成,本文围绕服务组合行为的正确性检验以及服务质量保证这二个正交的性质,深入研究了基于进程代数Pi演算及离散时间Ambient演算的服务组合形式化检验,以及基于QoS数学模型进行精确计算的服务组合优化与划分方法。实现了支撑形式化检验与QoS感知的服务组合架构,并将该架构应用于数字卡通的网上协同制作。本文完成的主要工作如下:
     (1)针对服务组合行为的检验,扩充了Pi演算上的可描述XML数据类型的类型系统,建立了BPEL4WS与Pi演算的双向映射。提出了带有出错程序片段追踪的验证算法,包括基于开互模拟的Pi演算检验、基于模态μ演算的性质检验、基于类型化Pi演算的服务相容性检验,其中独立提出了针对服务组合的相容性定义和检验算法,并且在Web服务组合过程中引入服务相容性检验制导的发现与组合方法。基于以上研究,研制了嵌入了Web组合服务验证工具WebJetChecker,采用组合验证的方法对服务组合程序的性质进行验证,在验证工具中实现了对服务组合程序的出错路径自动标识与出错提示。
     (2)为描述带时间约束的移动行为的分布式动态服务组合,以及复杂Web服务组合结构,独立提出了离散时间Ambient演算(Discrete Timed Mobile Ambient,DTMA)。给出了DTMA的语法和语义、DTMA的性质、DTMA模态逻辑。通过结合时间同步树与Ambient图两种形式化模型,以Ambient时间同步树的方式将实时和移动特征统一在一个形式框架内。对于DTMA与DTMA模态逻辑的子集给出了一个模型验证的算法,证明了验证算法的可判定性。在基于DTMA的BPEL4WS活动的编码基础上,讨论了多层scope的出错与补偿处理Ambient演算形式化模型,并用DTMA描述和分析了带时间约束的移动分布式服务组合实例。
     (3)深入研究了基于QoS的服务组合优化算法,在局部优化算法上实现了针对成分服务选择的基于自动修正区间判断矩阵的层次分析法。在全局优化算法研究上,基于启发式0-1整线性规划算法结合了修正单纯形法和启发式枚举法,仿真实验表明该算法与MATLAB 7的0-1整数规划方法比较,在优化程度及优化效率上得到了显著改进,并且对服务组合和候选服务集合的规模变化没有明显的相关性,因而该算法可用于服务组合规模动态变化的场景,但该算法不能应用于存在服务联盟(服务域)的非线性全局优化模型。因而本文进一步研究了基于QoS的Web服务优化选择的树型编码遗传算法,仿真实验表明在同等优化效果下,树型编码遗传算法比一维编码遗传算法获得了更快的速度,并可有效地支持组合服务运行时重计划。由于树型编码遗传算法可求解非线性全局优化模型,解决了服务联盟的服务组合优化问题。
     (4)针对数据流约束的应用环境,提出了按服务域的基于图聚类的服务组合划分算法。存满足服务域之间数据流量最小化及分布式系统吞吐量最大化的目标约束下,运用图聚类的多级算法划分BPEL服务组合,然后采取分布式方式运行服务组合片段,并对BPEL片段迁移到的分布式节点的负载进行均衡调整。
     (5)基于以上研究,提出了一种支撑QoS感知的服务组合架构。该架构包括服务组合执行引擎的设计,采取了解耦流程执行和成分Web服务调用的方式,实施了带有双控制反馈控制环的流程执行结构。仿真实验表明引入QoS反馈控制结构,使得引擎在组合服务负荷变化时,可为不同的请求服务等级提供服务响应时间保障;解耦流程执行和成分Web服务调用提高了引擎资源的使用效率及引擎的吞吐量。该架构还支持服务组合运行时容错处理的框架,基于此框架研究了用户SLA估计值与实测值偏差检测的在线容错机制,提出了容错选择因子概念及向容错处理方法的映射函数,对运行时故障处理方式提出了“重试调用—替代失效服务—重构局部流程”处理策略,仿真实验表明该在线容错机制有效地支持了服务组合流程的在线自恢复。
     综合应用以上研究成果,设计并实现了一个支撑服务组合的形式化检验与QoS感知的服务组合架构原型系统,并将该架构应用于数字卡通企业协作群的网上协同制作,实现了卡通动画的跨企业协同制作工艺流程。
The software service cooperation technology based on Web Services composition has become the critical technique to construct the circumstance of the dynamic cooperation and on-demand composition service interactions. Under the complicated application circumstance of Web Service composition, there exist two challenging and critical problems: one is how to eliminate the ill behaviors of the orchestration based on verifying the correctness of grammar and semantic, the other is how to guarantee QoS throughout the lifecycle of service composition.
     In order to achieve dynamic business cooperation and integration across different enterprises, this thesis mainly focuses on the two orthometric properties that are correctness verification and Qos guarantees of Web Service composition. Formalization verification of service composition based on Process Algebra and Discrete Time Ambient-Calculus, as well as combinatorial optimization and the partition method based on QoS mathematic model are deeply studied. The service composition architecture supporting formalization verification and QoS-aware composition has been also implemented. Furthermore, the architecture is applied to digital cartoon cooperation manufacturing in the Internet. The main work of this thesis is displayed as follows:
     (1) Aimed at the verification of Web Services composition, Pi-Calculus with type system for describing XML data structure is extended, then the dual mapping between BPEL4WS and Pi-Calculus is constructed. A verification algorithm with the function of tracking the error fractions for Web services composition is proposed, which includes Pi-Calculus verification based on open bisimulation, properties verification based on modalμ-Calculus and service compatibility verification based on Pi-Calculus with type. Moreover, we independently give the definition of compatibility and propose compatibility verification algorithm for Web services composition, and also introduce a novel method for discovering and composing services in the process of Web Services composition under the guidance of verifying compatibility of composite Web Services. Based on the above studies, a framework supporting formal verification of service composition, in which the verification tool called WebJetChecker is embedded, is proposed. WebJetChecker with the combination of three types of the verification techniques for verifying orchestration properties is implemented, by which the error fractions of the orchestration are automatically marked and the hints are given.
     (2) In order to describe distributed dynamic services composition with time-constrained mobile properties and complex structures of services composition, Discrete Timed Mobile Ambient (DTMA) is independently proposed. In the thesis, the semantics and syntax, properties and model logic of DTMA are given. Through combining two formalization models—time synchronous tree and Ambient graph, the time and mobile property are unified into a formal frame by Ambient synchronous tree. A model verification algorithm based on DTMA and the subset of DTMA modal logic is devised, and the decidability of the model verification is proved. According to the encoding of BPEL4WS activities on DTMA, the fault and compensation processing with multi-layer scope are modeled, and an instance of distributed service composition with time constraint and mobility is also described by DTMA and analyzed by the model verification method.
     (3) It is made our every effort to study optimal algorithms of QoS-aware Web service composition. On local optimal algorithms, an AHP approach is realized, which can automatically modify judgment matrix for selection of the component services. On global optimal algorithms, a heuristic 0-1 Integer Liner Programming algorithm is achieved, which combines heuristic enumeration method and revised simplex method. Simulation experiments show that the degree and optimization efficiency in our algorithm is obviously improved compared with the MATLAB 7 bintprog function that is a 0-1 integer programming algorithm. Moreover our algorithm isn't relevant to the scale changes of Web services composition and candidate service sets, thus it is applicable for the scenes that the scales of Web services composition changed dynamically. But for Web services composition with service alliance (service domain), the algorithm is unable because the non-linear global optimal model of the fitness function and QoS constraints can't be expressed in linear mode. Therefore, Tree-Coding Genetic Algorithm (TGA) is used to solve the QoS-aware global optimization with non-linear model. The results of simulation experiments show that TGA is capable of running faster than the one-dimension coding GA under the same conditions, and Tree-Coding has efficient capability for supporting re-planning. In conclusion, TGA has solved non-linear global optimization problems with service alliance.
     (4) Aimed at the application of data stream constraint, a Web services composition partition algorithm based on graphic clustering and service domain is put forward. Under the constraints of satisfying the data stream minimization between the clusters and the throughput maximization of the distributed system, multi-level algorithms based on graph clustering is used to partition BPEL service composition. Afterward, a way of distributed execution is employed to execute service composition. Furthermore the load of the distributed nodes transferring the BPEL fractions is adjusted to a balance.
     (5) According to the above studies, an infrastructure supporting QoS-aware service composition is proposed. The infrastructure includes the design and implement of Web services Composition Execution Engine with double feedback controlling loops, which can decouple flow execution and Web service invocation. From the simulation results, it can be concluded that QoS feedback controlling structure can make the engine supply the guarantee of service response time for different service classes when the workload of Web services composition varies significantly. Additionally, the method of decoupling flow execution and service invocation improves resource utilization and increases concurrence ability of flow execution and throughputs of the engine. This paper also presents run-time fault-tolerance processing framework supported by the infrastructure. Based on the framework, online fault-tolerance mechanism on the deviation detection between QoS measuring values and SLA estimated values is studied. A new concept—"fault-tolerance selection factor" and a mapping function which makes this factor map to the fault-tolerance processing are proposed. The simulation experiments also show that the "retry-substitute-reconfigure" processing strategy adopted at run-time fault processing can effectively support online self-resumption of service composition processes.
     On the basis of all of the above research results, a Web service composition prototype system supporting formal verification and QoS-aware service composition is designed and implemented. This architecture is applied to cooperation manufacturing across different digital cartoon enterprises in the Internet, through which the technologic process of cooperation manufacturing in digital cartoon is realized.
引文
[1] Mike P.Papazoglou. Service-Oriented Computing: Concepts, Characteristics and Directions. In: Massimo M,ed.The 4th International Conference on Web Information Systems Engineering (WISE03),IEEE Computer Society, 2003.3-12
    
    [2] Korhonen J., Pajunen L., Puustjarvi J.. Automatic composition of Web service workflows using a semantic agent. In:Proceedings of the IEEE/WIC International Conference on Web Intelligence (WI 2003),Halifax,Canada,2003,566-569
    [3] IBM Corporation.Web Services Flow Language (WSFL) Version 1.0.2001. http://www-3.ibm.com/software/solutions/webservices/pdf/WSFL.pdf
    [4] T.Andrews,F.Curbera,H.Dholakia,et al.. Business process execution language for web services, version 1.1.http://www-128.ibm.com/developerworks/webservices/library/ws-bpel/index.htm
    [5] Assaf Arkin. et al..Web Service Choreography Interface(WSCI)1.0.-2002.http://www.w3.org/TR/wsci
    [6] Nickolas Kavantzas. et al.. Web Services Choreography Description Language Version 1.0,2004. http://www.w3.org/TR/2004/WD-ws-cdl-10-20041217
    [7] Business Process Management Initiative,Business Process Modeling Language v1.0,2002. http://www.bpmi.org
    [8] R. Hull and J. Su. Tools for Composite Web Services: A Short Overview,SIGMOD Record, 2005, 34(2):86-95
    [9] M. Koshkina, F.van Breugel. Verication of business processes for web services.Department of Computer Science,York University,Technical Report CS-2003-11,2003.
    [10] Gerardo Canfora,Massimiliano Di Penta,Raffaele Esposito,Maria Luisa Villani.QoS-Aware Replanning of Composite Web Services. In:IEEE International Conference on Web Services (ICWS).2005, 311-327
    
    [11] Gao Chun-Ming, Liu Rong-Sheng, Yan Song, Chen Huo-Wang. WebJetChecker:A Formal Verification Tool Embedded into Services Composition Development Environment. In: Proc of the 5th International Conference on Grid and Cooperative Computing, changsha, P.R. China:IEEE Computer Society, 2006,355-362
    
    [12] J.Salas, F.Perez-Sorrosal, M. Patino-Martinez,R.Jimenez-Peris. WS-Replication:A Framework for Highly Available Web Services. In: Proc of the 15th Int'l Conf on World Wide Web. Edinburgh: ACM Press, 2006, 357-366
    
    [13] G.Chafle, S.Chandra, V.Mann, M.Gowri Nanda. Orchestrating Composite Web Services Under Data Flow Constraints. In:Proc of the 3th IEEE Int'l Conf on Web Services.Orlando:IEEE Computer Society,2005,211-218
    [14]B.Kiepuszewski.Expressiveness and Suitability of Languages for Control Flow Modelling in Workflows.PhD thesis,Queensland University of Technology,Brisbane,Australia,2003.http://www.tm.tue.nl/it/research/patterns
    [15]W.M.P.van der Aalst.Verification of workflow nets.In:R Azema and G.Balbo,editors,Proceedings of the 18th International Conference on Applications and Theory in Petri Nets,volume 1248 of Lecture Notes in Computer Science,Springer-Verlag,1997,407-426
    [16]W.M.P.van der Aalst.Challenges in business process management:Verification of business processes using Petrinets.Bulletin of the EATCS,2003(80):174-199
    [17]R.Cleaveland,S.T.Sims.Generic tools for verifying concurrent systems.Science of Computer Programming,2002,42(1):39-47
    [18]W.M.P.van der Aalst.Web Service Composition Languages:Old Wine in New Bottles? In:Proceedings of the 29th EUROMICRO Conference "New Waves in System Architecture"(EUROMICRO'03),2003,298-307
    [19]M.Koshkina.Verification of business processes for web services.Master's thesis,York University,2003.
    [20]Javier Camara,Carlos Canal,Javier Cubo,Antonio Vallecillo.Formalizing WSBPEL Business Processes using Process Algebra.FOCLASA 2005,San Francisco,Californa.USA.2005.
    [21]Gerard J.Holzmann.The Model checker SPIN.IEEE Transactions on Software Engineering,1997,23(5):279-295
    [22]K.L.McMillan.Symbolic Model Checking:An Approach to the State Explosion Problem.Department of Computer Sciences,Carneie-Mellon University,Technical Report CMU-CS-92-131,1992.
    [23]R.Cleaveland,J.Parrow,B.Steffen.The Concurrency Workbench:A semantics-based verification tool for verification of concurrent system.ACM Transactions on Programming languages and Systems,1993,5(1):36-72
    [24]H.M.W.Verbeek,W.M.P.van der Aalst.Analyzing BPEL processes using Petri nets.In D.Marinescu,editor,Proceedings of the Second International Workshop on Applications of Petri Nets to Coordination,Workow and Business Process Management,Miami,FL,USA,October 2005,59-78
    [25]胡建强,邹鹏,王怀民,周斌.Web 服务描述语言QWSDL和服务匹配模型研究,计算机学报,2005,28(4):505-513
    [26]R.Aggarwal,K.Verma,J.Miller,W.Milnor.Constraint Driven Web Service Composition in METEOR-S.In:IEEE International Conference on Services Computing(SCC 2004),Shanghai,China,2004,23-30
    [27]赵俊峰,谢冰,张路,杨芙清.一种支持领域特性的Web服务组装方法,计算机学报,2005,28(4):731-738
    [28]Hai Jin,Hanhua Chen,Zhipeng Lu,Xiaoming Ning.Q-SAC:Toward QoS Optimized Service Automatic Composition.In:5th IEEE/ACM International Symposium on Cluster,computer and the Grid(CCGRID),2005,623-630
    [29]G.Canfora,M.D.Penta,R.Esposito,M.L.Villani.An approach for QoS-aware service composition based on genetic algorithms.In:Proc.of Genetic and Evolutionary Computation Conference(GECCO 2005),Washington,DC,USA,2005.
    [30]T.Yu,K.J.Lin.Service Selection Algorithms for Composing Complex Services with Multiple QoS Constraints.In:3rd International Conference on Service-Oriented Computing(ICSOC 2005),Amsterdam,The Netherlands,2005,410-423
    [31]Bixin Liu,Yuanquan Wu,Yan Jia.QoS Aware Service Composition With Multiple Constrains.In:IFIP Conference of Network and Parallel Computing 2005,Lecture Notes in Computer Science 3779,2005,123-131.
    [32]G.Chafle,S.Chandra,V.Mann.Decentralized Orchestration of Composite Web Services.In:Proc of the 13th Int'l Conf on World Wide Web.New York:ACM Press,2004,134-143
    [33]B.Benatallah,Q.Sheng,A.Ngu,M.Dumas.Declarative Composition and Peer-to-Peer Provisioning of Dynamic Web Services.In:Proc of the 18th Int'l Conf on Data Engineering.San Jose:IEEE Computer Society,2002,297-308
    [34]Boualem Benatallah,Marlon.Dumas,Quan Z.Sheng.Facilitating the Rapid Development and Scalable Orchestration of Composite Web Services,Distributed and Parallel Databases,2005,17:5-37
    [35]Roger Weber,Christoph Schuler,Patrick Neukomm,Heiko Schuldt,Hans-J.Schek.Web Service Composition with O'Grape and Osiris.In:The 29th Very Large DataBase Conference(VLDB 2003),Berlin,Germany,2003,1081-1084
    [36]Mangala Gowri Nanda,Satish Chandra,Vivek Sarkar.Decentralizing Execution of Composite Web Services.In:Proc of the 19th Annual ACM SIGPLAN Conf on Object-Oriented Programming,Systems,Languages,and Applications(OOPSLA 2004).Canada:ACM Press,2004,170-187
    [37]Nanda MG,Karnik N.Synchronization analysis for decentralizing composite Web services.In:Proc.of the ACM Symp.on Applied Computing(SAC2003),2003,407-414
    [38]G.Chafle,S.Chandra,P.Kankar,V.Mann.Handling Faults in Decentralized Orchestration of Composite Web Services. In: Proceedings of the 3rd International Conference on Service Oriented Computing (ICSOC 2005),Amsterdam, Netherlands, 2005,410-423
    [39] M.Adel Serhani, Rachida Dssouli, Abdelhakim Hafid, Houari Sahraoui. A QoS broker based architecture for efficient web services selection, In:IEEE International Conference on Web Services (ICWS'05),2005, 113-120
    [40] Liang-Jie Zhang and Bing Li. Requirements Driven Dynamic Services Composition for Web Services and Grid Solutions, Journal of Grid Computing,2004,2: 121-140
    [41] Liangzhao Zeng, Boualem Benatallah, Marlon Dumas, Jayant Kalagnanam,Henry Chang. QoS-Aware Middleware for Web Services Composition. IEEE transactions on software engineering, 2004, 30(5):311-327.
    [42] T. Yu, K.J.Lin. Service Selection Algorithms for Composing Complex Services with Multiple QoS Constraints. In:3rd International Conference on Service-Oriented Computing (ICSOC 2005), Amsterdam, The Netherlands, 2005,12-15
    [43] Gwyduk Yeom, Dugki Min. Design and Implementation of Web Services QoS Broker. In: Proceedings of the International Conference on Next Generation Web Services Practices, 2005, 143-710
    [44] Eunjoo Lee, Woosung Jung. A Framework to Support QoS-Aware Usage of Web Services. In:The 6th International Conference on Web Engineering (ICWE). 2005 3579:318-327
    [45] Roberto Bruni, Hernan C. Melgratti. Ugo Montanari: Theoretical foundations for compensations in flow composition languages. In:Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Long Beach. California, USA. 2005,209-220
    [46] R.Milner. Communicating and Mobile Systems: ThePi-Calculus. Cambridge:Cambridge University Press, 1999.
    
    [47] Benjamin C.Pierce. Types and Programming Languages, The MIT Press, 2002.
    [48] David N.Turner. The Polymorphic Pi-calculus:Theory and Implementation. PhD thesis University of Edinburgh, 1995.
    [49] Allen L. Brown, Jr.,Cosimo Laneve, L. Gregory Meredith. PiDuce: a process calculus with native XML datatypes. In: Proc. of Workshop on Web Services and Formal Methods, 2005, 18-34
    [50] S. Carpineti, C. Laneve, L. Padovani. PiDuce - a project for experimenting Web services technologies January 2006 http://www.cs.unibo.it/PiDuce/#imp
    [51] J.C.Fernandez and L.Mounier. "On-the-fly" verification of behavioural quivalences and preorders. In K.G. Larsen and A. Skou, editors, Proceedings of CAV'91, volume575 of Lecture Notes in Computer Science, Springer-Verlag,1991,181-191.
    [52] D.Sangiorgi. A theory of bisimulation for the π -calculus. Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK, Technical Report, ECS-LFCS-93-270, 1993.
    [53] Bjorn Victor. A Verification Tool for the Polyadic π-calculus[Licentiate Thesis].Sweden: Department of Computer Systems,Uppsala University, 1994.
    [54] Stirling C. Modal and temporal logics for processes. LNCS, .Springer-Verlag,1996,1043:149-237
    [55] Fredrick B. Beste.The Model Prover-a sequent-calculus based modal μ-calculus model checker tool for finite control π-calculus agents. 1998,http://www.it.uu.se/profundis/mwb-dist/x4.ps.gz.
    [56] Massimo Paolucci,Takahiro Kawamura,Terry R. Payne,Katia Sycara. Semantic Matching of Web Services Capabilities. International Semantic Web Conference,Sardinia,Italy,2002
    [57] Franck van Breugel and Maria Koshkina. Models and Verification of BPEL.Draft paper,September 2006.http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf
    [58] S.Hinz,K. Schmidt,C. Stahl. Transforming BPEL to Petri nets. In W.M.P. van der Aalst, B. Benatallah, F. Casati,F. Curbera,editors,In: Proceedings of the 3rd International Conference on Business Process Management,Nancy,France,Springer-Verlag : volume 2649 of Lecture Notes in Computer Science,2005,220-235
    [59] Y.Yang,Q. Tan,Y. Xiao. Verifying web services composition based on hierarchical colored Petri nets. In: Proceedings of the 1st International Workshop on Interoperability of Heterogeneous Information Systems, Bremen, Germany:ACM, 2005, 47-54
    [60] Axel Martens. On compatibility of web services. http://www2.Informatik.hu-berlin.de/top/download/publications/WSCompatibility.pdf
    [61] S.Nakajima. Verification of Web Service Flows with Model-Checking Techniques. In Proceedings of the First International Symposium on Cyber Worlds, Tokyo: IEEE Computer Society Press,2002, 378-386
    [62] X. Fu,T. Bultan,J. Su. Analysis of Interacting BPEL Web Services. In S.I.Feldman,M. Uretsky,M. Najork,C.E. Wills,editors, Proceedings of the 13th International World Wide Web Conference, New York, NY,USA:ACM,2004,621-630
    [63] X. Fu,T. Bultan,J. Su. Synchronizability of conversations among web services. IEEE Transactions on Software Engineering,2005, 31(12):1042-1055
    [64] Yuliang Shi,Liang Zhang,Fangfang Liu,Lili Lin,Baile Shi. Compatibility Analysis of Web Services. In: The 2005 IEEE/WIC/ACM International Conference on Web Intelligence (WI'05), 483-486
    [65] Howard Foster, Sebastian Uchitel Jeff Magee, Jeff Kramer. Compatibility verification for web service Choreography. http://www.doc.ic.ac.uk/~hfl/phd/papers/compatibilityforchoreography-icws2004.pdf
    [66] C.Karamanolis,D.Giannakopoulou,J.Magee,S.M.Wheater. Model checking of workflow schemas. In: Proceedings of the 4~(th) Int ernational Enterprise Distributed Object Computing Conference, Makuhari, Japan: IEEE Computer Society Press, 2000,170-179
    [67] G. Pu, X. Zhao,S. Wang,Z. Qiu. Towards the semantics and verification of BPEL4WS. In: Proceedings of the International Workshop on Web Languages and Formal Methods(WLFM 2005),New Castle,UK: ENTCS , 2005,151(2):33-52, Elsevier, 2006.
    [68] Ferrara A. Web Services: A Process Algebra Approach. In:International Conference on Service Oriented Computing. New York City,USA. 2004.242-251.
    [69] 廖军,谭浩,刘锦德.基于Pi演算的 web 服务组合的描述和验证计算机学报2005,28(4): 635-643
    [70] M. Koshkina , F.van Breugel. Modelling and verifying web service orchestration by means of the concurrency workbench. ACM SIGSOFT Software Engineering Notes,2004,29(5): 1-10
    [71] G. Sala un, L. Bordeaux, M. Schaerf. Describing and reasoning on web services using process algebra. In: Proceedings of the IEEE International Conference on Web Services, San Diego, CA, USA: IEEE, 2004 ,43-51
    [72] Bjorn Victor. The Mobility Workbench User's Guide Polyadic version 3.122.1995. http://www.it.uu.se/profundis/mwb-dist/guide-3.122.ps.gz
    [73] Javier C amara,Carlos Canal,Javier Cubo,Antonio Vallecillo. Formalizing WSBPEL Business Processes Using Process Algebra, Electronic Notes in Theoretical Computer Science,2005
    [74] G. Sala un, A. Ferrara, A. Chirichiello. Negotiation among web services using LOTOS/CADP. In L. Zhang, editor, Proceedings of the European Conference on Web Services, volume 3250 of Lecture Notes in Computer Science,Erfurt,Germany: Springer-Verlag, 2004, 198-212
    [75] H. Foster,S. Uchitel,J. Magee,J. Kramer. LTSA-WS: A tool for model-based verification of web service compositions and choreography. In: Proceeding of the 28th International Conference on Software Engineering, Shanghai, China: ACM,May 2006, 771-774
    [76] Cardelli L,Gordon AD. Mobile ambients. In :Nivat M,ed. Foundations of Software Science and Computation Structure, Heidelberg: Springer Verlag,LNCS 1378, 1998,140-155
    [77] M. Mazarra, R. Lucchi. A framework for generic error handling in business processes. In: Proceedings of the 1st International Workshop on Web Services and Formal Method, volume 105 of Electronic Notes in Theoretical Computer Science,Pisa,Italy: Elsevier, 2004 , 133-145
    [78] Robin Milner. The Polyadic Pi-Calculus: A Tutorial.Department of Computer Science, University of Edinburgh, Technical report :1991.
    [79] Benjamin Pierce,Davide Sangiorgi. Typing and Subtyping for Mobile Processes.In: Proceedings 8th IEEE Logics in Computer Science, 1996,6(5) :409-453
    [80] Antonio Brogi,Carlos Canal,Ernesto Pimentel,Antonio Vallecillo. Formalizing Web Service Choreographies,www.lcc.uma.es/~av/Publicaciones/04/ws-fm04.pdf,WS-FM 2004.
    [81] Claus Pahl. A Pi-Calculus based Framework for the Composition and Replacement of Components. Conference on Object-Oriented Programming,Systems, Languages,and Applications (OOPSLA'2001)-Workshop on Specification and Verification of Component-Based Systems, ACM Press, 2001
    [82] Boualem Benatallah, Fabio Casati. Compatibility and replaceability analysis for timed web services protocols. "BDA", Saint Malo, France, 2005, 17-20
    [83] Pietro Cenciarelli,Ivano Talamo, Alessandro Tiberi. Ambient Graph Rewriting,Electronic Notes in Theoretical Computer Science, 2005, 117:335-351
    [84] Cardelli L.,Ghelli G.,Gordon A.D. Mobility types for mobile ambients. Lecture Notes in Computer Science,1999,1644:230-239
    [85] Cardelli, L., Gordon, A.D. Anytime,anywhere: Modal logics for mobile ambients.In Proceedings POPL'00, ACM, 2000, 365-377
    [86] Liang Chen. Timed Processes: Models,Axioms and Decidability. PhD thesis,Laboratory for Foundations of Computer Science, University of Edinburgh,1992
    [87] Charatonik,W.Talbot,J.M. The Decidability of Model Checking Mobile Ambients. In: Proc of FoSSaCS'04,LNCS, Springer-Verlag,2004
    [88] Raman Kazhamiakin,Paritosh K,Pandya,et al. Timed Modelling and Analysis in Web Service Compositions. In: Proceedings of the First International Conference on Availability,Reliability and Security(ARES2006),2006, 840-846
    [89] Leslie Lamport. Time,clocks,and the ordering of events in a distributed system. Communications of the ACM,1978,21(7):558-564
    [90]Martin Berger.The Two-Phase Commitment Protocol in an Extended π-Calculus,In:Proc of EXPRESS '00:Expressiveness in Concurrency,Electronic Notes in Theoretical Computer Science,Elsevier,Amsterdam,2000,105-130
    [91]Manuel MAZZARA.Timing issues in Web services composition.European Performance Engineering Workshop and International Workshop on Web Services and Formal Methods(EPEW/WS-FM 2005),In Proceedings.Lecture Notes in Computer Science 3670,2005,287-302
    [92]Fournet C,Gonthier G.The reflexive CHAM and the join-calculus.In:Proc of 23th Annual ACM Symposium on Principle of Programming Languages,New York:ACM Press,1996,372-385
    [93]陈靖.带实时的传值与移动系统研究.博士论文,中国科学院软件研究所.2003
    [94]Agositno Cortesi,Riccardo Focardi.Information Flow Security in Mobile Ambients.Electronic Notes in Theoretical Computer Science,2001
    [95]Chiara Braghin,Agostino Cortesi,Riccardo Focardi.Security boundaries in mobile Ambients.Computer Languages,Systems & Structures,2002,28(2002)101-127
    [96]Pascal Zimmer.On the Expressiveness of Pure Mobile Ambients.In:Proc.EXPRESS'00,volume 39 of Electronic Notes in Theoretical Computer Science,,Elsevier,2000,81-104
    [97]Pascal Zimmer.On the Expressiveness of Pure Safe Mobile Ambients,France,INRIA Research Report RR-4350,2002
    [98]Massimo Merro,Francesco Zappa Nardelli.Behavioural Theory for Mobile Ambients,INRIA Technical Report RR-5375.Available from:http://ww w.inria.fr/rrrt/rr-5375.html 2004,2004
    [99]Massimo Merro,Francesco Zappa Nardelli.Bisimulation Proof Methods for Mobile Ambients,Computer Science Report 2003:01,http://cogslib.cogs.sus x.ac.uk/csr abs.php?cs,University of Sussex,2003
    [100]Massimo Merro,Francesco Zappa Nardelli.Bisimulation Proof Methods for Mobile Ambients.In:Proceedings of ICALP'03,Springer,2003,volume 2719 of LNCS,584-598
    [101]Maria Grazia Vigliotti.Transitions systems for the Ambient calculus.Master thesis,Imperial College of Science,Technology and Medicine(University of London),September 1999
    [102]D.Sangiorgi.Bisimulation for Higher-Order Process Calculi.Information and Computation,1996,131(2):141-178
    [103]D.Sangiorgi.On the bisimulation proof method.Journal of Mathematical Structures in Computer Science,1998,8:447-479
    [104]WitoldCharatonik,Silvano Dal Zilio,Andrew D.Gordonet al..Model checking mobile Ambients.Theoretical Computer Science,2003 308(2003):277-331
    [105]Joost-Pieter,Katoen Concepts.Algorithms,and Tools for Model Checking.http://www.ift.ulaval.ca/~jodesharnais/Verification/avvs.ps.gz,1999
    [106]Glenn Bruns.Distributed Systems Analysis with CCS,London:Prentice-Hall,Inc.,1997
    [107]L.Cardelli,A.Gordon.Logical properties of name restriction.Spring,Lecture notes in Computer Science,Vol.2044,2001
    [108]Luca C ardelli,Andrew D.Gordon.Ambient Logic.Mathematical Structures in Computer Science,2006
    [109]H.Lin.A Predicate mu-Calculus for Mobile Ambients.Journal of Computer Science and Technology,2005,20(1):95-104
    [110]刘剑.传值进程与移动进程的模型检测方法.博士论文,中国科学院软件研究所,2005
    [111]P.Degano,U.Montanari.A model of distributrd systems based on graph rewriting.Journal of the ACM,1987,34:411-449
    [112]A.Tiberi.Distributed computation as hypergraph rewriting.Masters thesis,2004
    [113]程理民,吴江,张玉林.运筹学模型与方法教程.北京:清华大学出版社,2002
    [114]D.Bertsimas,J.N.Tsitsiklis.Introduction to Linear Optimization.Athena Scientific,Cambridge,Massachusetts,1997
    [115]Spielman DA,Teng SH.Smoothed analysis of algorithms:Why the simplex algorithm usually takes polynomial time.In:SIGACT,ed.Proc.of the 33rd Annual ACM Symp,on Theory of Computing,ACM Press,2001.296-305
    [116]Srinivas M.,Patnaik L.M..Genetic algorithm:A survey.IEEE Computer,1994,27(6);17-26
    [117]Rainer Berbner,Michael Spahn,Nicolas Repp,et al..Heuristics for QoS-aware Web Service Composition.4th IEEE International Conference on Web Services (ICWS'06),2006,72-82
    [118]Radicchi F,Castellano C,Cecconi F,et al..Defining and identifying communities in networks.In:Proc Natl Acad Sci,2004,101(9):2658-2663
    [119]M.Garey D.Johnson.Computers and Intractability:A Guide to the Theory of NP-Completeness,W.H.Freeman & Co Ltd,1979
    [120]Hendrickson B,Leland R.A Multi-Level Algorithm for Partitioning Graphs.In:Proc of the ACM/IEEE Supercomputing Conference,San Diego:ACM Press,1995,626-657
    [121]Chunming Gao,Xiaojuan Yuan,Huowang Chen.The Execution Mechanism of Service Proxy in the Web Services Composition Execution Engine.In:Proc.of The 31st Annual International Computer Software and Applications Conference (COMPSAC 2007),July 24-27,2007.Beijing,China.
    [122]L.Lovasz and M.Plummet.Matching Theory.Akademiai Kiado,North Holland,Budapest,1986
    [123]Tao Yu,Kwei-Jay Lin.Service Selection Algorithms for Web Services with End-to-end QoS Constraints.In:Proceedings of the IEEE International Conference on e-Commerce Technology,2004.USA:IEEE Computer Society Press,2004:129-136
    [124]D.Pisinger.A minimal algorithm for the Multiple-choice Knapsack Problem.European Journal of Operational Research,1995,83,b394-410
    [125]Ron Widyono.The design and evaluation of routing algorithms for real-time channels.University of California at Berkeley,International Computer Science Institute,Technical Report,TR-94-024,1994
    [126]廖渊,唐磊,李明树.一种基于QoS的服务构件组合方法.计算机学报,2005,28(4):627-634
    [127]陈彦萍,李增智,唐亚哲等.一种满足马尔可夫性质的不完全信息下的web 服务组合方法.计算机学报,2006,29(7):1076-1083
    [128]Canfora G.,Penta M.Di,Esposito R.,et al..A lightweight approach for QoS-aware service composition.In:Proceedings of the 2nd International Conference on Service Oriented Computing,New York,USA,2004,36-47
    [129]张成文,苏森,陈俊亮.基于遗传算法的QoS感知的Web服务选择.计算机学报,2006,29(7):1029-1037
    [130]Martello S and Toth P.Algorithms for knapsack problems.Annals of Discrete Mathematics,1987,31:70-79
    [131]Khan,S.,Li,K.F.,Manning,et al..M.Solving the knapsack problem for adaptive multimedia systems.Studia Informatica Universalis,2002,2(1):157-178
    [132]Xuan Thang Nguyen,Ryszard Kowalczyk,Manh Tan Phan.Modelling and Solving QoS Composition Problem Using Fuzzy DisCSP.ICWS 2006Washington,DC,USA,2006,55-62
    [133]J.Cardoso,A.Sheth,J.Miller,et al..Quality of service for workflows and web service processes,Journal of Web Semantics,2004,1(3):281-308
    [134]代钰,杨雷,张斌等.支持组合服务选取的QoS模型及优化求解.计算机学报,2006,29(7):1167-1178
    [135]Shoujian Yu,Qin Zhu,Xiaoling Xia,et al..A Novel Web Service Catalog System Supporting Distributed Service Publication and Discovery.IMSCCS 2006
    [136]U.Thaden,W.Siberski,W.Nejdl.A semantic Web based peer-to-peer service registry network,University of Hanover,Germany,Technical Report,2003
    [137]Farnoush Banaei-Kashani,Ching-Chien Chen,Cyrus Shahabi.WSPDS:Web Services Peer-to-peer Discovery Service.In:International Conference on Internet Computing,2004,733-743
    [138]Brahmananda Sapkota,Dumitru Roman,Dieter Fensel.Distributed Web Service Discovery Architecture.AICT/ICIW 2006
    [139]刘必欣,王玉峰,贾焰等.一种基于角色的分布式动态服务组合方法.软件学报,2005,16(11):1859-1867
    [140]Qiao Xiaoqiang,Wei Jun.A Decentralized Services Choreography Approach for Business Collaboration.IEEE SCC 2006:190-197
    [141]Wasim Sadiq,Shazia W.Sadiq,Karsten Schulz.Model Driven Distribution of Collaborative Business Processes.IEEE SCC 2006,281-284
    [142]B.Benatallah,Q.Z.Sheng,M.Dumas.The self-serv environment for web services composition.IEEE Internet Computing,2003,7(1):40-48
    [143]V.Atluri,S.A.Chun,P.Mazzoleni.A Chinese Wall Security Model for Decentralized Workflow Systems.In:Proceedings of the Conference on Computer and Communications Security,Philadelphia,2001,48-57
    [144]Shuping Lan.A Model for Web Services Discovery with QoS.ACM SIGecom Exchanges,2003,4(1):1-10
    [145]Ivona Brandic,Siegfried Benkner,Gerhard Engelbrecht,et al..QoS Support for Time-Critical Grid Workflow Applications.In:First International Conference on e-Science and Grid Computing(e-Science'05),e-science,2005,108-115
    [146]J.Almedia,M.Dabu,A.Manikutty,et al..Providing Differentiated Levels of Service in Web Content Hosting.In:Proceedings of the 1998 SIGMETRICS Workshop on Internet Server Performance,Piscataway,New Jersey,1998,91-102
    [147]Business Process Execution Language for Web Services Java Run Time (BPWS4J).http://www.alphaworks.ibm.com/tech/bpws4j.
    [148]ActiveBPEL.http://www.activebpel.org/
    [149]Network Simulator.http://www.isi.edu/nsnam/ns
    [150]K.Jeffay,F.D.Smith,A.Moorthy,et al..Proportional Share Scheduling of Operating System Services for Real-Time Applications.IEEE Real-Time Systems Symposium,1998.
    [151]G.F.Franklin,J.D.Powell,A.Emami-Naeini.Feedback Control of Dynamic Systems,1994.
    [152] K. J. Astrom, B. Wittenmark. Adaptive Control (2nd Ed.), Addison-Wesley, 1995.
    [153] WS-Policy,http://www.w3.org/Submission/WS-Policy/.
    [154] WS-PolicyAttachment, http://www.w3.org/Submission/WS-PolicyAttachment/.
    [155] Eder J., Panagos E., Rabinovich M.. Time constraints in workflow systems. In:Proceedings of the 11th International Conference(CAiSE'99), 1999,286-239
    [156] Gillmann M., Weikum G., Wonner W.. Workflow management with service quality guarantees. In: Proceedings of ACM SIGMOD International Conference,Management of Data, Madison, USA, 2002,228-239
    [157] Baccelli F ,Cohen G, Olsder GJ , et al. Synchronization and Linearity: An Algebra for Discrete Event Systems. New York :Wiley , 1992.
    [158] Kennedy J, Eberhart R C, Shi Y. Swarm Intelligence. San Francisco: Morgan Kaufman Publisher, 2001.
    [159] C. Ouyang, W.M.P. van der Aalst, S. Breutel, et al.. WofBPEL: A tool for automated analysis of BPEL processes. In: Proceedings of the 3rd International Conference on Service-Oriented Computing, Amsterdam, 2005, 484-489
    [160] C. Ouyang, W.M.P. van der Aalst, S. Breutel, et al.. Formal semantics and analysis of control flow in WS-BPEL. BPM Center, Technical Report BPM-05-15,2005.
    [161] H. Foster. A Rigorous Approach To Engineering Web Service Compositions. PhD thesis, Imperial College, London, UK, 2006.
    [162] H. Foster, S. Uchitel, J. Magee, et al.. Tool support for model-based engineering of web service compositions. In: Proceedings of the 2005 IEEE International Conference on Web Services, Orlando, FL, USA, IEEE, 2005, 95-102
    [163] K. Huynh. Analysis through reaction: walking the EMF model of BPEL4WS.Master's thesis, York University, Toronto, Canada, 2005.
    [164] E. M. Maximilien , M. P. Singh. Toward autonomic web services trust and selection. In:2nd international conference on Service oriented computing, New York, 2004,212-221
    [165] Tao Yu, Kwei-Jay Lin. The Design of QoS Broker Algorithms for QoS-Capable Web Services. In:Proc.of IEEE International Conference on e-Technology,e-Commerce and e-Service. 2004,17-24
    [166] M. Comuzzi,B. Pernici. An Architecture for Flexible Web Service QoS Negotiation. In:Proceedings of 9th IEEE EDOC Conference, Enschede, The Netherlands, 2005,19-22
    [167] LiangD,FangC.L,ChenC, et al.. Fault-tolerant Web service. In: Proceedings of the 10th Asia2 Pacific Software Engineering Conference(APSEC.03), ChiangMai,Thailand, 2003, 310-319
    [168] Bilorusets R.et al.Web service reliable messaging protocol. IBM/BEA/Microsoft/TIBCO Specification, 2004
    [169] IwasaK., DurandJ., RuttT., et al. Web service reliable messaging (WS-Reliability 1.1).OASIS Specification, 2004
    [170] TartanogluF., IssarnyV., RomanovskyA., et al.. Coodinated forward error recovery for composite Web services. In: Proceedings of the 22nd Symposium on Reliable Distribute Systems(SRDS.03), Florence, Italy, 2003, 167-176
    [171] J.Salas, F Perez-Sorrosal, M. Patino-Martinez, et al.. WS-replication:a framework for highly available web services. In: Proceedings of the 15th International Conference on World Wide Web,Edinburgh, Scotland, 2006, 23-26
    [172] F. Casati, M.-C. Shan. Dynamic and Adaptive Composition of E-Services.Information Systems, 2001, 26(3):43-162
    [173] D. Georgakopoulos, H. Schuster, A. Cichocki, et al.. Managing Process and Service Fusion in Virtual Enterprises,Information System. Special Issue on Information System Support for Electronic Commerce, 1999,24(6):429-456
    [174] L. Eggert, J. Heidemann. Application-Level Differentiated Services for Web Servers. World Wide Web Journal, 1999, 2(3): 133-142
    [175] C. Lu, Y. Lu, T.F. Abdelzaher, et al.. Feedback Control Architecture and Design Methodology for Service Delay Guarantees in Web Servers. IEEE Transactions on Parallel and Distributed Systems, 2006,17(9): 1014-1027
    [176] N. Bhatti, R. Friedrich. Web Server Support for Tiered Services. IEEE Network,1999,13(5):64-71
    [177] N. Vasiliou, H. Lutfiyya. Providing a Differentiated Quality of Service in a World Wide Web Server. Performance Evaluation Review, 28(2): 22-27
    [178] T. Newhouse, J. Pasquale. ALPS: An Application-Level Proportional-Share Scheduler. In:Proc.15th IEEE International Symposium on High Performance Distributed Computing, Paris, France, 2006 ,279-290
    [179] N. Vasiliou and H. Lutfiyya, Providing a Differentiated Quality of Service in a World Wide Web Server, Performance Evaluation Review, 28(2): 22-27

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700