符号语义中的面向服务计算

理论计算机科学电子笔记241（2009）135-164www.elsevier.com/locate/entcs面向服务计算演算的符号语义1罗萨里奥·普利亚塞2DipartimentodiSistemieInormatica，Universita`degliStudidiFirenze吉田伸子4伦敦帝国理工学院计算机系摘要我们介绍了一个符号表征的操作语义的COWS，一种正式的语言，用于指定和组合面向服务的应用程序，同时建模他们的动态行为。由于COWS中通信的值传递性质，这种替代语义避免了COWS术语的无限表示，并且更适合分析工具的自动操作，例如例如等价和模型检查器。 我们通过一个保留字：面向服务计算，服务编排，流程演算，符号语义。1介绍近年来，电子商务、电子学习、电子政务和其他类似的新兴模式的日益成功，已经导致万维网，最初被认为是人类使用的系统，向支持自动化使用的面向服务的计算（SOC）的体系结构发展SOC提倡使用松散耦合的“服务”，将其理解为自治的、独立于平台的、计算实体，这些实体可以被描述、发布、发现和组装，作为构建可互操作和可演进的系统和应用程序的基本块。虽然至少部分面向服务的技术的早期例子可以追溯到1这项工作得到了欧盟项目SENSORIA，IST-2 005-016004、EPSRC项目GR/T03208、GR/T03215、EP/F003757和欧盟项目MOBIUS，IST 2005-15905的支持。2电子邮件：pugliese@dsi.unifi.it3 电子邮件地址：tiezzi@dsi.unifi.it4电子邮件：yoshida@doc.ic.ac.uk1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.06.008136R. Pugliese等人理论计算机科学电子笔记241（2009）135回到CORBA、DCOM、J2EE和IBM WebSphere，SOC范例最成功的实例可能是最近的Web服务。这些是可以通过符合给定标准格式的XML消息通过Web发布、定位和调用的操作集。为了支持Web服务方法，设计了几种新的语言和技术，许多国际公司也投入了大量的资金。然而，目前的SOC软件工程技术仍然停留在描述层面，缺乏严格的形式化基础。在SOC应用程序的设计中，我们仍然经历着实践（编程）和理论（形式化方法和分析技术）之间的这些挑战来自于必须同时处理诸如异步交互、并发活动、工作流程协调、业务事务、故障、资源使用和安全性等问题，在这种情况下，许多不同的组件的需求和保证可能非常不同。因此，许多研究人员提出了使用进程演算的想法，这是当前通过数学方法对并发、分布式和移动系统进行规范和分析的- 主要是代数和逻辑工具。事实上，由于其代数性质，进程演算以提炼的形式传达了SOC的组合编程风格。因此，已经设计了许多进程演算（例如[9，8，16，13，10，15，4，6，27]），解决SOC的一个方面或另一个方面，并旨在评估不同的原语集合的适当性。建模、组合和分析面向服务的应用程序。通过从众所周知的流程演算和Web服务编排的标准语言WS-SQL[22]中获得灵感，在[17]中，我们设计了COWS（Web服务编排演算），这是一种用于规范和组合面向服务的应用程序的流程演算，同时对其动态行为进行建模。我们已经表明，COWS可以建模和处理（Web）服务的独特功能，例如，基于相关性的通信、补偿活动、服务实例和它们之间的交互、服务实例和服务定义之间的竞争条件。使用进程演算的一个主要好处是，它们拥有丰富的优雅元理论、证明技术和分析工具，这些都可能适合SOC的需求。关于这一点，在[12]中，我们开发了一个逻辑和一个模型检查器来表达和检查COWS中指定的服务的功能属性，而在[24]中，我们研究了COWS的观察语义理论。然而，这些工具缺乏组合性和效率。实际上，一般来说，模型和等价检查器，以及其他类似的验证工具，并不直接作用于语法规范，而是作用于过程行为的因此，对于值传递语言，如COWS，使用不适当的表示可能导致不可行的验证。实际上，根据COWS这种表示是一种标记转换系统，R. Pugliese等人理论计算机科学电子笔记241（2009）135137初始状态有无限个向外的边，每个边都标有一个输入标签，该标签具有不同的值作为参数，并导致不同的状态。因此，受Hennessy和Lin [14]的启发，在本文中，我们定义了COWS的符号操作语义。不同于更标准演算的符号语义，如值传递CCS或π演算，我们的处理，除了接收转换，一个复杂的功能，如，例如，新名称的生成和输出、模式匹配、表达式评估以及冲突接收者之间的优先级。由于COWS中通信的值传递性质，新语义避免了COWS术语的无限表示，并将有限表示与每个有限COWS术语相关联。然后，它更适合于通过分析工具（例如等价性和模型检查器）进行自动操作。我们的主要结果是一个“运算对应”定理我们证明，在适当的条件下，任何转换的原始语义可以产生使用的符号，反之亦然。然而，一般来说，可以使用符号语义来导出额外的转换，因为它还考虑了服务与环境交互的能力论文的其余部分组织如下。第2节提供了COWS的符号语义的一些动机，这是通过一个第三节介绍了COWS的原始语法和操作语义。第4节介绍了COWS操作语义的符号变体和我们的主要结果，以及一些澄清的例子。第5节展示了符号语义的扩展，用于处理多元通信。最后，第6节涉及与相关工作的比较和未来工作的方向。2A ‘translation service’在本节中，我们将逐步介绍COWS的主要功能和语法，同时对意大利语-英语翻译服务进行建模通过这个场景，我们讨论了一些验证问题，并提出了COWS符号操作语义背后的主要直觉。目前，我们使用COWS的一元变体，即我们假设调用和接收活动每次可以携带一个参数。事实上，为了便于展示，在第4节中为一元变体引入了符号语义，然后在第5节中扩展到多元通信。让我们考虑一种向其客户提供意大利语-英语翻译服务的服务。具体来说，当客户调用服务时，首先发送她的合作伙伴名称，然后发送意大利语单词，它将使用相应的英语单词或字符串可以在COWS中提供服务的高级规范，如下所示：[x]t·req？X. [y] t·word？y. x·resp！transmitting（1）其中t是翻译服务合作伙伴名称，req、word和resp是操作138R. Pugliese等人理论计算机科学电子笔记241（2009）135names，x和y是分别存储客户合作伙伴名称和要翻译的意大利语单词的变量，transs（）是一个total函数，它将意大利语单词的大子集映射到相应的英语单词，并为所有未出现在意大利语单词集中的单词返回字符串该服务简单地执行一系列的两个接收活动t·req？x和t字？y，对应于接收到客户发送的请求和意大利语单词，并通过调用活动x·resp！transs（y）.接收和调用是COWS提供的基本通信活动。除了输入参数和发送的值之外，它们还指示端点，即由伙伴名称p和操作名称o组成的对p · o，通过该对p·o进行通信。与大多数进程演算不同，COWS中的接收活动既不绑定名称也不绑定变量。唯一的绑定构造是定界：[e]s在作用域s中绑定定界元素e（定界元素的绑定和自由出现的概念相应地定义）。例如，service（1）使用定界运算符来声明变量x和y的作用域。当同一端点上的接收和并发调用的参数匹配时，就会发生服务间通信，并导致将接收的变量参数替换为调用的相应值参数（在变量声明的范围内）。例如，变量x将由客户提供数据的第一个接收活动初始化。在较低的级别上，服务可以通过使用并行组合操作符组合的三个实体来描述|这允许它们被同时执行并彼此交互。 翻译服务的低级COWS规范可以是[reqDB1，reqDB2，respDB1，respDB2]（转换器|DB1 |DB2）（2）这里使用定界运算符来声明reqDB1、reqDB2、respDB1和respDB2是三个组件Translator、DB1和DB2已知的私有操作名，并且只对它们已知（至少在最初，因为在计算期间私有名称可以像π演算中一样导出）。三个子服务定义如下：译者[x]t·req？X. [y]t·word？y.[k]（t·reqDB 1！y|[x1] t·respDB1？x1. （kill（k）|{1}|x·resp！X1|）的文件|t·reqDB2! y|[x2] t·respDB2？X2. （kill（k）|{1}|x·resp！X2|}））DB1t·reqDB1？““+t·reqDB 1？““加... + t·reqDB 1？“zucca“.t·respDB1！“DB2[z]（t·reqDB2？z. t·respDB2！“+t·reqDB2？““+t·reqDB2？““加... + t·reqDB2？“zuppo“.t·respDB2！“浸泡“）R. Pugliese等人理论计算机科学电子笔记241（2009）135139ServiceTranslator是可公开调用的，可以与客户交互，而不是与“内部”服务DB1和DB2交互这后两个服务，相反，只能由翻译器调用（事实上，它们使用的所有操作都受到限制），并在数据库中查找对应于给定意大利语的英语单词特别是，DB1在一个小的常用词数据库中执行快速搜索，而DB2在一个更大的数据库中执行较慢的搜索（这与函数transs（）建模的数据库完全对应）。在两次初始接收之后，例如出于性能或容错的目的，转换器并发地调用服务DB1和DB2当其中一个回复时，翻译器立即停止另一个搜索。这是通过执行kill活动kill（k）来完成的，它强制终止封闭[k]中所有未受保护的参数，从而停止kill效应。然后，Translator将响应转发给客户并终止。Kill活动相对于其他并行活动被急切地执行，但是关键代码可以通过使用保护操作符{||};这确实是响应x·resp的情况！x1在我们的例子中 服务DB1和DB2使用choice操作符+来选择替代行为：可以通过执行与引导行为的receive匹配的调用来选择其中一个。如果要翻译的单词是未知的，DB1不回复，而DB2返回字符串实际上，并行组合的语义避免了DB2在已知单词的情况下返回 这是通过将接收t·reqDB2？z优先级低于其他receive活动，因此只有当其他receive活动都不匹配要翻译的单词时才执行（有关COWS优先级语义的更多详细信息，请参见第3节）。现在，关键是等价和模型检查器，以及其他类似的验证工具，并不直接作用于上面的语法规范，而是作用于过程行为的更抽象的表示。因此，使用不适当的表示可能导致不可行的验证。在本节的其余部分，我们将讨论验证问题以及如何利用符号方法来处理这些问题。核查问题。当所考虑的规范语言是值传递进程代数并且值空间是无限的时，使用标准的标记转换系统（LTS）进行语义可以导致无限表示。例如，服务（1）的操作行为可以由图1左侧的无限LTS表示，其中节点表示状态，边缘表示从上到下隐式定向的状态之间的转换。值得注意的是，为了便于展示，图中所示的LTS依赖于早期风格的操作语义，其中在推断接收动作时应用替换。然而，在后期语义的情况下，无限表示的问题仍然存在必须在x的所有可能替换下考虑变量x。象征性的方法。为了解决上述问题，Hennessy和Lin在[14]中引入了所谓的符号LTS，并使用它们来定义有限语义。140R. Pugliese等人理论计算机科学电子笔记241（2009）135−−−−→图1.一、用于翻译服务的LTS和符号LTS（高级规范）价值传递CCS条款的实际表示。例如，在图1的右手侧示出了对应于COWS服务（1）的符号LTS。象征性的行动t·req？x和t字？y表示分别沿端点t·req和t·word接收未知值x和y;条件保护符号动作（z=transs（y），x·resp！z）表示发送未知值z，使得z=transs（y）。当然，出于同样的原因，表示服务行为（2）的LTS也是有限的，而相应的符号LTS也是有限的。实际上，如果为了呈现的目的，我们假设数据库DB1仅包含单词“a“的关联，将符号方法应用于COWS。这项工作的主要贡献是发展的一个象征性的操作语义COWS。为了实现这个目标，主要的问题是给接收活动一个正确的语义，因为它们的参数中的变量是要接收的东西的占位符。比如让p·o？X我们认为服务P·O？x.s. 如果p·o？x.s−→s，则必须在所有形式的替换下考虑延续服务{x <$→ v}（即s的语义可以直观地被认为是函数λx。从价值观到服务）。例如，在π演算的标准语义[21]的情况下，这个问题不在操作语义级别解决，而是推迟到观察语义级别。 事实上，在迟到a（x）π演算的互模拟，当P与Q互相似时，如果P−→PJ然后那里是QJ，使得Qa（x）QJ和P J{u/x}对每个u都与QJ{u/x}双相似。因此，在本发明中，在x的所有替换下考虑延拓PJ和QJ。相反，这里我们的目标是为COWS定义一个操作语义，它可以正确处理输入转换，并允许有限状态LTS与有限COWS术语相关联基本思想是允许接收活动通过执行与“外部世界”（即COWS上下文）的通信来进化为了避免无限分支（如早期操作语义的情况），我们将变量替换为R. Pugliese等人理论计算机科学电子笔记241（2009）135141图二、用于（简化）翻译服务的符号LTS（低级规范）未知值，而不是特定值。我们用x表示替换变量x的未知值。这样，项[x]（p·o？X. q·oJ！x）可以演变如下：Jp·o？[x个]Jq·oJ！X[x]（p·o？X. q·o！x）−→q·o！x−→0还接收具有值作为参数的活动（例如，p·o？v）和调用活动（例如，p·o！（5）可以通过与外部世界的交流而进化当然，这种沟通不会产生替代。当发生外部通信时，延续服务的行为取决于未知值的可接受值。为了处理未知值可以假设的真实值，我们为COWS定义了一个符号语义，其中每个转换上的标签都有两个组成部分：启用转换必须满足的条件以及转换的动作此外，为了存储到达状态所必须满足的条件和沿着路径导出的名称，我们定义了Φ， Δs形式的配置的语义，称为受约束的服务，其中条件Φ和名称集合Δ用于确定s可以执行的操作。因此，跃迁的形式为Φ， ΔεsΦJ，α1>−−−→ΦJ， ΔJ≠2，意思是“如果条件ΦJ（使得Φ是ΦJ的子项）成立，则s1可以通过将导出的私有名称集合Δ扩展到集合ΔJ“来执行导致s2的动作α与COWS术语相关联的符号LTS以提炼的形式传达关于术语行为的所有语义信息更具体地说，除了接收转换之外，符号表示还考虑了新名称的生成和导出、模式匹配、表达式评估以及冲突接收之间的优先级在操作语义级同时处理所有上述特征使得COWS的符号语义的开发比更标准的演算（例如值传递CCS或π演算）更复杂142R. Pugliese等人理论计算机科学电子笔记241（2009）135杀手标签：k，kJ，. . .元素（即 Killer labels/Variables/Names）：e，eJ，. . .表达式：，J，.变量/名称：u，uJ，.. .Variables：x，y，. . .Variables/Values：w，wJ，. . .值：v，vJ，.. .名字：n，m，. . .终点：合伙人：p，pJ，. . .无变量：p·o，.. . ，n，m，.. .操作：o，oJ，. . .可以包含变量：u·uJ，. ，u，uJ，. . .服务项目：s：：=kill（k）（杀死）接收保护选择：G：：=0（无）|u·uJ! є¯（invoke）|p·o? w'. s（请求处理sing）|g（接收保护选择）|S|s（平行组合）|{|S|}（保护）|[e] s（划界）|∗s(replication)|g+ g(choice)表1COWS语法3COWS及其标准操作语义COWS（Calculus for Exploration of Web Services，[17]）是最近设计的一个过程演算，用于指定，组合和分析面向服务的应用程序，同时对其动态行为进行建模。COWS以独创的方式结合了许多从众所周知的工艺结石中借来的成分，例如：异步通信、多元同步、模式匹配、保护、定界接收和终止活动，而结果与它们中的任何一个都不同。在本节中，我们将介绍COWS的标准语法和操作语义。对于感兴趣的读者，我们参考[17]中的许多示例，这些示例说明了COWS的特性和表达能力，并与其他基于过程的形式主义和编排形式主义进行了比较COWS的语法如表1所示。它是由三个可数和成对不相交的集合参数化的：（杀手）标签集，值集和“一次写入”变量集 值的集合是未指定的;然而，我们假设它包括名称的集合，主要用于表示合作伙伴和操作。该语言还通过一组表达式进行参数化，这些表达式的确切语法被故意省略。我们只是假设表达式至少包含值和变量，但不包含杀手级标签，因此，杀手级标签是不可传递的值。这样，killer标签的作用域就不能被动态扩展，而其终止将被kill强制执行的activity可以被静态确定。 伙伴名称和操作名称可以组合起来指定通信端点，写为p·o，并且可以进行通信，但是动态接收的名称只能用于服务调用（如Lπ [20]）。实际上，接收活动的通信端点是静态标识的，因为它们的语法只允许使用名称而不允许使用变量。 还要注意，要对异步通信建模，调用活动不能用作前缀R. Pugliese等人理论计算机科学电子笔记241（2009）135143选择只能由接收活动来保护（如异步π演算[1]）。注意事项和对象的最大值，例如： x是一个复杂的运算，用于定义变量的元组，即x1，. ，xn<$（其中n≥0）。我们假设同一元组中的变量是两两不同的。所有符号都应扩展到元组的组件方式. 我们采用以下关于操作符优先级的约定：一元操作符比并行组合更紧密地绑定，并且比选择更紧密地前缀化。接下来，我们将使用n在不包含变量的通信端点上进行测距（例如p·o），使用u在可能包含变量的通信端点上进行测距（例如u·uJ）。我们将省略尾随出现的f0，w i t in g e。G.p·o？我能偷到吗？w'. 0，且w [e1， . . ，en]sinpl aceof[e1]... [en] s.我们将写Is来给术语s指定一个名称i。唯一的绑定构造是定界：[e]s绑定作用域s中的元素e（即杀手标签，名称或变量）。事实上，为了使每个服务实例中的并发线程能够共享（部分）状态，COWS中的接收活动既不绑定名称也不绑定变量，这与大多数进程演算不同。相反，由通信产生的替换的应用范围由定界算子调节，该定界算子还允许产生新的名称（作为π演算的限制算子）并限定杀死活动的作用域。 因此，如果一个元素不在它的定界范围内，它的出现就是自由的。我们用fk（t）表示在项t中自由出现的killer标号的集合，用fe（t）表示在t中自由元素的集合。 两个项是阿尔法等价的，如果一个可以通过一致地重命名绑定元素从另一个获得。像往常一样，我们识别直到alpha等价的项COWS的操作语义仅定义为封闭服务，即没有自由变量/标签的服务，但当然规则也涉及非封闭服务（参见例如规则的前提（delcom）和（delkill1））。形式上，给出的语义方面的结构一致性和标记的过渡关系。结构一致性定义了直观地表示相同服务的语法上不同的服务。它被定义为由一组给定的方程定律导出的最小同余关系。我们在表2中明确显示了复制、保护和定界的定律，而省略了其他运算符的（标准）定律，即并行复合是可交换的、结合的，并且有0作为单位元素，而保护选择享有相同的性质，此外，是幂等的。 所有提出的法律都是直截了当的。特别地，连续定界的交换性意味着在[e1，. ，e n nn n]s是不相关的，因此在后续中，我们可以使用更简单的符号[e1，. ，en]s. 值得注意的是，最后一个定律可以用来扩展名称的作用域（类似于π演算中的一个类似定律），从而实现了受限名称的通信，除非定界的参数e是s2的自由killer标签（这避免了在s2内的kill活动的结果中涉及s1，并且对于静态地确定哪些活动可以被kill终止是必不可少的）。为了定义带标签的转移关系，我们需要一些辅助函数。144R. Pugliese等人理论计算机科学电子笔记241（2009）135∗0 ≡ 0伊什 ≡ S|伊什{|0|}≡0{|{1}|S|个文件夹|}≡ {|S|}{|[e]s|} ≡ [e]{|S|}[e] 0≡0[e1][e2]ss1[e2]s1|[e]s2[e]（第1条|（第2条）i f e∈/fe（s1）<$fk（s2）表2COWS结构一致性（定律摘录）M（x，v）= {x<$→v} M（v，v）= M（，）=M（w1，v1）=σ1M（w<$2，v<$2）=σ2M（（w1，w<$2），（v1，v<$2））=σ1±σ2表3匹配规则首先，我们利用一个函数[ ]来计算封闭表达式（即没有变量的表达式）：它接受一个封闭表达式并返回一个值。然而，[]]不能显式定义，因为表达式的确切语法是故意不指定的。然后，通过表3中的规则，我们定义了部分函数M（，），它允许对半结构化数据执行模式匹配，从而确定同一端点上的接收和调用是否可以同步。 规则指出，如果两个元组具有相同数量的字段并且对应的字段具有匹配的值/变量，则它们匹配。变量与任何值匹配，并且两个值是随机的。 当u_l_s_w_d_o_m_a_t_h时，M（w_，v_）返回一个用于新的v_a_b_s_i_w_a_b_i_ 子集s（用σ表示）是将变量映射到值的函数，并被写为形式为x → v的对的集合。将σ代入s，记作s·σ，其结果是，对于每个x<$→ v ∈ σ，用v替换x在s中的每个自由出现，通过可能使用阿尔法转换来避免v被s中的名称划界捕获。我们使用|σ|表示σ和σ1中的对数σ2表示σ1和σ2具有不相交整环时的并。我们还定义了一个名为halt（）的函数，它接受服务s作为参数，并返回通过只保留s中受保护的活动而获得的服务。halt（）是根据服务的语法归纳定义的。最重要的例子是halt（{|S|}）={|S|}中。在其他情况下，halt（）返回0，除了并行复合，定界和复制运算符，它作为同态。halt（k））=halt（u！）=halt（g）=0halt（{|S|}）={|S|}暂停（第1秒|s2）= halt（s1）|halt（s2）halt（[e] s）=[e]halt（s）halt（s）= halt（s）最后，在表4中，我们归纳地定义了两个谓词：noKill（s，e）成立，如果e不是killer标签，或者e = k，并且s不能立即执行一个自由的killer活动，则noKill（s，e）成立; noConf（s，n，v′，l），如果s不产生通信冲突，则h o d s不产生通信冲突，即 S不能立即执行接收活动，因为在这种情况下，S将生成一个子节点，其对数少于l。R. Pugliese等人理论计算机科学电子笔记241（2009）135145−−−→KKα†α†−−−−−JJ1 2−−12noKill（s，e）= trueif fk（e）= numnoKill（s）|sJ，k）= noKill（s，k）noKill（sJ，k）noKill（kill（k），k）= falsenoKill（[e]s，k）= noKill（s，k）ife/= knoKill（kill（kJ），k）= true ifk kJ noKill（[k]s，k）= truenoKil l（u！k）=noKil l（g，k）=truenoKil l（{|S|}，k）=n0Kil 1（s，k）noConf（k），n，v<$，l）=noConf（u！f（0，n，v<$，l） =trueJnoConf（nJ？w'. s，n，v<$，l） =falseifnJ=n |L|→sJ·{x<$→v}（delcom）†（删除1）[k]s−−→[k]sk（删除2）[e]s−−→[e]ss−−→sJs−→sJe∈/e（α）α/=k，†无Kil l（s，e）[e]s−−→[e]sJ（delkill3）[e]s−−→[e]sJ（del）αss s s ssssJnσv<$S1 1−−−→221−→s1noConf（s2，n，v<$，l）（聪）αnσv<$J（parcom）s−→sJs1|s2−→s1|S2sαJnQw<$JnQv<$J−→ss1−→s1s2−→s2M（w<$，v<$）=σnoConf（s1|s2，n，v′，|σ|）（保护）αJnσ|σ|vjJ（通讯录）{|S|} −→{|S|}S1|s2−−→s1|S2skJαJ1−−→s1s1−→s1αk，nσ lv<$kJ（parkill）S1|s2−−→s1|h alt（s2）（面值）S|s−α→sJ|S表50JJ146R. Pugliese等人理论计算机科学电子笔记241（2009）135COWS操作语义学标号转移关系α−−→是诱导服务上的最小关系通过表5中的规则，其中标签α由以下语法生成：α：：=nv<$|nDw¯|nσ lv¯|†|†R. Pugliese等人理论计算机科学电子笔记241（2009）135147接下来，我们用e（α）来表示cc urr i n g in α的名称、变量和killer标签的集合，exceptforα=nσ lv<$forhichw e lete（nσ lv<$）=e（σ），h eee（{x <$→ v}）={x} fe（v）且e（σ1σ2）= e（σ1）e（σ2）。实验室的方法如下：nvndnddentenvoke的不执行执行并在n，r，nσ lv′（ifσ）上执行接收活动）表示对于具有h_i_h_i_h_i_v_n、具有l个对的一般替换子节点和仍要应用的替换σ的通信的执行，k表示对于具有h_i_i_h_i_i_n [ k ]的从一个节点进行强制终止的请求的执行，以及分别对应于发生强制终止和通信（没有待处理的替换）的计算步骤。因此，来自封闭服务s0的计算是以下形式的连接转换序列：sα1α2α30−→s1−→s2−−→s3.wheere，foreachi，αiiseitherornlv（fororomen，landv）;serevicessi，forreachi，将被称为s0的约化。我们对要点发表评论。Activity kill（k）强制终止封闭[ k ]中所有未受保护的并行Activity（rules（kill）和（parkill）），通过将转换标签k转换为†（rule（delkill1））来停止killing效应。这种定界的存在是通过假设语义仅为封闭服务定义来保证的。 关键代码可以通过将其放入一种保护||这样，{|S|}的行为类似于s（rule（prot））。类似地，[e] s的行为类似于s（规则（del）），除了当转换标签α包含e时，在这种情况下，α必须对应于为e赋值的通信（规则（delcom））或e的kill活动（规则（delkill1）），或者当e的自由kill活动在s中处于活动状态时，在这种情况下，只能执行与kill活动相对应的操作（规则（delkill2）和（delkill3），当规则（del）的第三个前提不成立时也适用，即α=k或α=†）。这意味着，kill活动相对于包含在相应kill标签的定界内的活动被急切地执行。只有当参数中的表达式可以被计算时，服务调用才可以继续（rule（inv））。一个receive活动将一个可调用的操作按照一个给定的合作伙伴名称（rule（rec））进行调用，并且receive的执行允许在备选行为之间做出决定（rule （ choice ））。当两个并行服务执行匹配的接收和调用活动（规则（com））时，可以进行通信。通信生成一个替换，记录在transition标签中（用于后续应用），而不是像大多数进程演算中那样的静默transition。 如果可 能 有 多 个 匹 配 ， 则 选 择 需 要 较 少 替 换 的 接 收 进 行 （ 规 则 （ com ） 和（parcom））。这种机制允许关联不同的服务通信，从而隐式地创建交互会话，并且可以被利用来对服务实例与相应的服务规范之间的优先级进行建模，当两者都可以处理相同的请求时。当遇到接收的变量x参数的定界时，即x的整个范围被确定，定界被移除并且x的替换被应用于项（规则（delcom））;变量x从项中消失，148R. Pugliese等人理论计算机科学电子笔记241（2009）135条件：Φ，ΦJ，. . .导出的私有名称：Δ、ΔJ、. . .未知值：x，y，.变量/名称/未知值：u，uJ，. . . Value s/Unknown v alue s：v，vJ，. . .Variable/Values/Unknownvalu e s：w，wJ，. . .N ames/Unknown own values：n，mJ，. ..... . 你 好 。 ，p，o，. . .结束点/现在已知n值：n，mJ，. . . ，u，uJ，. . .约束服务：Φ，ΔΔs服务：s：：=杀死（k）|u·uJ！є|G|S|S|{|S|}|[e] s|伊什接收保护选择：g：：= 0|p·o？W.S|G+G表6受限制的服务不能被重新赋值（因为这个原因我们说COWS值得注意的是，在转换的推断期间，要应用的替换的长度减小，而初始替换的长度l从不改变，这使得在任何时刻都适合于检查更好匹配的存在，即具有更大优先级的并行接收的存在。规则（cong）是标准的，它规定结构一致的服务具有相同的转换。并行服务的执行是交错的（规则（par）），但是当执行kill活动或通信时。实际上，前者必须触发所有并行服务的终止（根据规则（parkill）），而 后 者 必 须 确 保 具 有 更 高 优 先 级 的 接 收 活 动 进 行 （ 规 则 （ com ） 和（parcom））。4COWS的符号语义在本节中，我们将介绍COWS的符号操作语义。为了简单起见，这里我们考虑COWS的一元版本，即。交流活动的形式是U！和n？w.s（我们将在第5节讨论如何定制符号语义来处理多元通信）。许多说明性的例子阐明了技术的发展。4.1符号操作语义学COWS的符号操作语义定义为：配置形式为Φ，Δs，称为受约束服务，定义见表6，其中Φ是达到当前状态必须满足的条件，Δ是之前导出的私有名称集，s是其操作由Φ和Δ确定的服务。 当集合Δ为空时将被省略，例如， Φ ► s而不是Φ，我们定义了一组丰富的服务的语义，其中还包括那些辅助术语，这些辅助术语是由第3节中介绍的语法产生的术语中的未知值替换（自由出现）变量而产生的，现在表达式也包含未知值。在扩展语法中，我们使用x表示未知值，t表示未知值或项t（其中t可以是n，v，u，w，n或u）。因此，u·uJ！p·o？w.s分别表示调用和接收活动在标准语义中，唯一的绑定构造是定界：letR. Pugliese等人理论计算机科学电子笔记241（2009）135149Φ， Δ<$C [[d]s]是一个受约束的服务（其中C是上下文1），[d]在作用域s中、在条件Φ中和在集合Δ中绑定d。我们用bn（t）表示在一个项t中有界出现的名字的集合，用uvar（t）表示被t中相应的未知值替换的变量的集合（即如果x是t中的未知值，则x∈uvar（t））。为了简单起见，我们假设约束服务中的绑定变量与约束服务的未知值对应的变量是成对不同的，并且绑定名称与自由名称都是不同的（当然，这些条件不是限制性的，并且总是可以通过使用alpha转换来满足）。这个假设避免了不同的未知值在受约束服务的条件Φ中由相同的xCOWS的符号操作语义仅针对封闭服务定义，并以结构同余和（双）标记转换关系的形式给出。结构一致性是第3节中定义的结构一致性对这里使用的丰富的服务语法的简单扩展。为了定义带标签的转换关系，我们利用了对第3节中定义的函数halt（）和谓词noKill（，）的丰富语法的平凡扩展。 我们还扩展了function[]来处理未知值。现在，它接受一个封闭表达式并返回一个对（Φ，v）：（可能未知的）值v是条件Φ成立的求值结果。具体地说，让是一个表达式，如果不包含未知值并且可以计算，那么[]]=（true，v）其中v是求值的结果，就像在原始COWS语义中一样。类似地，如果x是一个未知值x，则[x]=（true，x）。如果包含未知值且不是单个未知值，值（即，ϵx对于每个x），则[]]=（（ybnΦJ），y）其中y是一个新的未知值，必须与所有私有名称不同（即y=/bn）和fromallexis ten tt nknwvalues（i. e. y/∈u v）2，并且dΦJ是允许处理部分定义的表达式运算符的系数。函数[]]以及条件Φ J不能被显式定义，因为表达式的确切语法故意不指定。然后，考虑以下简单的表达式语言作为示例ϵ ：：= X | X |我|+|ϵ−ϵ|ϵ ∗ ϵ|中文（简体）|其中i是整数值。 对于上面的语言函数[]]是这样的：• [[(5（1）[1]=（1）;• [5−x]是unfined，因为表达式5−x不是封闭的;1上下文C是一个带有“hole”的服务，2值得注意的是，这里y可以是任何未知值，只要它满足条件y/= bn和y/∈ uv。通知条件y/∈ uv是变量名y的语法条件。稍后，我们将解释上述条件的确切含义，并说明在推断过渡的最后一步中如何评估它们。3当然，如果在所考虑的表达式中使用的所有运算符都是全函数，则条件ΦJ为真。150R. Pugliese等人理论计算机科学电子笔记241（2009）135• [[5−x]]=（（y bn<$y/∈uv <$y= 5−x），y）;• [[5[0]未定义;• [[5/x]] =（（y/= bn y/∈uvy= 5/xx= 0），y），其中条件x= 0是因为当运算符/的第二个参数为0时，它没有被定义。我们还定义了一个函数confRec（，），它将服务s和端点n作为参数，并返回一组（可能是未知的）值，这些值是s中活动的端点n上的接收活动的参数。该函数扮演标准语义的谓词noConf（，）的角色，并且实际上，被利用来在通信冲突的情况下禁用转换（通过将转换条件设置为false）。该函数归纳定义如下：confRec（0，n）=confRec（kill（k），n）=confRec（u！n）=confRec（n？x.s，n）=0confRec（g + gJ，n）= confRec（g，n）v.s，n）={v}confRec（nJ？如果n nJconfRec（{|S|}，n）=confRec（s，n）confRec（s |sJ，n）= confRec（s，n）<$confRec（sJ，n）confRec（[e] s，n）=<$if e∈ nconfRec（[e]s，n）=confRec（s，n）\{e}ife∈/nconfRec（s，n）=confRec（s，n）Φ，α在n>−→的情况下，与服务器相关的基本位置关系为：Φ，α在标记的转移关系− →上，这是服务上的最小关系由表7中的规则诱导。条件Φ和动作α由以下