论文部分内容阅读
随着面向服务计算技术的快速发展,越来越多的软件系统通过复用已有的服务来构建,这样的服务被称为参与者(Peer),为使来自不同组织各自独立的参与者能够有效地集成,构建出预期的分布式系统(Distribution System),有必要提供参与者在交互时应遵守的全局契约,这个从全局的角度来描述一组参与者之间的交互的契约称为编排(Choreography)。编排的可实现性分析(Analysis of the Realizability of Choreographies)的意义在于:对给定编排的情况下,将编排映射为一组参与者,再将一组参与者在不同的通信条件下进行组合,组合后所得的编排实现描述的各参与者之间的交互是否与原编排一致。本文关注编排分析中的可实现性分析问题。并首次提出一种以交互式接口Petri网作为形式化基础对编排进行可实现性分析的新方法,具体而言:(1)将原型Petri网扩展为交互式接口 Petri网,用于描述编排和参与者,并提出了将编排映射为参与者的方法。该方法首先基于交互式接口 Petri网定义编排,而后用动作映射将编排中的所有动作映射为有关动作和无关动作(注:用tau表示),最后保留有关动作,删除tau变迁得到参与者。(2)提出一种使用交互式接口Petri网对同步通信下编排的可实现性进行分析的方法。该方法将参与者在同步通信模型下进行并发组合,得到编排同步实现;而后将编排同步实现和编排之间的等价检验规约为编排实现可达图和原编排可达图之间是否满足强互模拟关系的检验,从而得出编排的同步可实现性分析结果。(3)提出一种使用交互式接口Petri网对有界异步通信下编排的可实现性进行分析的方法。该方法将参与者在异步通信模型下进行并发组合,得到编排的异步实现;而后将编排异步实现和编排之间的等价检验规约为编排实现可达图和原编排可达图之间是否满足弱互模拟关系的检验,从而得出编排的异步可实现性分析结果。