Erlang程序的形式验证方法研究

理论计算机科学电子笔记118（2005）145-162www.elsevier.com/locate/entcsErlang程序托马斯·诺尔1LehrstuhlfurInformatikII亚琛大学52056德国摘要本文提供了一个贡献的并发函数编程语言Erlang，这是专为电信应用程序编写的程序的形式验证。 它在重写逻辑中给出了这种语言的形式化描述，重写逻辑是一个统一的并发语义框架，它在语义上建立在条件项重写模方程理论之上。特别是它演示了使用方程定义抽象映射，减少系统的状态空间保留字：软件验证、并发函数编程、重写逻辑1介绍在本文中，我们在函数式编程语言Erlang[2]的背景下解决软件验证问题，Erlang[2]是由Ericsson公司开发的我们对这种语言的兴趣是双重的。一方面，它经常被成功地用于电信系统的设计和实现另一方面，它相对紧凑的语法和干净的语义支持形式化推理方法的应用。1电子邮件地址：noll@cs.rwth-aachen.de1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.037146T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145由于存在无界数据结构和动态进程生成，Erlang程序通常会导致无限状态系统。 因此，使用交互式定理证明助手（如EVT Erlang验证工具[5，6]）来建立所需的系统属性是很自然的在这里，我们遵循另一种方法，我们试图采用全在这里，我们集中讨论验证过程的第一部分，即要检验的（跃迁系统）模型的构造更具体地说，我们使用重写逻辑框架来正式描述Erlang，该框架是在[11]中提出的，作为并发的统一语义框架。它已被证明是许多具体规范和编程语言的适当建模形式主义[10]。在这种方法中，一个系统的状态是由一个等价类的模一组给定的方程的条款，和转换对应于重写操作的代表resenerator。因此，重写逻辑支持编程形式主义的定义，并通过采用（等式）项重写方法来执行或模拟具体系统。我们将看到，这些方程可以用来定义抽象映射，这些抽象映射减少了系统的状态空间特别地，我们将讨论一些例子，在这些例子中，有可能将一个具有无限多个状态的系统缩小到一个有限的状态。通过使用重写逻辑框架的可执行实现，例如ELAN工具[4]，可以自动导出给定Erlang程序的转换系统。此后，后者，但是，这超出了本文的范围。本文的其余部分组织如下。第2节通过概述其语法结构及其直观含义来介绍第3节介绍重写逻辑框架，并使用它来定义Erlang的转换系统语义。然后第4节演示了使用方程来减小过渡系统的大小，最后第5节以一些评论结束。2Erlang编程语言Erlang/OTP是一个编程平台，为开放分布式（电信）系统编程提供必要的功能：支持并发的Erlang语言，以及提供现成组件（库）和服务的OTP（开放电信平台）中间件，T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145147--|例如分布式数据库管理器、对“热代码替换”的支持下面我们考虑Erlang编程语言的一个核心片段，它支持在诸如原子常数（atoms）、整数、列表、元组和进程标识符（pid）等数据类型上运行的进程的动态网络的实现，通过称为邮箱的无界有序消息队列使用异步、真正的Erlang有几个额外的功能，如模块，进程分布（到节点上），支持健壮的编程和与非Erlang代码的互操作C或Java。除了Erlang表达式e之外，我们还使用匹配子句cs、模式p和值v的语法类别进行操作。Erlang表达式的抽象语法总结如下：e：：= e1，e2|e（e1，. ，e n）|CS结束的情况E |P = e |e1！e2|op（e 1，.|op (e1,...，e n）|spawn（e1，e2）self（）|Xcs：：= p1->e1;. ;pn->enp：：= op（p1，.，p n）| Xv：：= op（v1，.，v n）这里X的范围是Erlang变量，op的范围是一组原始常量和操作，包括元组e1，e2，列表前缀[e1e2]，空list [ ]、整数、pid常量和原子。Erlang的函数式子语言是相当标准的：原子、整数、列表和元组是值构造器; e1，e2表示顺序组合; e（e1，.，e n）表示函数调用。形式caseeofp1->e1;... ;pn->enend涉及匹配：e计算得到的值顺序地与模式pi匹配。如果成功，求值继续ei，其中由pi绑定的变量相应地被实例化。对于赋值p=e也是如此，如果e的值与p不匹配，则会引发运行时错误，否则此值将作为结果返回。涉及非功能行为的结构（即，（1）E1！e2表示输出步骤，异步地将e2的值发送到由e1标识的进程，而接收csend检查本地进程的邮箱q，并检索（并移除）q中与cs中的任何模式匹配的第一个元素。一旦找到这样的元素v，评估类似于cs结束的情况v进行。spawn（e1，e2）动态创建一个新进程，其中e1给出的函数被应用于列表e2给出的参数，self（）返回本地进程的pid148T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145作为一个介绍性的例子，我们考虑一个简短的Erlang程序，它实现了一个简单的资源锁，即，仲裁器，其在接收到来自客户端进程（在这种情况下为两个）的对应请求时，准许对单个资源的访问。在[3]中给出了该算法的扩展版本，它还能够处理来自给定有限集合的多个资源。Erlang程序由一组模块组成。每个模块基本上都包含一个函数声明列表。在我们的例子中，系统被定义在一个模块中。 它是使用start函数初始化的，根据导出声明，start函数是从locker模块外部可访问的唯一函数。通过调用相应的启动函数，它生成了三个新进程：一个locker和两个client。实际的进程创建由spawn内置函数执行，该函数接收模块标识符和在新进程中调用的函数名称及其参数。locker进程在非终止循环中运行locker函数。它使用receive构造来检查请求消息是否已经到达。后者应该是由请求标记和客户端进程标识符（由变量Client匹配）组成的一对。然后，通过发送一个ok消息，客户端被授予访问资源的权限。最后，在接收到来自相应客户端的释放消息之后，锁柜返回到其初始状态。客户端进程展示了互补行为。通过发出请求，它要求访问资源.在这里，self内置函数返回客户端进程的进程标识符（pid），然后由locker进程用作客户端的句柄。在接收到ok消息后，它访问资源，然后释放它。T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145149- 模块（储物柜）。-export（[start/0]）。启动（）->start_locker（），start_client（），start_client（）.start_locker（）->spawn（locker，[]）。locker（）->receive{request，Client} ->客户端！好了，接收{release，Client} ->locker（）start_client（client）->spawn（client，[client]）。客户端（Client）->客户端！{request，self（）}，receive确定->%临界区！{release，self（）}，client（）端结束结束。这种系统的理想正确性属性是简单的：无死锁：不存在等待彼此继续的循环进程链，即，储物柜应该总是能够接收新的请求或释放，互斥：没有两个客户端可以同时访问资源，无饥饿：所有能够进入临界区的客户端最终都应被授予其所要求的访问。稍后我们将看到如何通过构造上述程序的transi- tion系统来检查这些属性。使用后者，可以通过显示系统总是可以继续来验证死锁的存在，即，每个州都有一个直接继承人互斥可以通过证明在锁定器接收两个连续的请求消息之间必须总是发生释放操作来建立。然而，保证无饥饿属性需要关于进程调度器的行为的额外假设。原则上，可能会发生一个客户端进程无限地保持在其初始状态，150T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145⊆×也就是说，从来没有被安排向储物柜发送请求消息。然而，这种情况被排除在所有Erlang实现必须满足的要求之外（参见。[2，Sct. 5.6]）。首先，调度算法必须是公平的，即，任何被允许执行的进程最终都将被运行。此外，不允许任何进程长时间阻塞机器这是因为Erlang应该适合于响应时间必须在毫秒级的软一旦客户端将请求发送到locker，就可以保证最终访问资源，因为Erlang运行时系统中（locker）邮箱的实现遵循FIFO策略。3Erlang的形式语义任何严格验证的起点都是形式语义学。在这里，我们通过将转换系统与Erlang程序相关联来使用操作语义，从而精确地描述其可能的计算。3.1重写逻辑框架重写逻辑框架由J. Meseguer在[11]中提出。[10]中介绍了这种方法以及大量参考书目重写逻辑旨在作为一个统一的数学模型，并使用重写系统中的概念而不是等式理论。它的目的是在一个单独的描述的静态和动态方面的并发系统。更确切地说，它区分了描述系统状态结构的定律和规定系统可能的跃迁的规则。这两个方面分别形式化为一组方程和作为（条件）项重写系统。这两种结构都对状态进行操作，表示为（等价类的）n-项由于一个单一的转换可能包括几个独立的重写步骤，并发行为可以明确地以这种方式建模。更具体地说，在Meseguer• 签名是签名，即，功能符号的分级字母表• ET（Var）T（Var）是一个有限的方程组，它在一个变量来自给定集合Var的一个项的集合T（Var• L是一组有限的符号，称为（规则）标签，T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145151−→• R<$L ×（T<$（Var）× T<$（Var））+是（条件）转移规则的有限集合，其中每个（ρ，（l −→ r）（c1−→ d1）. （c k−→ d k））∈ R表示为c1−→d1.. . c k−→d k（ρ）L r这里l和r分别被称为规则的上面的部分叫做它的条件，有时可以缩写成字母C。如果k=0，则该规则称为无条件规则。关 于 重 写 逻 辑 的 语 义 ， Meseguer 定 义 重 写 理 论 T 需 要 一 个 E−[s]E−→[t]E，并写T[s]E−→[t]E如果这个概率可以通过有限次地应用特定的演绎规则来获得，这些规则指定了如何应用上述过渡规则。用这种方法，就有可能推理出状态由项表示并通过变迁演化的并发系统。在这里，状态是根据签名构造的，并且转换规则指定该结构中的局部转换，而演绎规则允许在给定局部转换的情况下推理并发系统的整体行为。等式用于识别仅在其语法表示中不同的术语。稍后我们将看到，它们也可以用来定义状态空间上的抽象映射。然而，事实上，（条件）项重写模方程理论通常太复杂，甚至是不可判定的。因此，在E中不可能存在任意的方程。遵循P.Viry在[14]中的思想，我们因此建议将E分解为一组有向方程（即项重写系统）ER和一组AC，该组AC表示某些二元算子的结合性和交换性。给定ER终止模AC，通过R模E的重写可以通过通过ER的归一化和通过R的重写的组合来实现，两者都模AC。这里，由R引起的步骤表示系统的实际状态转换，而由ER定义的约简必须被视为内部的、不可观测的计算。3.2Erlang的重写逻辑规范如前所述，Erlang运行时系统维护一组用户过程。任何这样的进程都由三个部分组成：一个必须被计算的Erlang表达式，一个进程标识符（pid），它唯一地标识152T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145ǁ⟨ ⟩相应的进程，由系统内部确定;以及一个用于传入消息的邮箱，本质上是Erlang值的列表此外，我们将把一个转换标签和一个当前的评估环境归因于一个过程。前者用于指示导致当前状态的转换的类型。后者存储Erlang变量和赋给它们的值之间的绑定。它通过赋值或模式匹配操作进行修改。对代码施加的语法限制保证变量名的每次出现都位于绑定操作的范围内。如前所述，在一个系统中可以有多个进程并发运行。因此，我们引入了进程系统的概念，它只是一组并发进程，并构成了transition-system语义中的状态S={\displaystyle\alpha}|e|我|Q|ρ⟩|α标记，E表达，I PID，Q邮箱，ρ环境}∪ {⟨i⟩|I pid}{s1|s1，s2∈S}构造i表示实际计算已经终止的死进程。相反，第一种形式的过程被称为生活。 利用结合和交换并行复合算子将活进程和死进程结合起来，得到一个并发进程系统。然而，这只有在每个进程都由其pid唯一标识时才有意义。 因此，如果进程元组中出现的所有pid都是不同的，我们称之为良构的进程系统，并假设从现在开始每个进程系统都是良构的。单个过程和过程系统的状态都随着时间的推移而演变（例如，进程的表达式由于评估而改变，或者邮箱存储传入消息）。附加到进程的转换标签反映了导致当前状态的转换类型。这些包括标签τ，它表示采取了不涉及边效应的步骤，例如对+这样的内置函数的求值。其他转换标签，如msg（j，42）描述了将值42发送到由j标识的进程，而spn（foo，[1，2]，j）表示调用涉及侧对象的函数（本例中为spawn函数）。在这里，重要的是要注意转换标签不仅仅是对流程的注释。相反，它们实现了两个层次的语义，单进程和并发系统之间的通信手段，从而确定了并发进程系统作为一个整体可以采取为了简化介绍，我们避免将这些方面正式化，T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145153ǁ1212Erlang中的模块系统。因此，我们总是假设函数的主体可以通过它的模块标识符和它的名字来确定。3.3等式理论下一步是定义重写理论的方程组E。在AC部分我们只需要声明并行运算符到是结合的和交换的。有向方程组，ER，是用来模拟一些辅助功能，采用的过渡规则。由于空间有限，我们不显示规格，而是参考[1]。让我们只提一下，我们得到了一个项重写系统，它是收敛模AC。3.4转变规则我们定义中最重要的部分是通过条件转移规则对Erlang进程系统的操作行为进行形式化。为了获得更清晰的结构，我们将R分解为两个不相交的子集：R = RPrcRSys.在这里，RPrc包含所谓的在下文中，我们将从这两个类别中给出一些例子，再次参考[1]以获得完整的定义。和以前一样，我们将使用某些标准的表示法来表示规则中出现的重写逻辑变量，可能是索引或启动形式。我们让e表示Erlang表达式，p表示模式，X表示Erlang变量，a表示原子，v表示值，f表示函数名，c表示条款。此外，α表示一个转换标签，cs表示一个子句列表，i、j、k表示pids，q表示邮箱，ρ表示环境，s表示并发进程系统。3.4.1Expression–Level第一条规则描述了列表的递归求值。由于Erlang的最左⟨ τ|e1|我|Q|ρ ⟩ −→ ⟨ α|eJ1|我|QJ|pj⟨τ|[e|e]|我|Q|ρ⟩−→⟨α|[eJ|e]|我|QJ|pj（清单1）一般来说，我们假设在我们的形式化中，其他-154T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）1452或者，该标签指示应当由另一个适当的（系统级）规则处理的副作用一旦列表构造函数的第一个子表达式是不可约的（即，值），则求值继续执行第二子表达式：⟨τ |e|我|Q |ρ⟩ −→ ⟨α |eJ|我|QJ|pj⟨τ |[v|e]|我|Q |ρ⟩ −→ ⟨α |[v|eJ]|我|QJ|pj(list（二）以下规则处理模式匹配操作。在这里，我们只是形式化的情况下建设。⟨τ |e|我|Q |ρ⟩ −→ ⟨α |eJ|我|QJ|pj⟨ τ| CS结束的情况E|我|Q|ρ ⟩−→⟨ α |cs结束的情况eJ|我|BJ|ρ ⟩匹配c（v，cs，ρ）=（e，ρJ）（案例1）（案件）⟨τ| CS结束的情况V|我|Q|ρ ⟩ −→ ⟨τ|e|我|Q|pj最后，我们考虑一个Erlang内置函数，它在语义的系统级上引起副作用。j=newPid（）⟨τ|spawn（a，v）|我|Q |ρπ −→ π spn（a，v，j）|J|我|Q |ρ⟩（产卵）这里的newPid（）是一个函数，它返回一个新鲜的pid，这个pid唯一地标识了新进程，并且作为spawn调用的结果返回。下面的规则处理Erlang的核心概念之一：异步发送消息。正如我们将看到的，消息将被附加到目标进程的邮箱中。请注意，进程也可以向自身发送消息。（发送）⟨τ|你好！v|我|Q|ρ−→ ρmsg（j，v）|v|我|Q|ρ⟩3.4.2System–Level第一条规则只是表示，如果并发系统中的单个进程执行计算步骤，那么整个系统也执行计算⟨ τ |e|我|Q |ρ ⟩ −→ ⟨ τ |eJ|我|QJ|pj⟨τ|e|我|Q|ρs−→τ|eJ|我|QJ|pjs（沉默）流程生成的形式化如下。spawn内置函数带有两个参数：一个函数原子和一个参数列表。新进程将使用这些参数调用此函数，从空邮箱和空环境开始。⟨τ|e|我|Q|ρπ −→π spn（a，v，j）|eJ|我|QJ|pj⟨ τ|e|我|Q|帕里什−→⟨ τ |eJ|我|QJ|ρJτ |a㈤ |J|无|nil（Spawn）T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145155接下来，我们指定如何将消息存储在接收进程的邮箱中。⟨τ|e1|我|年q1|ρ1−→μmsg（j，v）|eJ1|我|q1J|ρJ1⟨ τ|e1|我|年q1|ρ1 ⟩ ǁ ⟨ τ|e2|J|Q2|ρ2ε s−→⟨τ|eJ1|我|q1J|ρJ1ππτ|e2|J|q2·v|ρ2εs（Com）下一个规则处理进程正常终止的情况，即，将其表达式求值为一个值，然后变为死值。（终止）⟨τ|v|我|Q|ρs−→i s需要更多的规则来完成我们的Erlang重写理论T的定义。与初始表达式e0（以及具有函数定义的模块集合）一起，它定义了一个标记转移系统如下。T=（S，s0，−→）其中S是由S ={s}定义的状态集合|s0−→ <$s}，s0是由s0=<$τ给出的初始状态|e0级|我0|无|对于某个初始pid i0，请注意，状态空间S通常是无限的，这是由于以下几个原因：• Erlang支持无限的数据结构，例如整数或列表。• 递归函数调用的无限制使用可以产生任意大的表达式。• 进程的邮箱可以存储无限数量的消息。• 此外，动态进程创建与递归函数的结合产生了无限状态空间。然而，使用我们的语义的实现，这将在下文中列出，可以证明第2节中的储物柜示例的状态空间是有限的。它包括大约180个州。不同数量的客户端进程的实验表明（预期）的效果，状态空间呈指数增长的客户端的数量-模型检查应用程序中的状态爆炸问题的一个典型缓解这一问题的方法将在第4节中讨论。乍一看，尽管储物柜和客户端函数都是递归定义的，但储物柜系统拥有有限的状态空间可能看起来令人惊讶。这可以通过只使用尾部递归的事实来解释，也就是说，递归函数调用只能作为相应函数体中的最后一个表达式发生因此，这样的调用对应于跳转到相应函数体的开始，因此表示计算的控制状态的表达式的大小是有界的。事实上，尾递归产生了一种称为last的实现技术。156T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145调用优化，允许在恒定的内存空间中评估这些函数（参见[13]的一般思想和[2，Sct.9.1]中的3.5在ELAN中实施为了开发Erlang的评估器原型，我们选择了重写逻辑框架的现有实现，即 ELAN 工 具 （ 参 见 [4] ） ， 这 是 在 法 国 南 希 的 LORIA 研 究 所 的PROTHEO小组内开发的ELAN系统提供了一个环境，用于以基于重写规则的语言指定和原型化演绎系统，其应用可以由策略控制。ELAN既可以作为一个逻辑框架，也可以用来描述和执行确定性和非确定性的基于规则的过程。在这里，我们通过定义Erlang语义的可执行规范来利用第二个特性。系统规格在称为元件模块的特殊ELAN模块中给出。在元素模块中，可以导入其他模块，定义重写理论的排序、运算符和重写规则。 等式推理由高效的AC此外，可以描述策略，这些策略定义了方法（即，顺序和位置），其中规则可以应用于术语。事实证明，这些特性对于实现我们的Erlang语义非常有用。细节可以在[1]中找到。如前所述，使用该实现方式，例如，计算第2节中的locker示例的转换系统，其中包含不同数量的客户端进程（这些进程都是在初始调用start函数时产生的）。这使我们能够证明系统确实表现出所需的性质（互斥等）。这一点在本章开头已经提到过。我们将在下一节回到这个问题。4方程式抽象注意到，到目前为止，ER，定向方程的集合，仅用于实现Erlang的重写逻辑规范中出现的辅助函数。这与引入方程以减少重写规则的数量和/或转移系统的状态空间的最初动机有些矛盾。在下文中，我们概述了两种针对第二个目标的方法。第一个想法是“隐藏”这些计算在一个给定的这样，我们得到T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145157一个抽象的转换系统，它只代表人们想要观察的那些状态变化。更具体地说，我们移动那些从RPrc到ER的转换，也就是说，我们让R τ=.p−→pJ|......这是什么？|... | ... | ... | .. . ⟩Σ={（list 1），（list 2），.. . }RPrcJ=RPrc\RτERJ=ER<$Rτ通过这种方式，当然，程序的某个动作是否有趣取决于应用程序。因此，对于不同的验证问题，集合Rτ的选择可以不同。在任何情况下，一个主要的要求是，抽象映射的选择确保正确性的保存属性：假阳性应该被排除，也就是说，属性检查为真的抽象系统也应该保持具体的系统建模。另一方面，术语假阴性指的是抽象系统表现出不能追溯到具体系统的错误的（不那么关键的）情况。 在这里，抽象被选择得过于粗糙，对错误情况的检查可能会建议一种方法来细化它。图1显示了具有两个客户端的储物柜示例的抽象转换系统，如第2节所述。这里start表示初始状态，由一个单独的进程组成，它评估函数调用start（）。锁定器进程由L表示，可能由客户端编号（1和/或2）上标以指示其消息邮箱的内容。例如，L12表示一个锁柜进程，它在邮箱中存储了来自第一个和第二个客户端（按此顺序）的请求客户端由C1和C2表示，其中条指示相应的客户端处于临界区。转换被标记以指示引起状态改变的动作的类型。这里spn指的是进程的创建，reqi和reli表示Ci分别向锁定器发送请求或释放消息（其中i∈{1， 2}），oki表示从锁定器进入临界区的许可。因此，抽象系统包含14个状态，而标准转换158T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145开始SPNLSPNL-1req1rel1LC1C2L1C1请求2请求1spn ok1L2C1C2版本2rel1L1C1C2LC1请求1ok2请求2ok1 spnL21C1C2rel1ok2请求1LC1C2L12C1C2版本2确定1请求2LC1C2L1C1C2L2C1C2Fig. 1. 抽象转换系统与1客户端2客户端3个客户原始LTS65个国家10分钟182个国家55分钟536个州380分钟抽象LTS5个州20秒14个州90秒42个州13 min表1原始系统与抽象系统在原始语义中导出的系统包括182个状态。表1显示了几个客户端的状态空间的大小和计算它所需的时间。结果非常有希望，邀请进一步研究Erlang程序的方程抽象的好处如前所述，使用形式语义，我们可以推导出我们的locker实现行为正确。更具体地说，图1中的（抽象的）过渡系统具有以下性质：无死锁：不存在循环的进程链互相等待SPNT. Noll/Electronic Notes in Theoretical Computer Science 118（2005）1451591−→−→1继续，这可以从这个系统中的每个国家都有一个直接继承人的事实中推断出来，互斥：没有两个客户端可以同时获得对资源的访问，因为在每个状态中在临界区中最多有一个客户端进程用横条标记），以及无饥饿：每个能够进入临界区的客户端最终都得到其所需的访问。乍一看，这个属性似乎被违反了，因为系统中存在一个（可到达的）循环，其中第二个客户端永远不会活动：SPN开始SPNLLC请求1−→ L1-C1ok1 L-1rel1 LC请求1−→ ...（可以构建一个类似的场景来表明第一个客户也可能挨饿。然而，这个循环无限期地将主进程中的start函数排除在派生第二个客户端进程之外，因此与Erlang运行时系统的每个实现所假设的要求相因此，我们确实可以保证C2将被派生，而且，C2将获得向锁定器发送请求换句话说，系统最终将达到索引2出现在锁定器进程的邮箱上标中的状态。这同样适用于第一个客户。因此，为了建立这很容易通过检查过渡系统来验证。当然，可以通过适当的工具（如TRUTH）自动检查这些属性。现在让我们转向第二种方法，它使用有向方程来定义抽象映射。下面的例子表明，这样的方程有时可以用来减少一个有限系统的无限。下面给出的代码片段实现了一个简单的并发服务器，它重复地接受以三元组形式传入的查询，三元组由原子请求标记，并且包含请求本身（由变量Request匹配）和客户端进程（Client）的pid。然后，它生成一个进程，该进程通过调用句柄函数（这里没有显示）来服务请求，并将结果作为响应原子标记的元组发送回客户端。−→−→160T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145concurrent_server（）->receive{request，Request，Client} ->spawn（serve，[Request，Client]）end，concurrent_server（）.serve（Request，Client）-> Client！{response，handle（Request）}。以这种方式处理服务器请求，即，由独立的并发子进程组成，代表了一种在Erlang应用程序中广泛使用的编程技术。除了运行服务器进程的主机的负载可以通过控制并发进程的数量来容易地平衡的事实之外，它还具有很大的优点，即服务器本身的计算和单个请求的计算被保持隔离，并且因此不能相互干扰[2，第8章]）。然而，它的后果是，在每次完成服务进程之后，系统中仍然存在一个死进程。因此，如果对并发服务器的调用总数没有限制，则系统状态的数量也没有限制使用归约规则si−→s（其中s表示系统，ia pid），有可能得到一个有限的转移系统，假设对服务器的同时调用的数量是有界的，并且单个请求的处理只涉及有限的行为。5结论在本文中，我们提出了Meseguer重写逻辑的一个变体，一个语义框架，在其中可以形式化Erlang编程语言的操作语义。特别地，我们已经看到，等式推理允许测试和比较不同的抽象，以减少状态空间的大小。从而避免了具体的运行时文件表明，在实现重写逻辑框架（在我们的例子中是ELAN）的工具的优化和所考虑的编程语言的描述方面还有很多工作要做，这通常涉及相当复杂的语义结构。当然，在这方面不应过于乐观。重写模结合性和交换性的条件方程项总是隐含着一定的复杂性，这是我们的T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145161框架.因此，期望从特定语言的重写逻辑定义自动导出的求值器将实现手写的优化实现的效率是虚幻的相反，“可执行规范”方法证明了其在可扩展性和用户友好性方面的优势。因此，ELAN和类似的系统应该被视为验证工具前端的快速原型工具。这个问题在[9]中讨论过。进一步的技术形式抽象的Erlang程序与无限状态空间有限状态的形式，其次是完全自动化的模型检查，是由F。Huch in [7].他采用抽象解释的技术来定义无界数据结构的有限域抽象。这使他能够证明，对Erlang程序的抽象解释，其中只采用尾递归，只产生有限数量的进程，并且只使用邮箱的有限部分， 一个有限的过渡系统，因此适合于经典由于一个无限状态空间不可能总是在不丢失“基本”信息的情况下被简化为一个有限状态空间 在任何情况下，都必须实现Erlang的语义，将Erlang程序映射到转换系统。 （此外，抽象函数必须为模型检查方法实现。在这里，我们的编译器引用[1] 阿米拉纳什维利Core Erlang语义的重写逻辑形式化。硕士[2] J.L.Armstrong，S. R.M.C.维尔丁 威廉姆斯和华盛顿。 我知道了。在Erlang中并 发Programming。Prentice Hall International，第2版，1996年。[3] T. 艺 术 ， C.B. 厄 尔 和 J. 德 里 克 。 Erlang code ： a resource locker case study.在 FormalMethodsSpringer–Verlag,[4] ELAN主页。http://www.loria.fr/ELAN/网站。[5] L. Fred lund，D. 古罗夫和T。 没有。 S em i- a t o m a t e d v e r l ang c o d e的简化。第16届IEEE自动化软件工程国际会议（ASEIEEE Computer Society Press，2001.[6] L. -是的 Fred lund，D. 你好，T。 不，M。 D AM，T。 艺术，和G。 Cu gun ov. 一个用于Erlang的值。International Journal on Software Tools for Technology Transfer，4（4）：405162T. Noll/Electronic Notes in Theoretical Computer Science 118（2005）145[7] F.哈。 使用抽象解释和模型检查验证Erlang程序。ACM SIGPLAN Notices，34（9）：261[8] M. Lange，M. Leucker，T. Noll和S.托比Truth -并发系统的验证平台。系统规范、开发和验证的工具支持，计算科学进展，第150[9] M. Leucker和T.没有规范语言实现的快速原型。在第10届IEEE快速系统原型国际研讨会（RSP'99）的会议记录中IEEE Computer Society Press，1999.[10] N. 我的天啊-我的天啊。Meseguer. 重写逻辑：重写和重写。 计算机科学，285（2）：121[11] J. Meseguer。条件重写逻辑是并发的统一模型。Theoretical Computer Science，96（1）：73[12] T. 诺伊尔湖-是的 Fr ed lund，andD. Gurov.Er la ng Ver i f i c ationTool。在ProseceeDing的第7届关于系统构造和分析的工具和算法的国际会议'01），计算机科学讲义的第2031卷，第582-585页中Springer–Verlag,[13] G.L.斯蒂尔揭穿“昂贵的过程调用”的神话，或者过程调用实现可以被认为是有害的，或者LAMBDA，最终的GOTO。ACM会议记录，第153-162页，1977年[14] P. Viry。重写：一个有效的并发模型。在PARLE'94会议录Springer–Verlag,