摘要
当前基于网格服务组合的编排方案(choreography proposals)只给出服务描述层面上的定义,没有提供任何推导方法来保证基于此编排方案的服务的一致性。如何验证组合服务行为的正确性和有效性是当前亟需解决的一个研究课题。形式化方法提供了行之有效的建模、推导和验证机制。本文给出网格服务组合基调,基于此基调分析了网格组合服务的动态交互行为特性,提出基于CPi-calculus(Conditional Pi-calculus)的网格组合服务的行为交互模型(IABM),并给出组合服务交互行为的形式化描述,最后进行交互行为的模拟验证。该网格服务行为交互模型为今后网格服务的组合优化工作提供了代数推导依据。
Current grid service choreography proposals remain at the descriptive level, without providing any kind of reasoning mechanism for checking the compatibility of grid services. The research work on how to formalize and verify the behavior of composite grid services is therefore imperative. Formal approaches offer an effective and unambiguous way to model, represent and verify the grid service composition. A novel grid service composition signature is proposed in this paper. By analyzing the interactive behavior of the composite grid service based on the signature, we present interactive behavior model （IABM） for composite grid services, specify the interactive behavior using the CPi-calculus （Conditional Pi-calculus）and formally simulate the interactive behavior finally. The interactive behavior model for composite grid service is algebraic foundation to be used afterwards in automatic and dynamic composition.
出处
《计算机科学》
CSCD
北大核心
2007年第6期13-18,共6页
Computer Science
基金
国家自然科学基金资助项目(60173026)
上海科委重大项目(03DZ15029)
上海高校网格技术E-研究院资助(200301-1)。
