McErlang模型检查器的验证过程及其在LambdaStream公司的实现

理论计算机科学电子笔记271（2011）23-40www.elsevier.com/locate/entcs基于McErlang6的Java管理器组件实例研究大卫·卡斯特罗1 维克托·M 古利亚斯2西班牙阿科鲁尼亚大学计算机科学系ClaraBenacEarle3Lars-ClaraKeFredlund4巴贝尔集团，计算机科学学院，马德里政治大学（UPM），西班牙塞缪尔·里瓦斯5LambdaStream Servicios Interactivos S.L.RondadeOutei r o33Entlo.，ACorunCorona，西班牙摘要在本文中，我们提出了一个正在进行的工作，正式验证的过程中使用的McErlang模型检查器。进程管理器是Erlang/OTP标准管理器行为的替代实现。目前在LambdaStream公司使用的这个实现，针对几个安全性和活跃性属性进行了检查关键词：McErlang，模型检查，验证，监督程序，Erlang1电子邮件：dcastrop@udc.es2电子邮件：gulias@udc.es3电子邮件：cbenac@fi.upm.esc4电子邮件地址：lfredlund@fi.upm.es5电子邮件：samuel. lambdastream.com6这项工作得到了以下项目的部分支持：ProTest（FP 7-ICT- 2007-1 215868）、DESAFIOS10（TIN 2009 -14599-C 03 -00）、PROMETIDOS（P2009/TIC- 1465）、AMBITIIONS（MICIN TIN 2010-20959）和XUGA（PGIDIT 07 TIC 005105 PR）。1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.02.00924D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）231引言编写正确的并发软件是一项艰巨的任务，因为这种系统具有固有的不确定性行为。并发声明语言似乎是一个有趣的和实用的选择，实现并发软件，由于没有副作用（或至少减少他们的数量）。例如，并发函数语言Erlang [5]被世界上的几家公司用来实现复杂的并发控制系统。一种经常用于检查并发程序是否满足一组所需属性的技术是模型检查[9]。在模型检查中，理论上例如，McErlang [7]，一个用Erlang编写的程序的模型检查器，直接使用实际的Erlang源代码作为要分析的模型。McErlang已成功应用于许多案例研究，例如使用Erlang的公司的一个例子是LambdaStream S.L.，该公司对提高软 件 质 量 感 兴趣 ， 正 如 他 们参 与 欧 洲 基 于 属 性 测 试的 研 究 项 目（ProTest7）所示 由于这个项目，La mbdaStream的 开 发 人 员 与UniversidadPoli t'ecnicadeMadrid的研究人员之间建立了富有成效的合作。这种归类的一个例子是使用McErlang对几个Lambda流组件的属性进行验证的经验，因为McErlang模型检查器非常适合验证这类并发软件组件。在本文中，我们描述了使用McErlang检查LambdaStream的管理器组件上的几个属性的经验。进程管理程序负责启动、停止和监视其子进程.测试和再现这种代码中的错误是固有的困难，由于其非确定性行为，异步通信，定时等。与此同时，建立该关键软件组件的可靠性至关重要，因为它集成到LambdaS-Stream的几个软件系统中。使用本文所述的技术，不可能完全验证该组件。这种局限性来自于状态爆炸问题，它是所有模型检测技术的一个特例.虽然主管已经在几个产品中使用了一段时间，并且经过了双方的测试，7http://www.protest-project.eu/D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）2325开发人员和一个特定的测试团队，并进行了部分验证，确定了组件规范和组件实际实现之间的差异。本文的其余部分组织如下。第2节简要介绍了Erlang和McErlang。第3节中给出了过程管理器组件的描述，以及我们所考虑的属性的简要描述。这些属性的实现和用McErlang检查它们的实验结果在第4节中解释。最后，在第5节中讨论了一些结论和未来的工作路线。2背景2.1Erlang编程语言Erlang [1，5]是一种并发编程语言和运行时系统。该语言的顺序子集是一种具有严格求值的动态类型函数式程序设计语言.并发性是通过异步消息传递进行通信的轻量级进程实现的。Erlang除了进程间的通信外，没有引起副作用的结构。表达式的求值与Standard ML类似.Erlang与其他函数式语言的不同之处在于它对并发和分布的支持。 使用Erlang的并发原语，它类似于Milner由于没有副作用，仅限于显式的进程间通信，并发编程比标准的命令式语言简单得多。一个Erlang虚拟机（Erlang术语中的node）承载多个并发运行的Erlang进程。通常，一个Erlang节点被映射到一个操作系统进程;事实上，一个轻量级的用户级线程，几乎没有创建和上下文切换开销。分布式Erlang应用程序由运行在多个节点上的进程组成，这些节点可能位于不同的（物理或虚拟）计算机上。尽管每个节点的初始化和管理都是依赖于平台的，但其良好特性是远程进程之间的通信在一个分布式框架，当然，尽管远程通信的效率较低。8严格地说，这是不正确的，因为Erlang有一个带有副作用的进程注册表，以及各种存储可变数据结构的库。然而，与其他编程语言相比，Erlang中这些特性的使用往往会大大减少26D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）23Erlang中的容错是通过将进程链接在一起来实现的，以便检测并可能从异常进程终止中恢复异常终止发生在，例如，一个函数试图访问一个空列表的尾部。与异常终止的进程相关联的进程会收到终止通知，因此可以采取纠正措施，即，可能重新启动失败的进程。流程链接始终是双向的，但双方对流程终止通知的处理可能会有所不同。处理大量进程很容易变成一项无法管理的任务，因此Erlang程序员大多使用库提供的高级语言组件。OTP（Open Telecom Platform）组件库[12]是迄今为止使用最广泛的库，包含几种可以用具体回调函数实例化的行为（Erlang中的设计模式）。例如，OTP行为包括通用服务器（用于客户端-服务器通信）、有限状态机或用于分层结构化容错系统的管理器组件，其中父管理器负责监督和管理其子（工作过程）。2.2McErlang模型检查器McErlang [7]是一个用于Erlang程序模型检查的工具。McErlang的输入是我们想要验证的Erlang程序以及感兴趣的属性。程序是模型的事实促进了在现实世界开发中的使用。由于模型检查工具本身是在Erlang中实现的，我们受益于动态类型函数式编程语言的优点：易于原型设计和实验新的验证算法，丰富的可执行模型使用直接在Erlang中编程的复杂数据结构，能够将可执行模型作为程序（由Erlang解释器直接执行）和数据互换处理等。为了使用Erlang程序作为模型，McErlang经历了一个源到源的转换，以准备在模型检查器下运行的程序。然后，实际的Erlang编译器将程序转换为Erlang字节码。最后，程序在McErlang运行时系统下运行，在验证算法的控制下，使用常规的Erlang字节码解释器。 代码的纯计算部分（即没有副作用的代码）和内存管理（包括垃圾收集）由正常的Erlang运行时系统执行。但是，副作用部分是在McErlang运行时系统下执行的，这是对基本进程创建、调度、通信和故障的ErlangD. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）2327Erlang的搬运机械。自然地，新的运行时系统将整个程序状态的简单检查点（捕获所有节点和进程的状态、所有进程的消息邮箱的状态以及在进程之间传输的所有消息）作为一个特征。使用McErlang执行模型检查所需的步骤如下：(i) 创建模型。直接使用Erlang程序。McErlang提供了对几乎全部语言的支持、全部数据类型的支持、对一般进程通信的支持、节点语义（进程间通信的行为方式与进程内通信有细微的不同）、故障检测和容错，并且至关重要的是，它可以验证使用大多数Erlang程序所使用的高级OTP Erlang组件库编写的程序。(ii) 制定正确性属性。写下要验证的属性，作为安全监视器或线性时序逻辑（LTL）中的公式。安全监视器用于验证安全属性（不好的事情永远不会发生），通过保持内部状态来检查要验证的程序达到的每个状态的属性。给定一个程序和一个监视器，McErlang以锁步方式运行它们，让监视器分析生成的每个新程序状态。 如果该属性不成立，则生成一个反例（执行跟踪）。 它们都能观察到 系统的形状（例如，哪些过程是活的）和重要的系统事件（例如，在进程之间发送的消息）。有些属性不能用安全监视器来表示，例如，liveness属性（最终会发生一些好的事情）。在McErlang中，人们可以用线性时态逻辑（LTL）来表达这些属性，并使用LTL2Buchi工具[11]自动将LTL公式转换为Bu？c hi自动机[3]。(iii) 生成场景。模型检查通常是内存密集型操作，并且频繁地完全验证大型系统可能需要比可用的更多的计算机内存。作为一次性验证整个系统的替代方案，我们指定了大量较小的系统场景，指定了系统配置和过程通信，因此每个场景都足够小，可以进行完整的验证。例如，如果要验证的系统是一个客户端/服务器架构，我们验证了大量的28D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）23工人1工人3工人2工人4工人5主管3主管2主管13案例研究：主管流程3.1监督的概念管理程序是负责启动、停止和监视子进程（Process）。基本上，每当一个子进程终止时，管理程序都应该重新启动它，即，产生一个新进程，执行被终止的子进程的任务。一个监督者通常不仅监督过程工人，而且监督其他监督者，定义了一个层次结构，如图1所示。1.一、Fig. 1. 监督树有几种策略可以说明管理程序进程应该如何处理子进程的异常终止这两项主要政策是：• 一对一：如果一个子进程终止，只有该进程重新启动。• onefor all：如果一个子进程终止，则终止所有其它子进程，然后重新启动所有子进程，包括最初终止的进程。通常有一种机制可以防止进程由于相同的原因重复终止，然后立即重新启动。该机制涉及最大重启强度。当一个子进程达到这个重新启动强度时，管理程序会终止所有子进程，然后终止自己。由于监管树是分层的，当较低级别的监管者终止时，则下一个较高级别的监管者可以采取纠正动作。也就是说，要么重新启动已终止的Supervisor（及其子系统进程），要么在该级别的Supervision树上无法处理错误时自行终止。除了重启策略，子进程的创建和终止顺序也必须在管理程序中指定。D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）2329·联系我们--3.2主管执行Erlang/OTP的开源发行版提供了监督程序行为的标准实现在本案例研究中，我们使用了与OTP实现略有不同的Supervisor进程LambdaStream公司实现了这个变体（从现在开始没有管理程序），因为他们希望更容易地将其产品集成到一个更可配置的特别地，对于nos supervisor中的每个子节点，允许不同的重启策略。在指定子进程之后，子进程由监督进程产生。在nos supervisor中，子规范是一个元组：{Id，StartFun，RestartFun，RestartStrategy，RestartIntensity，Restart，Options}• ID是一个名称，用于由主管在内部标识子规范• StartFun定义用于启动子进程的函数调用• RestartFun定义了重新启动子进程的函数调用• RestartStrategy。当一个子进程崩溃/死亡时，如果它的重启策略是child，那么只有这个子进程会被重启。如果其重启策略为all，则所有子进程将按反向启动顺序停止，并按启动顺序重新启动（包括最后• RestartIntensity：元组MaxR，MaxT，Finally或无穷大：MaxR，MaxT，Finally。如果在MaxT或更短的时间内重新启动子进程MaxR次，则会触发Finally操作：最后==杀了苏。管理程序以相反的开始顺序关闭其活动子进程，然后终止。最后，孩子停止了。未重新启动正在结束的子级。剩下的孩子继续正常重新开始。无穷大. 如果子进程终止，则主管程序将始终尝试重新启动它。• - 是的关断策略与OTP Supervisor中的相同。残忍的杀戮Supervisor终止进程，即，子进程P将由发送退出（P，kill）消息的管理程序无条件地终止。无穷大. 监督程序将通知子进程它应该终止，然后等待接收来自子进程的退出信号，表明它确实已经终止。（integer）. 如果在指定的时间内没有收到来自子进程的退出信号，则子进程无条件终止。···30D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）23--• Options是一个选项列表，其中的选项可以是持续重启，这意味着重启功能失败将被视为进程崩溃而不是重启错误，或者是notify，pid（），它使管理程序向指定的进程标识符发送不确定消息。3.3nos主管的属性通过阅读nos supervisor文档，我们发现了许多用于验证其实现的inter-sector属性 举一个简单的例子，我们想检查一个已经终止的子进程是否真的被它的监督程序重新启动。我们还关注了不同重启强度和关闭策略的属性，检查了这些选项的所有组合例如，我们制定并检查了一个属性，该属性声明，如果存在任何子指定，则重新启动强度的Finally操作设置为杀死sup并且这个子进程达到最大重启强度，以相反的开始顺序对其子节点应用策略，然后它完成了。在下面的部分中，我们将描述如何使用McErlang验证其中的一些属性。4使用McErlang进行为了使用McErlang验证上一节中描述的nos管理程序，我们遵循第2.2，即，我们创建了一个可验证的模型，我们制定了一些正确性属性，然后我们生成了一组场景。4.1创建模型由于McErlang可以使用实际的源代码作为模型，因此获得这个案例研究的模型非常简单。在本节中，我们将解释获得可验证模型所需的对nos管理程序源代码的唯一更改。为了测量重启强度，nos管理程序需要确定在特定时间间隔内发生的重启次数由于McErlang目前既没有实现实时模型检查算法，也没有实现离散时间模型检查算法，因此我们被迫从时间间隔中抽象出来add_restart（# child_spec {再起动强度=Infinity}）->[];add_restart（# child_spec {restart_intensity={MaxR，最大T，最终y}，状态=ChildState }）->Restarts=ChildState#child_state。restarts，Now = now（），check_restart% s（MaxRD. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）2331最后，，filter_restarts（MaxT、【现在|Restarts]））。正如我们在上面看到的，nos管理程序将每个进程的重启时间存储在一个列表中，然后使用当前重启时间与重启强度指定的最大时间之间的差异进行过滤。如果结果列表大于允许的重新启动次数，则触发Finally操作。 如果不是，则使用新的重新启动时间过滤列表返回：filter_restarts（MaxT，[H|Restarts]）->F =fun（重新启动）->difference（重新启动，H）caselingth（Restarts）>MaxRoftrue -> Finally;false -> Restarts端解决方案是不存储重启时的具体时间，而只是记录发生了重启（使用符号now），直到包含重启指示的列表的长度等于最大重启次数。因此，add restart的最后两行被以下代码片段替换：新Restarts=cases th（Restarts）>=最大R fruee->Restarts;false -> [现在|重新开始]结束，check_restarts（MaxR，Finally，NewRestarts）.过滤列表不再有意义，而是模型检查器必须考虑两种可能性：这些重新启动是否在最大时间内发生。McErlang允许使用mce erl：choice的函数调用来表达这种非确定性选择，将分支作为匿名函数列表，如下所示，并且在模型检查期间，将探索两种替代方案：check_restarts（MaxR，Finally，Restarts）->caselingth（Restarts）>=MaxRof真实->mce_erl： choice（[fun（）->最终结束，fun（）-> Restartsend]）;错误->重新启动端32D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）234.2制定正确性属性如2.2节所述，在McErlang中，正确性属性可以使用与系统并行运行的安全监视器来指定，以验证和观察其动作，或者作为线性时序逻辑的公式。在实践中，大多数相关的nos管理程序正确性属性可以表示为安全监视器。在McErlang中，安全监视器是作为Erlang行为实现的;实现安全监视器的模块必须实现以下回调函数：• 初始化监视器的init函数（返回监视器的初始状态）。• stateChange函数：当模型检查器计算新的系统状态时，使用以下参数调用该函数：（i）新的系统状态，（i i）监视器的当前状态，以及 （ iii ） 在 计 算 新 的系 统 状 态 期 间 发 生 的 系 统 动 作 的 序 列 。stateChange函数应确定在给定监视器的当前状态的情况下，新的系统状态和系统操作是否可接受。如果是这样，函数应该返回一个新的监视器状态，否则是一个失败的原因。4.2.1安全监视器示例在本节中，显示了一个安全监视器，它为nos管理程序检查一些属性相关权益物业为：• 孩子只有在死亡后才能出生• 如果没有兄弟进程已经终止太多次（因此它不应该被再次重启），则没有进程被NOS监督程序杀死为了能够确定是否允许由nos监督程序引起的进程生成或终止操作，监视器必须跟踪其所有子进程的状态。因此，监视器的状态是一个记录，记录了受监督的所有子进程- record（monitorState，%列表的死或从未开始儿童%下令通过的碰撞时间{deadProcesses=[]%儿童杀通过主管，杀死进程=[]%催生儿童目前活着、spawnedProcesses=[]%number的重新启动儿童、主管儿童=[客户端]D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）2333--，supervisorPid=undefined}）.监护仪的主要功能如下所示stateChange（_，MonState，Actions）->...情况interpret_action（Action）{died，Pid，normal }->{ok， Monstate};{died，Pid，Reason}->died（Pid，Monstate）;{spawn，SpawnInfo，SpawnedPid}->caseSpawnInfof{主管，强度}->setChildren（强度s，Monstate）;{worker，WorkerNam e}->spawned（{WorkerName，SpawnedPid}，Monstate）结束;{killedby，SourcePid，KilledPid}->killed（KilledPid，Monstate）;- -{ok， Monstate}端...其中，函数interpreter action将具体的程序操作划分为不同的抽象类别，并且对于每一个类别，它检查该操作在当前监视器状态下是否可接受。例如，actiondied，Pid，normal表示进程已正常终止（因此不应重新启动）。如果抽象操作表示一个新的子进程被派生，则调用函数spawnedspawned（{Workername，Pid }，State）->DeadProcs =#programState。deadProcesse% s，SpawnedProcs =#programState。他的爪子需要过程，caselists：member（WorkerName，DeadProcs）oftrue->#programState{deadProcesses=lists：delete（WorkerN ame，DeadProcs），spawnedProcesses=[{WorkerName，Pid}| sort]};错误->throw（已经）产卵。工人 ”）端派生函数检查新派生的子函数（的名称）是否尚未派生，并将新的子函数从死进程列表中删除，然后将其添加到派生进程列表中。如果子进程已经生成，则抛出一个异常，通知McErlang监视器发现错误。34D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）23类似地，当一个子进程异常死亡时，调用deed函数，它会增加子进程的重启计数器。当nos管理程序终止子进程时，将检查此计数器，以确保已终止进程的某个兄弟进程有趣的是，我们使用安全监视器来制定正确性属性的方式。不是在时态逻辑中指定它们，而是开发一组简化的系统模型，然后检查实分量的行为是否与这些模型相对应。使用相同的语言进行常规开发和指定安全监视器，使开发人员易于采用这种技术4.2.2检查活动属性一些特性，即，表达关于最终行为的声明的活性属性不能被实现为安全监视器。在这种情况下，我们可以用LTL来表达这个属性，并使用从LT Lfor mulae到Bu？chi监视器的自动翻译器。例如，在案例研究中，要检查的一个有趣的属性是，子进程总是异常终止，它最终会重新启动。此属性表示为：总是（P =>最终Q）其中P和Q分别是断言子进程异常终止和死子进程重新启动。这些谓词在Er-lang中指定，并且LTL公式中的名称与具体实现之间的对应关系必须交给McErlang。 作为谓词的一个示例，此函数实现声明子异常终止的谓词：child_terminated（_，Actions，_）->lists：any（ fun（A）->try模具d==mce_erl_act ions：类 型 （A），normal=/=mce_erl_actions：get_died_re ason（A）catch _：_ -> false end结束，动作）。可以看出，谓词是一个接收三个参数的函数。第一个是程序状态，第二个是触发状态改变的动作，第三个是一些私有状态。如果任何操作是对应于进程死亡的操作（死亡操作），其原因不同于正常情况，这意味着子进程异常终止但是，请注意，此属性仅适用于子级具有重启强度无穷大的nos主管;否则，在足够多的死亡次数之后，子级将不会重新启动。要检查更复杂的特征，D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）2335我们需要保留一个私有状态，并在状态谓词之间传递它（在生成的Bu？hi自动机中，这个状态对应于一个监视器状态4.2.3模块化安全阀与其试图使用单个复杂的安全监视器来检查系统的所有期望属性，不如定义多个安全监视器，每个安全监视器检查系统的特定属性。这种方法降低了使用不正确的安全监视器检查系统的风险，因为生成的监视器更容易理解和编写。此外，安全监视器代码的大部分在编写新代码时是可重用的。也就是说，将具体操作转换为抽象操作的策略，以及在进程死亡、生成和杀死时更新监视器状态的方式，是完全通用的。从一个安全监视器（属性）到另一个安全监视器（属性）的变化是如何解释动作-即，当动作信号的出现被解释为错误时。这些是用于验证超级监视器组件的一些安全监视器：(i) 主管总是试图重新开始一个孩子，直到一个达到最大的重新开始强度。适用于检查重新启动强度不同于无穷大的子规范，并具有终止最终动作。(ii) 当一个孩子达到其最大重启强度时，活着的工作者以相反的启动顺序被杀死，然后它终止。适用于重新启动强度不同于无穷大的儿童规格，并具有杀死最终动作。(iii) 当一个孩子达到最大的重新开始强度时，生活工作者以相反的开始顺序停止。 适用于重新启动强度不同于无限（killsumminallyaction）和无限（infinity）作为关闭策略的子规范。(iv) 如果一个孩子有无限的关闭策略，监督者永远不会杀死它。(v) 如果一个子进程使用整数作为关闭策略，那么管理程序在尝试停止进程之前不会杀死(vi) 当子进程的关闭策略为stop child时，当Supervisor停止时，未重生的工作进程已达到其最大重启强度。(vii) 对于所有重启策略，当一个子节点死亡时，管理程序将以相反的启动顺序杀死活着的子节点36D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）23(viii) 对于所有重启策略，在杀死所有存活的子进程之后，工作进程将按开始顺序重启。4.3验证情景为了使用McErlang针对上述正确性属性验证nos监督程序，手动设计了许 多 场 景 ， 尽 管 自 动 生 成 它 们 应 该 不 会 太 困 难 （ 例 如 ， 使 用QuickCheck-/Erlang [2]）。为了创建这个场景，我们实现了一个测试工作者，它只跟踪它的开始时间。为了模拟进程崩溃，我们启用了McErlang模型检查器中的一个选项，非确定性地，杀死任何状态下的任何进程。我们通过执行以下命令来选择一个正在运行的进程的子集进行终止：mcerlang：process flag（do terminate，true）在任何可能终止的进程中（在案例研究中，工作进程）。因此，一个工作进程可以在任何时刻非确定性地死亡，这将导致nos管理程序被通知（并希望采取行动）。作为一个具体场景的例子，如果一个子节点死亡，那么最终nos管理程序将重新启动该子节点，检查liveness属性，最简单的适当场景将是一个nos管理程序，它使用restart strategychild生成一个子节点（其余选项不相关）。{工人1，{nos_test_worker，start_link，[worker1，foo]}，{nos_test_worker，restart_linkk， {worker1，foo}}，child，infinity，brutal_kill，[]}我们确定了相关的场景，作为一个nos主管，至少有一个(two或三个，取决于属性）子进程。一个场景中的所有子进程都具有相同的简单性规范每一个场景都被选择来验证与nos管理程序的行为相关的属性，这些属性与nos管理程序的一些选项相关例如，如果我们想验证当一个子进程达到其最大重启强度时，nos监督程序是否正确地评估了Finally操作，我们只需要一个不同于无穷大的重启强度，但是我们必须 知 道 我 们 应 该 期 待 一 个 退 出 （ kill ） 还 是 一 个 退 出（shutdown）（应用的是哪种关机策略）。4.4McErlang出版社如果一个属性失败了怎么办？ McErlang提供了一个工具，用于探索反例，手动探索状态空间，. 关于McErlangD. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）2337}联系我们调试器当使用安全监视器2运行模型检查器时，McErlang返回一个反例，表明此属性失败：* 在最小深度13处* 显示器失败显示器错误：{failed_monitor，“Processes not killed in reverse start order”}堆栈深度13个条目;状态表包含44446个状态。使用get（result）要查看反例，请键入“mce_erl_debugger：start（get（result））。“的...可以看出，示出了导致错误的迹线的长度，以及故障的具体情况。在给出的程序跟踪中，通过调试器，我们意识到kill命令不是规范中提出的。调试器还允许我们手动探索状态空间以分析其他路径，并帮助我们定位错误（在什么情况下会出现此错误）。4.5实验结果根据第4.3节所述，在一组场景上检查了上述安全监视器。我们在这里提出了一些措施，在英特尔（R）核心（TM）2四在2.33 GHz的4GB的RAM存储器。图2显示了模型检查器探索的状态数（图2a）和所需的时间（图2b）。2b）检查第2b节中给出的安全监视器（i）4.2.3，对于具有重启策略子级的场景，重启inten.{1，1，kill sup}的值和不同的工作进程数。状态空间可以根据场景参数而变化（使用相同数量的工作者）。例如，模型检查器使用1，1，killsup、2，1，killsup和3，1，killsup探索的状态数分别为6617、13656和26712。正如模型检查技术所预期的那样，状态空间以指数方式增长，使得难以使用实际实现作为模型来检查大型场景。然而，尽管nos supervisor行为已经部署在许多LambdaStream产品中，并且预计不会发现真正的关键错误，但令人惊讶的是，在组件文档中的规范和nos supervisor的实际实现之间发现了一个差异。McErlang返回了一个反例，38D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）2310610510410310310210110010−11 2 3工人数量(a) 探讨的国家1 2 3工人数量(b) 需时间图二. 探索的状态和所需时间（重启策略=子，重启强度={1，1，kill sup}）。如果具有指定kill_sup和Finally的任何子节点达到最大重新启动强度，则管理程序仅在所有“较年轻”子节点（在该子节点之后启动的那些子节点）没有运行（停止、被杀死、崩溃、死亡等）之后才杀死该子节点。. ）的。使用McErlang调试器分析了McErlang返回的反例，结果发现一个 他们不是按照文件中明确规定的相反顺序被杀的。 虽然这种差异似乎并不相关，但在某些情况下可能会导致不当行为。例如，如果相互依赖的工作者需要在停止之前执行某些操作，则按指定的顺序。5结论在本文中，我们使用McErlang工具在部署为几个真实产品的一部分的流程管理器上探索了安全性和活性属性的验证由于这种验证，我们提高了组件的可靠性，不仅因为识别出从这一验证中，我们可以得出结论，模型检查是分析并发程序的一种有价值的技术，并且McErlang可以成功地应用于工业软件。我们遵循的方法包括三个步骤：（a）为组件创建模型，（b）表达和实现感兴趣的属性，以及（c）创建检查属性的场景创造-探讨的国家时间（秒）D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）2339创建模型是一项简单的任务，因为McErlang可以使用源代码作为模型，只需进行最小的更改。在案例研究中，唯一需要的更改是从监督程序的时序方面抽象为非确定性选择，因为目前McErlang既没有实现实时模型检查算法，也没有实现离散时间模型检查算法。尽管我们已经能够在不考虑确切时间的情况下验证监督程序的大多数方面，但未来工作的一个重要方面是为McErlang添加对实时模型检查算法的支持。感兴趣的属性是从组件文档和与Supervisor组件开发人员的非正式讨论中提取的。大多数属性都是用Erlang编写的安全监视器，它在管理一组子组件时观察Supervisor组件的操作，并在Supervisor发出错误命令时发出错误信号。换句话说，我们定义了一组简化的模型，并检查真正的监督程序是否具有与模型相同的行为（直到监视器的抽象层为了解决模型检查不可避免的状态爆炸问题，我们不将McErlang模型检查器应用于大型单一场景，而是定义和检查大量较小的场景（例如，工作流程的数量）。尽管验证是部分的，因为我们无法检查每一个可能的场景，我们发现文档和组件的实际实现之间存在差异，在一个由一个主管和三个孩子组成的与其他模型检查器相比，McErlang中采用的模型检查方法的一个显著优点是，不需要学习新的规范语言，因为Erlang既用作编程语言又用作规范语言。这是可以实现的，部分原因是函数式编程语言的内在力量，它具有足够的表达能力，既可以用于编程，也可以用于编写更抽象的规范。这种技术可以用来检查大型系统的属性，尽管必须始终选择一组小的场景但显然还有很大的改进空间。学习曲线能够有效地使用McErlang，并制定正确性属性， 目前太高了。在McErlang的下一个版本中，计划对工具的可用性进行改进，例如，提供有关错误原因的更好信息，选择适当验证选项的指导，以及用于正确性属性公式化的简化API40D. Castro et al. /Electronic Notes in Theoretical Computer Science 271（2011）23引用[1] J· 阿 姆 斯 特 朗 《 Programming Erlang ： Software for a Concurrent World 》 PragmaticBookshelf，2007.[2] T.艺术和J·休斯快速检查Erlang。在2003年Erlang用户会议（EUC）上，2003年。[3] J. Büchi。 关于限制二阶算术中的一种判定方法。1960年国际逻辑、方法论和科学哲学大会出版物，第1-11页。北京：清华大学出版社.[4] C. 贝 纳 克 厄 尔 湖 Fredlund ， J. Iglesias ， and A. 利 迪 玛 Robocup 团 队计 算 机 科 学 讲 义 ，5348/2009：34[5] F. Cesarini和S.汤普森Erlang编程[6] L. F redlund和J. S'anchezPenas.使用McErlang修改VoD服务器。在2007年Eurocast会议记录中，2007年2月。[7] L. Fre