全球服务协调政策：面向服务的体系结构、协调与一致性的形式化方法

理论计算机科学电子笔记260（2010）73-89www.elsevier.com/locate/entcs全球服务协调政策1西恩佐·钱西亚2 Gian Luigi Ferrari2 Roberto Guanciale3Daniele Strollo丹尼尔·斯特罗洛2，3摘要面向服务的方法的一个重要问题是通过可编程的协调模式聚合服务交互所涉及的活动的可能性。可以采用两种不同的方法来处理服务协调：编排和编排。在本文中，我们介绍了一个正式的方法，目的是从全局观察者的角度来处理服务之间的协调，在编舞模式的精神。特别是，我们解决的问题，验证服务交互的设计和编排约束之间的关键词：面向服务的体系结构，协调，会话，一致性1引言Web服务协议栈（例如WSDL、SOAP、SOAP）通过利用设施来发布、发现和调用网络可用服务，为面向服务的体系结构的开发提供基本支持。服务协议栈对于突出面向服务的计算方法的关键创新特性非常有价值。当前的大多数开发方法和标准都集中在服务的组合上。可以采用两种不同的方法：配器和编舞。在业务流程中，业务流程是一个中间环节，组织者负责根据工作流程计划安排服务活动。该策略提供了参与者的本地视图。另一方面，编排模型涉及所有参与方及其相关交互，提供系统的全局视图。已经出现了相关的标准技术来模拟协调政策。其中，业务流程执行语言（BusinessProcessExecutionLanguage，简称BPEL）[22]（用于编排）和Web服务（WebService）1欧盟FP 6-IST IP 16004SEN SORIA部分支持的研究2Universit`adegliStudidiPisa，DipartimentodiInformatica3Institute for Advanced Studies IMT卢卡1571-0661 © 2009 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.12.03274诉Ciancia等人理论计算机科学电子笔记260（2010）73编排描述语言（WS-CDL）[24]，用于编排。然而，这种标准存在缺陷的情况并不少见.事实上，构造常常是非正式的。这通常会导致歧义或冗余。尽管研究仍在进行中，但目前有几项研究成果正在为编配和编排提供基础模型，包括COWS[18]，Global Calculus [5]，λreq[2] ORC [21]，SCC [3]，SOCK [15]和[17]等贡献。用于指定和编程分布式系统的众所周知的范例是事件通知范例（EN，简称），其中分布式计算组件可以充当发布者和/或订阅者。当组件打算向其他组件发送数据或从其他组件请求服务时，它发出事件，该事件最终将触发来自预先订阅了这种事件的订阅者的反应EN范式提供了一个合适的框架来处理需要组件松散耦合的面向服务的体系结构具体而言，EN范式具有高级协调机制，允许程序员/设计师解耦组件并完全依赖事件处理。在[9]中，引入了一种用于服务协调的中间件，称为Java信号核心层（JSCL 中间件由一组API组成，用于编程通过合适的事件进行交互的服务。JSCL配备了一个图形环境，一个Eclipse插件，提供了设计组件及其互连的能力。JSCL APIwww.tao4ws.netJSCL的一个显着特点包括严格的相互作用之间的正式语义基础，实现语用学和实验评估所产生的编程结构。更确切地说，JSCL中所有可用的编程工具都是语义驱动的。在抽象层次上，中间件采用信号演算（SC）的形式[9，10，8]。SC演算是π演算[23]的变体，具有显式原语来处理事件通知和组件分发。SCJSCL框架允许指定和编程仅依赖于事件通知的服务协调策略（编排和编排）此外，它还将会话作为同步分布式和独立组件的工作流程的机制。值得注意的是，该中间件并没有采用任何集中的机制来发布、订阅和通知事件。相反，每个订阅者明确定义它感兴趣的事件类别。在[20]中，这种模式被称为非代理模式，与在信号分类之上实现发布/订阅机制而不考虑所涉及的组件的代理解决方案相反。基本上，代理解决方案依赖于全局状态空间，例如Linda元组空间[14]。所有的SC概念都在JSCLAPI中得到了体现。事实上，JSCL实现的设计选择已经在SC演算方面得到了正式因此，SC和JSCL可以被看作是一个描述、验证和编程分布式服务协调策略的在SC和JSCL中，组件被认为是孤立的，它们的行为独立于它们将要操作的网络上下文。只有在插入网络后，组件才会接收到有关其诉Ciancia等人理论计算机科学电子笔记260（2010）7375邻居，即直接连接的用户这与协调的局部观点相对应在本文中，我们介绍了一个正式的方法，SCJSCL框架的目的是管理服务之间的协调，从一个全球性的观察员的精神编排模型。特别是，我们解决的问题，验证服务交互的设计和编排约束之间的合规性和一致性。我们的方法是基于过程演算技术。我们引入了一个过程演算，称为网络协调政策（NCP），扩展和装备我们的框架与编排模型。这两种结石（SC和NCP）位于两个不同的抽象层次。前者是为支持服务的（正式）设计而定制的，后者是声明协调策略的规范语言。策略采取流程的形式，代表观察者从全局角度看到的行为，从而看到网络基础设施上发生的所有公共交互。因此，每个NCP过程描述了预期发生的交互，以及这些交互是如何交织的。事实上，某些特性可以在两个层次上描述：NCP规范声明了服务网络基础设施的预期，SC设计规范了如何实现它。形式上，这意味着两个演算共享相同的计算范式，并且两个语义通过正确性结果相关联：对于每个SC网络，都有一个反映网络所有属性的NCP 我们建立了一个基于语义的转换映射到一个NCP网络的SC设计的介绍，这一结果。我们表明，转换是完全抽象的一个抽象的语义概念。反之则不然：并不是每一个可以指定的协调政策都是可执行的。我们的第一个贡献是介绍了NCP过程演算。正如在π演算中一样，NCP的基本能力是范围挤出 to model模型fresh新鲜resource资源generation生成. 然而，作为新鲜度和作用域挤出对象的名称不是纯名称，而是它们携带被认为是新鲜的并且在接收时被挤出的网络拓扑。一方面，这是因为NCP的基本结构是网络拓扑，而不仅仅是通道名称。另一方面，这为进程演算中的私有子网提供了一个模型。虽然没有增加或 删除演 算的任 何表达 能力， 但这种 例如， 我们可 以提到 虚拟 专用网 络（VPN）。我们的第二个贡献是定义了NCP演算的抽象语义。抽象的语义允许我们的原因SC服务的行为时，插入到合适的网络上下文与某些编排约束。特别是，它区分在同一网络环境中行为不同的服务。这个特性对于评估服务调用在特定种类的编排中是如何成功的（例如，满足SLA约束）非常有用。从技术上讲，NCP抽象语义受到[16，1]中提出的异步π演算的“定向HT互模拟”的启发76诉Ciancia等人理论计算机科学电子笔记260（2010）73不ⓍⓍ→Ⓧ→本文的主要结果是SC在NCP中的嵌入。这个结果可以用来弥合编排模型和实际设计之间的差距：通过检查它们之间的弱双相似性，可以正式证明SC设计与NCP规范的一致性。2英文名：The Signal Calculus在本节中，我们将回顾Signal Calculus（SC）的语法和操作语义。我们假设一个可数的主题名称集合（范围为τ）和一个可数的组件名称集合A，范围为a，b，c，.。.我们采用符号a来表示一组组件名称。微积分的核心是组件的概念。组件是服务的容器。组件由名称a（服务的公共地址）唯一标识，并具有内部行为。组件交换消息，称为信号。信号是成对的主题τcτJ，其中第一个元素是信号类型（标识事件类型的唯一名称），第二个元素是是会话标识符。会话标识符和事件类型可以自由交换，并且可以动态生成。当组件（发布者）引发事件时，它会通知有兴趣处理它的组件（订阅者）。请注意，通知不是匿名的，即订阅与事件主题和发布者都相关。 因此，组件的行为就像反应性代理，它声明了它们感兴趣的事件类型集 要对其进行处理的相关任务（反应），以及用于通知传递的目标组件集（流程）。微积分提供了两种不同的反应：λ反应和检查反应。 Lambda反应独立于信号会话被激活，而检查反应处理属于定义明确的会话的信号。Lambda反应一旦被安装，就在组件接口中保持持久性，而检查反应一旦被执行，就从组件接口中移除现在我们介绍微积分的语法。 我们从解释反应的语法开始。R：：= 0|⟨ ρ ⟩ → B| R|R其中，输入的p_r_f_p_f是l_a_b_da反应（τ_c_λτJ）或c_e_k反应（τ_c_τJ）。λ反应τcλτJB由具有与其会话无关的主题τ的相反，检查反应τcτJB仅对针对会话τJ发出的具有主题τ的信号作出反应。一旦对某个信号的反应发生，行为B就开始与已经活动的行为并行执行注意，对于λ反应，名字τJ在行为B中是受约束的，而对于检查反应，它是自由的。反应组合物允许组分以不同的方式对不同种类的信号作出反应现在，我们介绍行为的语法，即构造组件执行以处理协调问题。行为由以下语法描述：诉Ciancia等人理论计算机科学电子笔记260（2010）7377⟨Ⓧ ⟩FFǁ∅⟨Ⓧ ⟩B：：=出τcτJ.B（信号发射）|（ντ）B（主题限制）|rupd（R）.BJ（最新反应）|fupd（F）.BJ(Flow更新）|B|BJ（平行构图）|0（空行为）其中a是一组形式为（τ，b）的对，其中τ是主题，b是组件名称。信号发射outτcτJ.B在网络中产生主题τ和会话τJ的信号，然后作为B继续。通过约束算子作为绑定器，可以动态地生成主题，即τ在B中的出现是绑定的。演算提供了两个原语来允许组件动态地改变其接口：反应更新rupd（R）.BJ和反应流更新fupd（F）.BJ。 前者在元件的接口部分安装一个新的反应R，后者将F附加到其支路上。其余的结构具有明显的意义。网络描述了组件分布和组件之间交换的信号。N：：=N|a[B]R|NN|⟨τⓍcτJ⟩@a| （ντ）N一个网络可以是空的，一个单一的组成部分a[B]R有名字a，安装反应R，流程F和行为B，或网络N NJ的并行组合。网络承载组件之间交换的信号对于每个目标分量，信号发射最后一个操作符允许在网络中扩展动态主题的范围。在下文中，我们假设组件通过其名称唯一标识因此，我们将始终考虑格式良好的网络，即不允许具有相同名称的组件的网络2.1SC操作语义我们简要概述了SC约简语义，如[10]中所给出的。我们首先定义结构一致性。这是满足交换幺半群定律（结合性，交换性和0是单位元）的最小等价关系（R，|，0），（B，|，0）和（N，N，N）.此外，以下定律成立，我们78诉Ciancia等人理论计算机科学电子笔记260（2010）73→F1F2FF用fn（−）表示任何实体的自由名（ντ）00，（（ντ）B）|Bj（ντ）（B|BJ），若τ∈/fn（BJ）（ντ）<$，（（ντ）N）<$NJ<$（ντ）（N<$NJ），如果τ∈/fn（NJ）（ντ）（ντJ）B（ντJ）（ντ）B（ντ）（ν τJ）N（ντJ）（ντ）N如果B≠BJ，τcλτJ→BτcλτJ →BJ（1）τcτJ→BτcτJ →BJ（2）其中τJ可以在（1）中进行α转换。最后，在网络的情况下，以下等式成立：F1<$F2B1 <$B2R1<$R2，τ∈/fn（R）<$fn（F）<${a}.a[B1] R1 [B2]R2a[（ντ）B]R（ντ）a[B]R约简语义描述了组件如何通信和更新它们的接口.图1中描绘了减少关系。归约规则的直观解释是直接的。请注意，规则emit在网络中引入了一组信封，即每个订阅者组件的信封。该规则利用辅助算子（F（τ）），定义如下：F（τ）={b|（τ，b）∈ F}规则check和lambda描述了check反应的激活，这需要会话标识符的精确匹配，以及lambda反应的激活，接收会话标识符作为参数。3编舞模式在本节中，我们将介绍网络协调策略演算（NCP）的语法和操作语义。这个演算是专门设计来 成为SC基本上，NCP是异步π演算的扩展，支持多播通信和具有隐藏网络层的多层动态拓扑。网络层是一阶实体：它们可以在通信中动态创建和交换。许多其他进程演算被设计来处理进程分布。NCP的新特性是能够限制网络拓扑的一部分诉Ciancia等人理论计算机科学电子笔记260（2010）7379∈FFJFFFFFFF FJ（面值）N→NJ（npar）NM→NJMN<$NJNJ→MJMJ < $M（struct）N→Ma[B]R−→a[BJ]RJN→N1（新）a[B]|B1]R−→a[BJ|B1]RJ（ντ）N→（ντ）N1a [rupd（RJ）.B] R → a [B] R|RJ（rupd）a [fupd（FJ）.B] R → a [B] R（fupd）F FFFFJF（τ）={b1，.， bn}（发射）a[out]a [out] B]R→a[B]Rτcτj@b1.. . ǁ⟨τⓍcτJ⟩@bnτ|R→a[B|[BJ]R（检查）τ|R→a[B| {τJ/τ1}BJ]τcλτ1→BJ|R（lambda）Fig. 1. 操作语义该语言的语法定义如下：P：：=P P|（ντ：T）P|跳过|i∈Iρi@ai。Pi|⟨τⓍcτJ⟩@a| τ τJ@a.P|fu pd（F）@a.Pρ：：=τ（τJ）|τ τ J其中T是一组形式为（a，b）的对，a/=b，称为连接。最后，I是一组有限的指数。我们用作为一种简写来表示空的保护和iρi ai.PiNCP过程称为协调策略。我们使用政策一词来强调这样一个事实，即微积分已经被引入来指定和约束SC网络的行为。一个策略ρ@a.P从全局的观点描述了组分a对反应ρ的执行，其延续为P。除了反应，我们还有其他形式的预固定。Prefixτ（τJ）描述了通过侦听主题τ来接收任何主题作为输入的动作。我们称这种操作为lambda操作，因为它是定制的描述SCλ反应。类似地，PrefixττJ描述了接收具有主题τ和会话τJ的信号的动作。我们称之为检查这个动作。后面会更清楚，上面的两个操作lambda和check为NCP提供了一80诉Ciancia等人理论计算机科学电子笔记260（2010）73种（受限的）递归形式和一种（受限的）匹配形式。动作ττJ@a.P描述了由组件a在会话τJ上针对那些服务的包络的发射，诉Ciancia等人理论计算机科学电子笔记260（2010）7381--⟨Ⓧ ⟩g×− {|∈}−正在收听主题τ。动作fupd（F）允许描述更新SC组件的链接的操作。 信封τcτJ@a表示一个消息（其目的地是a）仍然在网络中挂起。请注意，生成封套的源组件不会被记住。（ντ：T）P定义了主题τ的范围，在策略P中有一个相关的链接T，代表一个隐藏的网络层。假设主题τ是新鲜的。例如，约束（ντ：（a，b））P扩展了网络拓扑，其中a和b之间的新链接用于新主题τ。请注意，此机制允许通过名称限制来表示网络隐藏，并通过名称绑定来表示多层网络范围。最后，策略skip.P表示在执行P之前执行内部活动。保单的自由名fn（P）和绑定名bn（P）的定义与通常一样。NCP的操作语义从全局的角度定义了策略的含义。由于策略不仅描述了组件之间的交互，而且还反映了网络中事件拓扑的结构，因此我们需要引入一个合适的状态概念定义3.1我们将主题驱动拓扑定义为一组三元组（a，τ，b），其中a，b是组件名称，τ是主题名称。在下文中，我们使用μ来涵盖主题驱动的拓扑。我们介绍了一些有用的辅助操作的主题驱动拓扑。• 设μ是一个主题驱动的拓扑，a是一个组件名，F是一个流。定义μ（a×F）为主题驱动拓扑μ {（a，τ，b）|（τ，b）∈ F}.• 设μ是一个主题驱动的拓扑，设τ是一个主题。 定义μ（τ）为连接{（a，b）|（a，τ，b）∈ μ}。类似地，函数μ（τ）（a）被定义为集合{b| （a，τ，b）∈ μ}。• 设μ是一个主题驱动的拓扑，设τ是一个主题名，T是一个链接。 定义μ（τT）为主题驱动拓扑μ（a，τ，b）（a，b）T，其中表示集合之间的差异。• 设μ是一个主题驱动拓扑，n（μ）表示μ中出现的所有名字的集合。定义3.2设μ为主题驱动拓扑，P为协调策略，则（μ，P）对称为NCP状态。我们现在介绍NCP的标记转换系统语义。操作规则在精神上类似于Honda和Tokoro [16]以及Amadio、Castellani和Sangiorgi [1]在异步π演算情况下给出的规则。我们的操作语义利用主题驱动拓扑的概念来显式地管理编排的全局视图。实际上，协调策略的评估取决于网络拓扑的状态。这使我们能够以自然的方式对多播通信进行建模。例如，在动作ττJ中监听主题τ不足以接收关于该主题的消息。事实上，我们要求拓扑必须链接主题τ的发送者和接收者。我们首先引入作用集α。82诉Ciancia等人理论计算机科学电子笔记260（2010）73⟨Ⓧ⟩⟨Ⓧ ⟩⊗×g×α：：=α| ττJ@a| （ττJ@a）|⟨τⓍcτJ⟩@a| τ动作模型模拟了不可观察的活动，比如内部通信。动作τcτJ@a是类型τ、会话τJ和目的地a的自由（异步）事件通知。动作τc（τJ：T）@a表示一个绑定事件通知;利用链接TActionττJ @a是一个自由反应激活，它的灵感来自早期实例化风格中的asyn-π -演算的语义。最后（ττJ@a）表示接收消息并与当前进程并行存储的动作。这种行为在任何系统中都可以观察到，因此包括空策略。在下文中，我们用n（α）来表示动作α中的名称集合。NCP的标记转换系统语义由图2中描述的规则定义，其中，n表示语法恒等式模α−转换。我们使用μ，P−→αμJ， PJ表示协调策略P，插入到拓扑中通过执行动作α，μ演化为策略PJ，网络拓扑演化为μJ。为了简单起见，我们省略了par、com、close、new和open的对称规则。规则struct和par具有标准含义。Skip表示内部计算。Fupd扩展了主题驱动的拓扑μ，其中链接从a导出，该链接从子流信息F导出。 规则发出对异步多播通信进行建模。 该规则检查拓扑（μ（τ）（a））的状态以导出主题τ的订户组件的集合。然后，对于每个订户，将一个信封生成到网络中。规则notify描述了将一个信封通知给一个组件，并对应于异步π演算的输出规则规则检查和lambda模型反应的执行。如果选择检查反应（Pj=ττJ），则策略可以仅读取具有相同主题和会话的信封。如果选择了lambda反应（ρj=τ（τJ）），则策略可以独立于接收到的会话τ j的身份和链接T（τJ和T充当变量）读取具有主题τ的任何信号。换句话说，它对接收到的会话和关联的链接执行早期实例化。请注意，在通信发生后，所有竞争对手的输入都将被丢弃。与异步π演算中的规则一样，规则Bclc允许任何策略执行输入，简单地存储接收到的消息以供后续使用（因此允许任意延迟通信）。规则com允许不在限制范围内的会话（τJ）的通信规则new允许我们为新生成的主题（τ）扩展拓扑（μ（τ T））。 请注意，该规则隐藏了主题拓扑的更新依赖于其范围之外的生成名称（μJ（τJTJ））。最后，规则打开和关闭模型名称（τJ）的作用域挤出，以及它的绑定通信。3.1示例为了更好地突出NCP的主要功能，我们介绍两个简单的例子。我们还请读者参考[6]，以了解我们将在哪些情况下诉Ciancia等人理论计算机科学电子笔记260（2010）7383−−−−−−→−−−−−−→−−−−−−−−−→αμ，ττ@a.P−→μ，P⟨τⓍcτ⟩@bp@a.P−−−−→我我 i−→JJ12Σμ，skip.P−→μ，P（跳过）μ，fupd（F）@a.P−→μ（a×F），P（fupd）μ（τ）（a）=b（）下一页j∈I pj =ττJ（检查）吉吉b∈b发射μ，我i∈IττJ@a我 我Jj∈I pj =τ（τJJ）（lambda）μ，μp@a.PττJ@ajμπ（τJ×T），{τJ/τJJ}Pp@a.Pi∈I（通知）（c）μ，τcτJ@aτcτJ@aμ，（ττJ@a）−−−−−→ μ，PτcτJ@aτJ∈n/（μ） μπ（τJ×T）， P<$τcτJ@aμm（τJ×T），PJ（开放）μ，. ντJ：T<$P<$τ<$c（τJ：T）<$@aμm（τJ×T），PJμ，PττJ@a μJ，PJμ，PτμJ，PJ1−−−−→12−−−−−−−−→2（close）μ，P1<$P2−→μ，. ντJ：T（PJ<$PJ）τ∈n/（α）<$n（μ）μ<$（τ×T）， P−→μJ， PJ TJ=μJ（τ）（新）μ，（ντ：T）P−→αμJg（τ×TJ），. ντ：TJ<$PJμ，PττJ@a μ，PJμ，P⟨τⓍcτJ⟩@aμ，PJ1−→12−→2（com）μ，P1<$P2−→<$μ，PJ<$PJμ，P−→αμJ，PJ1 2μ，Pμ，P−→μ，PμJ，PJ（面值）n112 2N（struct）μ，P<$P1−→αμJ，PJP1μ，P−→αμJ，PJ图二. LTS语义我喜欢使用SC和NCP建模，[11]对于使用SC/NCP框架解决与代码重构相关的问题Jμ，Pαμ，PJJ84诉Ciancia等人理论计算机科学电子笔记260（2010）73. Σ3.1.1NCP隐藏通信设μ为主题拓扑。下面的NCP状态描述了组件b引发事件的演变，该事件与a接收到的事件具有相同的会话：μ，τ τJ@a.skip.τ1τJ@b直观地说，该规范对协调策略进行建模，其中组件a可以接收具有主题τ的信号。在一些内部活动已经发生之后，组件b产生具有与由组件b接收的信号相同的会话（τJ）的信号。诉Ciancia等人理论计算机科学电子笔记260（2010）7385--єєєa.该行为约束组件a和b交换所接收的会话的名称τJ，然而，该通信未被显式地表示。操作规则lambda、skip和emit详细说明了所需的行为。lambda规则处理输入的早期实例化，允许任何名称τJJ的转换。请注意，lambda反应仍然处于活动状态，并且由组件b生成的信封具有与接收到的信封相同的会话。下面给出了实际的操作推导μ，τ（τJ）@a.skip.τ1τJ@bττJJ @ aє є−−−−→−→−→μ，τ（τJ）@a.s kip. τ1τJ@b<$c∈μ（τ1）（b）<$τ1 <$cτJ J<$@c3.1.2拓扑的NCP范围令μ=（a，τ，b））描述从组件a到主题τ的分量b。让我们考虑下面的NCP状态。μ，τ（τ1）@b. τ1τs@a（. ντJ：<$σfu pd（{（τJ，b）}）@a. ⟨τⓍcτJ⟩@b)当协调开始时，主题τJ的拓扑隐藏在并行策略的右侧部分之外。对b分量的信号的接收（通过lambda反应）在拓扑中执行了名字τJ因此，a可以向接收者b发射具有τJ的信号。上述行为由以下运算推导表示。μ，fu pd（{（τJ，b）}）@a. ⟨τⓍcτJ⟩@b−→μ{（a，τJ，b）}，τcτJ@bμ，（vτJ：b）fu pd（{（τJ，b）}）@a. ⟨τⓍcτJ⟩@b−→μ，（ντJ：{（a，b）}）τcτJ@bμ，τ（τ1）@b. τ1τs@a（（τJ：b）fu pd（{（τJ，b）}）@a. ⟨τⓍcτJ⟩@b)−→μ，τ（τ1）@b. τ1τs@a<$（（ντJ：{（a，b）}）<$τ<$cτJ <$@b）86诉Ciancia等人理论计算机科学电子笔记260（2010）73⟨ Ⓧ ⟩联系我们єα1−−−−−−−−−→111222−−−−−−−−−→221122然后，两个并行策略可以通信，挤出τJ链接：μ{（a，τJ，b）}，τcτJ@bτcτJ@b−−−−−−→μπ {（a，τJ，b）}， μ πμ，τ（τ1）@b.τ1 τs@aττJ@b−−−→μπ {（a，τJ，b）}，τJτs@aμ，（ντJ：{（a，b）}）τcτJ@bτc（τJ：（a，b））@b−−−−−−−−−−−−→μπ {（a，τJ，b）}， μ πμ，τ（τ1）@b. τ1τs@a<$（（ντJ：{（a，b）}）<$τ<$cτJ <$@b）−→μ，（ντJ：{（a，b）}）（τJτs@a τ s）3.2互模拟语义为了结束本节，我们介绍NCP的黑盒语义，其形式为一个互模拟关系。Honda-Tokoro [16]和Amadio等人 [1]研究了异步演算的双相似性。我们使用这些结果（特别是[1]中的有向HT标记转移系统）来定义我们的互模拟语义。遵循这些方法，在互模拟博弈中，任何进程都可以充当“缓冲器”，读取任何可能的消息并存储它，而不消耗消息。在我们的情况下，这是根据规则10.c进行的。另一方面，在互模拟博弈中根本观察不到实际消耗消息的“有效”输入，而由这些输入引起的同步却被观察到。因此，在定义双相似性时，我们考虑了由规则bk c引起的跃迁，而不是由check或lambda得到的跃迁。定义3.3给定两个协调策略P1和P2，以及两个主题拓扑μ1和μ2，互模拟关系<$1是最大对称关系，使得对于每个（μ1，P1）<$（μ2，P2），以下成立：• 对于每个变换μ1，P1-→μJ， P J，其中α∈{α，ττcτJα，（ττJα）}，则re是a过渡αJ J1 1J J）（JJ）。μ2，P2−→μ2，P2和（μ1，P1 ∼ μ2，P2• 对于每个跃迁μ，PτμJ， PJ，其中τJ∈/fn（P），re是一个变换，μ，PτμJ，PJ和（μJ，PJ）<$（μJ，PJ）.NCP和异步π演算的一个关键区别是在语义上对主题拓扑的感知。但是，如果要求只有具有相同拓扑的策略才可以是双相似的，则限制性太强。例如，空网络在任何拓扑下都与自身双相似。这也反映在约束输出子句的定义中：当约束输出转换在互模拟关系中匹配时，与诉Ciancia等人理论计算机科学电子笔记260（2010）73870==并将其映射到策略中。函数定义如下：没有考虑过渡，因此可以是不同的。弱转移关系以标准方式定义μ，P=μJ， PJiffμ，P（−→）μJ， PJμ，P=αμJ， PJiffμ，P=α. −→α . =μJ，PJ（对于α）最后，弱互模拟的定义是通过用定义3.3中的弱互模拟替换强标记跃迁而得到的。显然，μ，P <$μJ，PJ意味着μ，P<$μJ，P J。4检查编排在本节中，我们将介绍一种形式化的方法，用于根据NCP规范给出的全局协调策略来验证SC组件网络的正确性。我们的方法的第一步包括提供从SC网络到NCP策略的编码编码的基本思想是将SC反应转化为标记为NCP的NCP跃迁。编码函数B采用SC行为B，其被定位在compo内。新界东北 ，并将其映射到策略中。 该函数定义如下：一0a=NCPJa=BaBJ）a（1）B|B）<$（ντ）B）a=（ντ：π）<$B）a<$outπτπcτJπ。B）a=ττJ@a。（B）aB）a=skip. <$R）a<$B）a<$fupd（F））a= fupd（F）@ a。（B）a功能 R取一个SC反作用R，安装在组件的接口（1）J J（1）a ）a|R）a<$R）a<$<$R）a<$τ_cτ_J→ B）a=τ_J@a。<$B）a<$τcλτJ→ B）a=τ（τJ）@a. （B）a最后，函数 N 取SC网络N并将其映射到NCP状态。 的函数定义如下：88诉Ciancia等人理论计算机科学电子笔记260（2010）73（2）CF（2）（2）（F）¢<$）=，<$$>τCτj@a）=，<$τcτJ@a=J=JJ=μ，P T=μ（τ）NN μ，P N μ，P<$N<$NJ）=μ<$μJ，P<$PJ<$（ντ）N<$））=μg（τ×T），（ντ：T）Pa[B]R =μ，B）aA、R）a其中μ=μa×F编码的正确性是“高达”双相似性，如以下定理所示。定理4.1设N和NJ是SC网络。 N→ NJ当且仅当（μ，P）和（μ，P）（NJ）<$N）−→证据（概要）证明是通过对SC网络的结构（并行组合的情况利用了一个弱化引理，该引理显示了NCP互模拟关于网络上下文的组合性：如果（μ，P）<$（μJ，PJ），则对于每个图σ，我们有（μ<$σ，P）<$（μJ<$σ，PJ）。Q前面的定理使我们能够推导出一个供应链网络的编排模型。我们方法的下一步是使验证成为组合。 一旦一个编排被验证，它应该可以“插入”将其转换为组件的分布式网络，而不改变已验证的属性。 这一点在本节的其余部分中得到了正式的说明首先，我们必须定义SC网络上下文。我们用发生的概念一个术语中的一个符号，以及可以用标准方式定义的替换定义4.2单孔SC网络上下文的集合被定义为由以下语法生成的术语的最小子集，其中占位符的出现次数为1。C：：=| a[B]R| C C|⟨τⓍcτJ⟩@a| （ντ）C| ∗设C ∈ C，N为SC网络。 C的应用C [N]到N被定义为在C中出现一次的N的句法替换。我们有以下的组合结果。定理4.3设N1和N2是SC网络， N1 ∼ N2. 为所有C∈ C，则 C [N1] ∼ C [N2]。证据 （提纲）证明是通过对上下文结构的归纳来完成的，通过互模拟关系的共归纳。很容易看出，对于N网络和τ主题名，只有两种单洞上下文是可能的，即（ντ）和N。有趣的上下文是形式（ντ）的上下文，特别是є诉Ciancia等人理论计算机科学电子笔记260（2010）7389（Ⅲ）图3.第三章。符合模型驱动开发中的规范当在共同归纳方案中考虑开放规则时，问题在于，该图拓扑结构是不确定的。然而，在到达的状态（通过一个绑定的输出转换）的互模拟关系被限制到那些观察，其主题是不受限制的名称，因此它是保持在一个步骤，然后通过共归纳，我们得到的证明。Q把本节的内容放在一起，我们有一个策略满足的定义：设N是一个SC网络，P是一个NCP策略，设μ表示一个主题驱动的拓扑。我们说N实现提供的编排（μ，P）则N<$（μ，P）。 使用弱互模拟，内部计算步骤可以是丢弃。这在通过互模拟验证服务时很常见，如果考虑到演算的异步性质，这是有用的，这会在产生或消费消息时引入额外的计算步骤这种满意度的定义是一个基于语义的概念，至少对于利用双模拟检查技术（如[13]）的有限状态系统可以进行机械检查。这种满意度的概念可以支持模型驱动开发方法中的系统开发。例如，设计人员可以开发几个实现相同高级策略的SC系统，每个系统都通过添加更多细节来完善前一个系统。 一致性 每个设计的NCP策略规范可以通过我们的技术正式验证。图4说明了这种方法。5总结发言在本文中，我们扩展了SCJSCL框架的编排模型：NCP演算。我们已经提出了一个编码的设计语言（SC）的编排语言，以验证SC网络是否尊重全球NCP政策。这是通过互模拟检查完成的一些研究工作已经解决了将编舞和配器联系起来的问题。例如，已经考虑了仿真一致性的概念[4，19]。[5]中还考虑了提供单独语言来描述服务协调的全局和局部视图的方法论思想。然而，我们的框架引入了一些新的概念，如多层网络和多方会话。我们的长期目标是提供模态逻辑和模型检查算法，基于NCP的标记语义定义。此外，我们计划90诉Ciancia等人理论计算机科学电子笔记260（2010）73在JSCL设计环境中实现和集成这些验证技术，可能会开发[12，13，7]中开发的标称演算的有限状态技术。引用[1] 阿马迪奥河M.，I. Castellani和D. Sangiorgi，关于异步π演算的互模拟，Theor。Comput. Sci. 195（1998），pp.291-324。[2] Bartoletti，M.，P. Degano，G. Ferrari和R. Zunino，Secure service orchestration，in：FOSAD，Lecture Notes in Computer Science4667（2007）。[3] Boreale，M.，R. 布鲁尼湖凯尔河D. 尼古拉岛拉尼斯湾Loreti，F.马丁斯大学Montanari，A.拉瓦拉D. Sangiorgi，V. T. Vasconcelos和G. Zavattaro，Scc：以服务为中心的微积分。WS-FM，Lecture Notes inComputer Science4184（2006），pp.38比57[4] Busi，N.，R. 戈列里角圭迪河Lucchi和G.Zavattaro，Choreography and orchestration：A synergicapproach for system design，in：ICSOC，Lecture Notes in Computer Science3826（2005），pp.228-240[5] Carbone，M.，K. Honda和N. Yoshida，Structured Communication-Centered Programming for WebServices，ESOP 2007，Lecture Notes in Computer Science4421（2007），pp.2-17[6] Ciancia，V.，G. L. 费拉里河，巴西-地Guanciale和D.Strollo，Checking Correctness of TransactionalBehaviors，Forte，Lecture Notes in Computer Science5048（2008），pp.134-148。[7] Ciancia，V.和U.杨文，一种新的命名集的抽象函子，电子笔记理论。Comput. Sci. 203（2008），pp.49比70[8] Ferrari，G. L.， R. Guanciale 和D. Strollo，基于 事件的动 态和异构 网络服务 协调。 ，在 ：A.丹和W.Lamersdorf，编辑，ICSOC，Lect. Notes in Comput. Sci. 第4294（2006）号来文，第4294（2006）页。453-458[9] Ferrari，G. L.，R. Guanciale和D. Strollo，Jscl：一个用于服务协调的中间件。Forte，Lecture Notes inComputer Science4229（2006），pp.46比60[10] Ferrari，G. L.，R. Guanciale，D. Strollo和E. Tuosto，基于事件的框架中类型的协调，第27届IFIP WG6.1网络和分布式系统形式方法国际会议FORTE4574（2007），pp。66比80[11] Ferrari，G. L.， R. Guanciale，D. Strollo和E. Tuosto，Refactoring long running transactions，in：WS-FM，《计算机科学讲义》（Lecture Notes in Computer Scienceto appear，2008）。[12] Ferrari ， G. L. ， 联 合 Montanari 和 M. Pistore ， Minimizing Transition Systems for Name PassingCalculi：A Co-algebraic Formulation，in：M. Nielsen和U. Engberg，编辑，FOSSACS 2002，讲义计算机科学2303（2002），pp。129比143[13] Ferrari，G.L.，联合Montanari和E.Tuosto，Coalgebraic minimization of hd-automata for the pi-calculus using polymorphic types. ，Theor。Comput. Sci. 331（2005），pp.325-365[14] Gelernter，D.，Linda，ACM Transactions on Programming Languages and Systems7（1985），pp.80比112[15] 圭迪角，R.卢基河Gorrieri，N. Busi和G. Zavattaro，A calculus for service ori