进程代数中的动态一致性与Paradigm协调建模语言的自动验证 (Process Algebra and Automated V...

理论计算机科学电子笔记229（2009）3-20www.elsevier.com/locate/entcs进程代数中的动态一致性：从范式到ACPS. Andova1，2形式方法组荷兰埃因霍温理工大学L.P.J. 格勒内韦根FastGroup，LIACS荷兰莱顿大学E.P. de Vink形式方法组荷兰埃因霍温理工大学摘要协调建模语言Paradigm解决了组件之间的动态约束方面的协作。在Paradigm模型中，组件动态在不同的抽象层次上被一致地指定。为了实现Paradigm模型的自动验证，提供了Paradigm到进程代数的转换。给出的例子和指导方针，系统的翻译成过程代数ACP进行了讨论。还提供了基于mCRL 2工具集的验证结果关键词：自动验证，协作，动态一致性，动态约束，范式，进程代数1介绍进程代数正成为从软件体系结构和描述形式主义到自动分析和验证工具的重要垫脚石，例如[1、16、14、13]。在本文中，我们通过进程代数ACP与mCRL 2工具集连接协调建模语言 这样，1通讯作者2 电子邮件：s. tue.nl1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.06.0264S. Andova等人/理论计算机科学电子笔记229（2009）3将软件系统视为松散耦合但结构化的组件集合的协调与过程等价性和模型检查的计算严格性有关。一个系统的翻译范式协作作为一个递归的specification系统的并行进程。范式的核心是沿着两个轴分解动态约束：（i）垂直方向，一个组件在它参与的所有协作中所扮演的角色的限制，（ii）水平方向，协作中参与者所执行的子行为的协调和同步协调建模语言Paradigm [8，9]指定了组件之间协作中的角色和相互作用是对部件动态特性的暂时约束。约束可以是两种类型，或者纯粹的顺序每个组件（垂直）或逐步同步的组件（水平）的合奏。顺序约束对应于组件协议中的角色，即组件底层的行为视图，通常是隐藏的动态。同步约束对应于组件对协议的分布式执行，它们的角色的指定并行化，构成动态一致的协调计算。Paradigm的特点是，通过适当的约束组合，它允许建模进化和自适应[9]。进程代数（Process Algebra，简称PA），如CCS、CSP、LOTOS、ACP等，为并发系统的形式化建模和推理提供了一个强有力的框架。基石是组合性的概念。该系统的每个组件分别建模，并获得完整的系统作为其相互作用的组件的并行组合。此外，进程代数具有定义动作的同步和隐藏的机制（通过将它们重命名为所谓的沉默动作τ）。进程代数ACP [2，4]的特征是用户定义的通信功能|多个动作，例如，<${a，b，c}（a.P <$b.Q <$c.R）产生d。（P Q R）如果我们有一个|B |c = d。可以建立各种等价关系过程结石对于ACP，强互模拟和分支互模拟是突出的。本文首先通过两个实例介绍了范式模型在PA中的翻译。在这两种情况下，系统由n个客户端组成，他们试图从一个服务器上独占服务，这是一个临界区问题。不同之处在于，在一个示例中，服务器应该以非确定性方式选择下一个客户端，而在另一个示例中，这是以循环方式完成的。对于这两个示例，给出了到PA的翻译，并讨论了使用mCRL 2工具集的后续分析。虽然两个示例的Paradigm模型到PA的转换都是手动完成的，但是整个系统的状态空间（包括所有交织和交互）的计算及其分析超过了人类的能力，客 户 数 量 增 加 。 (As 在 第 4 节 中 讨 论 过 ， 对 于 n 个 客 户 端 的 系 统 ， 这 是（5·2n−2−1）·n+ 1。）利用工具集mCRL 2，释放按钮技术来生成完整的符号状态空间，可以做到。这两个例子的功能正确性的几个性质S. Andova等人/理论计算机科学电子笔记229（2009）35检查过了例如，正如预期的那样，非确定性服务器不保证最终访问服务，除非假设公平性。相比之下，轮询服务器保证在一个周期内访问，这也不足为奇。然而，主要的一点是，一旦翻译成ACP已经实现，分析范式合作的正式方法是触手可及的。因此，将协作嵌入到进程代数中，在协调的抽象级别上带来了模型检查我们翻译成PA保留了原始范式模型的一般结构和动力学，这是我们在翻译成Petri网时不希望持有的属性。因此，要讨论的轮廓，一个反例得到的模型检查可以追溯到原来的范式模型。相关工作。 我们在水平和垂直维度上的一致性工作已经被Küster的工作[6，12]所证实。基于CSP的Wrightlangage[1]提供FDR支持以检查静态一致性属性。除了Paradigm内置的一致性，Paradigm建模的重点是动态和约束的变化。至于Korrigan ADL [15]，形式主义应该 不仅仅是一个框和线的符号。Paradigm协作的管理者让人想起[3]的编排连接器。然而，在Paradigm中，管理者和协作的协调是明确分离的，产生了不同从软件架构到自动化验证的其他桥梁包括从UML通过Object-Z和Promela到SPIN模型检查器的管道，以及从UML通过Object-Z和CSP到FDR模型检查器的管道[17，13]。在[16]中提出了作为CCS协调的过程代数驱动原型。CCS规范生成的骨架与Paradigm协作重叠。在TITAN框架[14]中，CCS在面向方面软件工程的异构环境中扮演着统一的角色。论文的结构。在第2节中，我们给出了Paradigm的基础知识以及两个运行的示例。第三节简要介绍了进程代数。在第4节中，给出了两个协议的Paradigm模型的详细翻译，然后在第5节中给出了Paradigm模型的一般翻译。第六节是论文的总结。2范式与两个临界区模型本节简要介绍范式的主要概念。通过两个例子，这将被用作贯穿全文的运行示例，解释了范式方法的主要方面。我们还介绍了一个UML风格的架构图的协作组件，为各种动态概念的阶段。我们指出的范式的概念是相关的，以及如何动态的一致性可以得到保证。范式的基本概念包括6S. Andova等人/理论计算机科学电子笔记229（2009）3出来进入等待离开在门口不• 状态转换图或STD是一个三重转换图，AC，TS。这里，ST是状态的集合，AC是动作的集合，TS是转换的集合。转换（x，a，xJ）∈TS被称为从状态x到状态xJ，并表示为：x→axJ。• STD_BLOCK_ST、AC、TS_BLOCK的子过程或阶段是STD_BLOCK_ST、AC、TS_BLOCK，使得stST，ac AC和ts {（x，a，xJ）∈ TS |x，xJ∈ st，a ∈ ac}.• 相位S=λst，ac，tsλ st的陷阱t是状态tλst的非空集合，使得x∈tandx→axJ∈tsimplythatxJ∈t. 一种方法是将相位设置为对于没有相位的情况，SJ=AstJ，acJ，tsJ，如果t是tJ，则旋转S→tSJ。• 一个分区{（S i，T i）|i∈I}是一组相位Si={i，aci，tsi}，每个相位都有一组陷阱Ti。• 在分区π ={（S i，T i）}级别的全局进程或全局STD |i∈I}，anSTDZ=πST，AC，TSπsanSTDZ（π）=πS^T，A^C，T^Sπw ihS^Tπ{Si|i∈I}，A^C<$i∈ITianddT^S<${Si→Sj|i，j∈I，t∈A^C}是phechanges的集合。Z是称为全局STDZ（π）的详细STD。客户端−i没有3 每个Client-i分区的阶段特里夫中断与中断与notYet做请求图1.一、（a）STD，（b）相位和（c）圈闭约束和分区。STD是属于某个组件的动态的从状态到状态的逐步描述。它通常被可视化为一个有向图，其中节点是状态，而标有动作的边是转换。STD的初始状态用黑色点箭头表示。图1a给出了商店内和周围的示例STD客户端i我们稍后考虑的整个系统包含n个这样的客户端，每个客户端具有相同的动态（以及其他组件）。状态和动作的含义应该是不言自明的。总的要求是，只有一个客户端在一个时间，所有n个客户端，被允许在其状态忙。因此，处于忙碌状态是一个临界区问题（CS供以后使用）。为了解决这个问题，客户端i动态受到规定相位的约束。图1b显示了无、无和有三个阶段。无阶段通过禁止采取解释和感谢的动作（标有）来排除处于忙碌状态。实际上，阶段With允许进入和离开状态Busy。最后，阶段“没有”是“没有”的中断形式，因为不能采取行动“进入”，但等待等待解释在门口谢谢 忙出来离开门口出来进入等待解释离开在门口谢谢忙S. Andova等人/理论计算机科学电子笔记229（2009）37但是，等待状态是允许的鉴于当前阶段要转变为下一个阶段，当前阶段必须取得足够的进展;必须首先进入连接陷阱。图1c描绘了上述三个阶段的相关连接陷阱特别是，我们需要traptriv从Without 连 接 到 Without ， trapnotYet 从 Without 连 接 到 Without ， traprequest 从Without连接到With，最后trapdone从With连接到Without。以这种方式，图1c给出了在这些阶段及其陷阱的更高、更全局水平上的客户端i这些成分构成了一个分区以及一个全局STD客户端i（CS）两个额外的平凡陷阱，trivofa和triv ofWith，对于更高层次的动力学来说并不真正需要，也没有画出来。Client−i（CS）global STD Client−i（CS）...及其ACP-改进没有[Triv][notYet]notYet做特里夫notYet完成[done]三[triv]做请求（三）请求[request]请求全局STD Client−i（CS），精确形式图二. (a)全球进程和（b）完善的全球进程。图2b显示了一个稍微细化的“官方”全球STD图。在这里，状态名称跟踪当前阶段- 就好像它可以被看作是当前施加的一个阶段中的一个较小的阶段;动作名称类似地指相应的陷阱进入。正如下面将要指出的，全球过程的细化形式为我们的PA翻译服务到目前为止，我们已经讨论了约束的顺序组合：通过提交的陷阱交替施加阶段。任何当前阶段都将可选择的操作约束为属于该阶段的操作。因此，在任何时刻，当前的详细状态也应该属于当前阶段。由此，详细的STD和全球STD的一致动态如下。Paradigm的一致性规则是同步合成的本质。它们规定了所谓管理者的详细行为和任意多个所谓员工的全局行为的组合。任何一致性规则都描述了经理的步骤和每个员工的全局步骤的同时执行。图3展示了一个Paradigm模型的概述，它是UML对象、复合结构和协作图的自由混合名为Clienti的元素是employeenotYet特做打断与请求没有8S. Andova等人/理论计算机科学电子笔记229（2009）3CS客户端−n客户端-1服务器一般协作. . .员工-n员工-1经理-m经理-1检查1检查2垃圾NDChecking1 NDChecking2许可证继续继续NDHelping1 NDHelping2检查−n拒绝NDChecking−n允许继续ND帮助−n空闲P.罗托好的。L作用作用P.罗托好的。L客户端-1（CS）Client−n（CS）. . .. . .图3.第三章。Paradigm架构的印象CS协作的组成部分。作为员工，他们为协作贡献自己的动力，不是直接的，而是通过全球STD客户端i（CS）作为角色。适当同步的角色是协议，其动态由一个或多个管理器驱动，每个步骤只有一个管理器一致性规则以一致的方式指定协议动态：Paradigm的约束表示单个角色动态和相应的单个详细员工动态如何保持一致。从语法上讲，一致性规则将来自不同全局STD的全局步骤（出现在规则的右侧，作为阶段更改列表）与左侧的一个详细管理器步骤相对于我们的运行示例，n个客户端一次一个地获得服务，我们将考虑服务器与n个客户端的协作的两个实例，一个是非确定性的，一个是循环的。非确定性服务器以任意顺序检查如果被检查的客户端准备好被服务，则它被服务，也就是允许进入临界区。如果没有，客户将被拒绝。只有在完成对特定客户端的服务后，服务器才返回到空闲位置，在那里它可以再次选择任何客户端进行检查。NDetServer. . .见图4。 STD非确定性管理器NDetServer。非确定性服务器NDetServer的STD包括图4。作为管理器，NDetServer的详细步骤需要耦合到客户端的阶段。这可以按如下方式NDetServer：Idlech→eckiNDChekingiC inti（CS）：Witt→riv中断NDetServer：NDCheckingire→fuse允许IdlecloeClienti（CS）：Interruptno→tYet请求没有NDetServer： NDCheckingi→ NDHelpingi客户端i（CS）： NDetHelping→与NDetServer：NDHelpingicon→tinueIdlel'english（CS）：I'msorry.d→oneW ith out其中注意，对于该协议，服务器的管理器步骤对应于恰好一个客户端的阶段改变例如，在一个示例中，服务器从Idle状态移动到NDChecking状态S. Andova等人/理论计算机科学电子笔记229（2009）39我一期+1→ii+1RoRoServer通过进行RR检查1格兰特通过RR检查2格兰特进行通过. . .通过进行RRHelping1 RRHelping2RR检查−n格兰特进行RR帮助−n客户端进程Clienti（CS）从阶段Without变为阶段Through。然后服务器进行检查i转换。但总的来说，有一个前提条件。在没有足够进展的阶段内，应该已经取得了进展，这样就达到了陷阱，在这种情况下，是平凡的陷阱triv。在这里，需求是空洞的，就像琐碎的陷阱，由详细的性病，是微不足道的达到。对于实际的检查，上面的两个中间一致性规则，取决于陷阱，即notYet与request，决定了经理转换和下一个员工阶段的目标，即。状态Idle和phaseWithout或状态NDHelpingi和phaseWith。在本示例中，一致性规则保持水平一致性在服务器和客户端之间。客户端的详细转换需要被当前阶段和相关陷阱允许的约束一方面强制雇员的垂直一致性，另一方面强制其在协作内的抽象。作为上述示例的一个变体，我们接下来考虑对服务的循环访问现在，服务器依次检查客户端是否有请求被服务。如果需要的话，客户等待检查。服务器RoRoServer的STD如图5所示。在我们的设置中，服务器充当分区CS的管理者，每个客户端通过其全局进程Clienti（CS）是分区CS的雇员使服务器的详细步骤和客户端的全局阶段同步的一致性规则如下（隐式地以n为模计数且1≤i≤n）：RoRoServer：RRCheckingigr→antRRHelpingC S：Int erupreq→uestWithRo RoServer：RRHelpingipro→ceedRRCheckingC_S=C_S特里夫无，客户端i+1（CS）：无中断Ro Ro服务器：RRCheckingp→assRRCheckingpClienti（CS） ：Intruptno→tYetWithut，Clienti+1（CS） ：Withutt→RivIntrupt注意与非确定性协议的区别例如，在这里的第二一致性规则中，客户端i（CS）的全局步骤done的服务器步骤proceed与客户端i+1（CS）的全局步骤triv之间的同步准确地表达了客户端i离开临界区和客户端i+1被中断以被检查的同时事件。相比之下，在前面的非确定性情况下，类似的协调分为两个一致性规则，即首先在帮助客户端i之后，服务器返回空闲状态，然后检查下一个客户端。图五. STD循环管理器RoRoServer。10S. Andova等人/理论计算机科学电子笔记229（2009）33进程代数进程代数（Process Algebra，PA）是一种用于并发进程系统建模和分析的形式化方法.任何PA的基本成分是一组运算符，包括常数和一组方程，也称为公理或定律，捕获运算符之间的依赖关系。PA通常由一组原子操作A参数化，A是流程可以执行的最小活动。在PA中，动作被视为常量。其他的基本运算符是顺序组合的“统计”、非确定性选择的“+”和并行组合的“否”。我们将在这里考虑的进程代数ACP [2，4]具有额外的操作符，封装'H '和抽象' τ I '。封装运算符抽象运算符过程由代数表达式描述，过程之间的关系无限过程可以用递归的规范来表示。例如，一个进程Clienti，单独考虑，由以下递归规范描述：外出i=进入i·等待i等待i=解释i·忙i忙i=谢谢i·在门口i在门口i=离开i·外出i在规范中，索引i显示为范围在{1，.，n}。注意，进程Clienti具有没有任何分支的顺序行为，因此，在描述中不会出现非确定性选择两个过程的并行合成的行为是通过交织两个独立的行为得到的。此外，进程可以通过同步某些操作来进行通信。在ACP中，动作同步是由用户定义的所谓的通信功能。通信功能可能涉及两个或更多个参数，从而实现多方同步。正如我们将在第4节中讨论的那样，通过通信进行同步非常自然地表达了范式中的一致性规则。这并不奇怪，因为它们都是为了表达某些行为之间的同步。更高级别的抽象行为是通过隐藏活动来获得的，这些活动被认为是内部的。这些动作随后将在进一步的计算中被忽略（在很大程度上）。例如，图2a中所示的流程客户端的更抽象的行为。可以很容易地从图2b中的流程的更详细的行为中获得，通过抽象出以下事件：状态With[triv]和With[done]之间的actiondone，状态[triv]和状态[notYet]之间的actionnotYet以及类似的actionrequest。抽象行为首先通过将这些作用重新命名为特殊作用τ，然后通过一些代数定律来操纵特殊化，这些代数定律允许从特殊化中删除一些τS. Andova等人/理论计算机科学电子笔记229（2009）311如下所述，范式模型的过程代数描述有助于我们在更详细的层面上“观察”动态。例如，在Paradigm中，一个阶段对详细的STD动态施加约束的机制是隐含的，而在进程代数中，这必须显式指定。事实上，它被定义为交换某些信息的两种行为的同步，在这种特定情况下，允许或不允许进行某些步骤。一旦构建Paradigm模型的所有组件都被转换为过程代数，原则上，就可以计算出完整的行为。此外，各种验证技术可以应用于所获得的系统。一种被广泛接受的用于验证系统属性的技术是模型检查，我们在下面也会使用这种技术简而言之，一旦以STD的形式获得模型，就可以针对系统的模型来检查模态公式。例如，可以验证属性“在任何时刻，在关键部分中最多有一个客户端”是否通常，描述整个系统的模型非常庞大，没有计算机的帮助，人类无法进行推理。幸运的是，已经开发了许多有效的工具来支持分析，特别是提供模型检查的自动化工具。为在我们的实验中，我们使用了工具集mCRL 2[10，11]。3它的形式化规范语言mCRL2是基于ACP，以及抽象数据库的设施和符号化的参数化布尔方程系统（PBES）方法。模型检查的目的。4两个翻译成ACP的在本节中，来自前面介绍的范例模型的各种STD将被转换为ACP过程。特别是，每个STD将被解释为一组递归定义的进程，并扩展了特定的通信细节。 对于详细STD和全局STD的通信，我们使用actionsok？（。）和ok！（。），将详细步骤的标签作为其参数。如果详细STD当前阶段允许将其作为约束。此外，我们使用的行动在？（。）和在！（。）以将当前状态从详细STD发信号通知给全局STD。在同步这些操作时，全局进程将更新其陷阱信息。对于协议内的通信，例如服务器与其客户端之间的通信，动作man（. ）是为了补充emp（. ）员工方面的行动。同步导致执行相应的一致性规则：经理的本地转换，涉及的员工的阶段变化对于两个具体的例子，这产生了以下结果。我们装饰了n个进程3可查阅http://www.mcrl2.org。12S. Andova等人/理论计算机科学电子笔记229（2009）3i=1客户端i与状态动作在！和过渡动作好吗？出去！（Outi）. 我出去好吗？（输入i）。我在等我在等！（等待i）。等待i+ok？（解释一）。 忙我忙i=ok？（谢谢）。在门口i在门口i=at！（在门口i）。在门口i+ok？（离开我）。 奥特岛以类似的方式，n个进程客户端i（CS）与在？OK！由于这些全球流程作为员工参与到协议中，因此emp行动也已到位。见图1我是你的[三V] =O K！（lea vei）. 我是你的[三V]+O K！（输入i）。[三v]+emp（trivi）. Interrupti [triv]i[triv]=at？（在门口i）。 i[notYet] +at？（Outi）. [notYet]+在哪里？（等待i）。[request] +ok！（离开我）。i [triv] Inte rupti[not Ye t] =o k！（lea vei）. Inter rup ti[not Yet]+em p（not Yeti）.Withouti[triv]Inte rup ti[reques t] =em p（requesti）. Withi[triv]Withi[tri v] =a t？（AtDor）i. Withi[don e] +o k！（explain ni）. Withi[triv]+ok！（谢谢）。 Withi[triv]Withi[don e] =em p（donei）. 我是你的朋友。非确定性NDetServerSTD由以下规范定义空闲=nman（检查i）。 NDCheckingiNDranking gi=ma n（permiti）。 NDHelping gi+ma n（refusei）. IdleNDHelpingi =man（continuei）.无所事事。另见图4。 对于通信功能，|”“我们把在！（个）|在哪里？（s）=at（s）和ok？（一）|好的！（a）=ok（a），对于s=Outi，Waitingi，AtDoori，和a=enteri，explaini，thanki，leavei。注意，ACP允许保持同步的结果动作可观察，这对验证很有用。此外，在由NDetServer驱动的协议的情况下，我们假设人（检查i）|emp（trivi）=检查i男子（许可证i）|emp（requesti）= permitima n（refusei）|em p（not Yeti） =refusei男子（续一）|emp（donei）= continuei.来自集合H={man，emp，at？，at！，好吗？，好！}需要被阻止以加强通信。最后，协作过程如下所示CSNDet= CSNH（客户端1）CSNDet = CSNH（客户端1（CS））CSNDet. 客户端n客户端n（CS）NDetServer）。对于循环调度的情况，客户端iSTD的转换保持相同。全局STD客户端i（CS）的转换仅略有变化。我们只需调整客户端1（CS），即第一个客户端的全局流程。这是因为这一全球STD将在第二阶段开始。更具体地说，它的起始状态是[triv]。S. Andova等人/理论计算机科学电子笔记229（2009）313客户端1（CS）=i[triv]，客户端k（CS）=无i[triv]，k≥1然而，RoRoServer的STD确实有一个相当不同的翻译，14S. Andova等人/理论计算机科学电子笔记229（2009）3协议的不同特征。 参见图5。RRCheckingj =man（grantj）. RR帮助j + man（passj）. RR检查j+1RRHelpingj =man（proceedj）. RR检查j+1。循环协议的通信函数定义为男子（格兰特一）|emp（requesti）= grantiman（proceedi）|emp（donei） = proceedi人（通过i）|emp（notYeti）|emp（trivi+1） 帕斯岛被阻止的动作的集合现在被定义为HJ={man，emp，at？，at！，好吗？，好！}中。轮询协议的完整协作过程定义如下：CSRoRo= HJ（Client1 Client1（CS）... 客户端n客户端n（CS）RoRoServer）。将 基 于 ACP 的 规 范 转 换 为 n 个 客 户 端 Clienti 、 全 局 Clienti （ CS ） 和 服 务 器NDetServer和RoRoServer的mCRL 2工具集的输入语言在很大程度上是简单的。在附录中，给出了三个客户端的协作流程的mCRL 2规范。与ACP规格的相似性是显而易见的。根据这些规范，该工具生成相应的转换系统。对于四个客户端，协议由1080个状态和3456个转换组成。然而，如果我们从内部通信中抽象出来，专注于临界区的入口和出口，它可以减少到77个状态，仅使用分支互模拟204个转换更一般地说，我们发现在循环调度的情况下，对于n个客户端（n≥2），状态的数量可以减少到（5·2n−2−1）·n+1。我们考虑两个协议的以下属性，其中我们假设clients客户端i和客户端j对于i j：1. 在任何时候，最多只有一个客户端将被提供服务。换句话说，永远不会有两个（或更多）客户端同时处于临界区。在μ演算中，mCRL 2的属性指定语言，它表示为[ true*.ok（explaini）.（！ok（thanki））*.ok（explainj）]false一系列动作，其中出现ok（explaini），并且在稍后的某个点出现ok（explainj）和noactionok（than ki）。例如，我们使用ok（解释i）和ok（感谢i）来检测进入和离开临界区。更多细节请参见[5]。2. 在任何时候，服务器都不允许为两个不同的客户端提供服务。换句话说，不允许两个或更多个客户端同时访问临界区。显然，这对应于前面的属性，只是从服务器的角度来看。在μ演算中，对于RoRoServer（以及类似的NDetServer），它表示为：[真 *.格兰特岛（！proceedi）*.grantj] false3. 两个客户端可以同时请求访问临界区。换句话说，在详细STD中，可以有多个客户端处于等待状态我再次重申，S. Andova等人/理论计算机科学电子笔记229（2009）315使用底层详细STD的动作转换，我们可以通过以下μ-演算公式来表达此属性： true存在一系列动作，其中动作ok（输入i）的发生之后（不一定以连续的方式）是在动作ok（感谢i）的任何发生之前的ok（输入j）。4. 在通常的强公平性假设下，每个请求服务的客户端相应的公式为：[ true*.ok（enteri）.（！ok（explaini））* ] true*.ok（explaini）>true<一旦客户端需要服务，她将被允许访问，前提是任何不包含此操作的循环最终都将离开。5. 每个请求服务的客户最终都会得到服务，而无需进一步假设。它由以下公式表示：[true*.ok（enter i）] mu X. [！ok（explaini）]X正如预期的那样，前四个属性对于非确定性服务器是有效的，而第五个则不是，因为NDetServer不保证对临界区的一般这一点在规范中很清楚，因为NDetServer总是可以忽略客户端，即使它已经请求了服务。另一方面，所有五个属性对于轮询协议都是有效的。5在ACP基于上面介绍的两个例子翻译，我们通过公式化如何在ACP中表达一般范式模型来进行。为了清楚起见，我们限制在层次结构的情况下，其中协作中的组件是经理或员工[8]。然而，员工可以有多个角色，以应对不同的经理。此外，为了便于介绍，我们假设行动决定论，即。任何两个不同的过渡都有不同的作用。通过这种方式，一个转换通过它的标签来识别。员工将其详细行为与全局行为同步，而全局行为由一致性规则管理。管理者的行为也通过一致性规则与员工的行为联系起来。员工的过程代数翻译包含“通知”和“执行”元素。为了阐明这种双重性质，在图6中，我们重复了图3中架构印象的基本片段，并附加了通信操作。流程中针对一个员工的“通知”由处的操作建模。 它保持过程不变，从而通知原始STD状态向一个执行角色转变。此外，雇员由具有相关参数的动作OK来我们需要一个原始的全球性病的细化形式，如图2b所示在这样的角色过程被告知详细STD的当前状态并且16S. Andova等人/理论计算机科学电子笔记229（2009）31s∈ t<$tMs→ s∈ pat！，好吗？在？，好的！作用见图6。 过程交互：（a）顺序，（b）同步。如果断定已经进入了一个新的陷阱（而不改变当前的阶段），它将通过向下一个细化的全局状态迈出一步来存储这个信息：与以前相同的阶段，但是内部陷阱取代了迄今为止进入的陷阱。Paradigm中的员工Z有许多角色，比如R1到Rn。在每个角色中，我们区分相位pij，1≤i≤n，1≤j≤ni。对于每个状态s，我们在ACP中定义一个递归方程如下：Zs=at！（s）.Z s+ a好吗？（a）.Z sJ.s→ s对于雇员Z的角色Ri中的阶段p，我们定义一个递归方程组p[t]，由阶段p中的陷阱t索引。p[t]=πJ在哪里？（s）。p[tJ] +taJoki（a）.p[t]+n{crγ（a，t1，.，t，.，t m）.pJ [triv]|γ：s→a sJp.1→t1pj，.. . ，p→tpJ，...，下午→tmpJ}。因此，详细的STD愿意将其状态信息传达给每个分区;分区仅在？（s）如果s在电流陷阱T的内部陷阱TJ中。 通信功能满足！（个）|在哪里？（s）=τ，其中s∈Z。Atransitions→asJiedete dd e te d et e d e d et ed et e de detedet e d e d et e d e d et e d e det e d e de分区。所以，单身OK？（a）的As应与所有oki（a）匹配，任何相位p[t]，t是p的陷阱，p是Pi的相位，1≤i≤n.在这种情况下，同步是在n+ 1方、详细STD及其n个分区之间。 我们把OK？（一）|ok1（a）| ··· |okn（a）= τ。相位/陷阱过程p[t]的方程的最后一部分，从涉及相位P的陷阱T。 如果一致性规则被触发，则阶段pJ进入分区Pi中。由于没有特定的状态信息，平凡陷阱triv是假设。同步和通信功能将在下面讨论。管理者Z的流程表达式更简单，因为没有与其可能角色的交互。但是，管理员所做的所有转换都应该与特定协作的一致性规则相对于状态s∈Z，我们现在有递归方程Z = n{cr（a，t，...得双曲余切值. ）.ZJ | γ: s a斯杰普t1 pJ，...，ptmpJ}。人EMPEMP经理作用. . .议定书作用员工S. Andova等人/理论计算机科学电子笔记229（2009）317s γ1m s →1→1m→m因此，在协作中，除了经理Z之外，还涉及m名员工 对于要应用的一致性规则γ，Z必须已经到达状态s，而雇员必须已经到达陷阱t1，.，t m。因此，为了沟通18S. Andova等人/理论计算机科学电子笔记229（2009）3函数我们要求同一通信动作的m+1个副本同步，crγ（a，t1，.、t m）|crγ（a，t1，.、t m）| ··· |crγ（a，t1，.，t m）= τ。从上面的一般翻译大纲可以看出，以及如何更复杂的范式模型可以处理。每个协议的多个管理器在同一时间最多具有其中一个管理器的一个cr动作，与来自不同过程的cr动作的相关组合同步，用于不同角色，可能不同地驱动。6结论在本文中，我们通过以下方式链接了协调建模语言Paradigm： 使用mCRL 2工具集的进程代数ACP，能够将Paradigm模型系统地转换为ACP，并支持后续工具验证其正确性。每个Paradigm STD，无论是详细的还是全局的，都被描述为一个递归规范。因此，每个全局和详细STD都有单独的质量标准，包括经理。由一个详细的和相应的全球代表（一个员工和一个角色）组成的组合具有特定的互动，保证了组合动态的一致进展。协调组件的全局动态的相互作用，由一个经理过程驱动，在范式中描述因此，在翻译中，一致性规则由通信功能捕获。因此，Paradigm STD之间的所有交互，无论是显式描述（一致性规则）还是隐式描述，都被忽略了：在过程代数转换之后，由单个通信模式表示，实际上，失去了其体系结构级别的特征。由于各种验证技术可以应用于过程代数规范，通过转换，现在可以分析Paradigm模型的正确性。在我们的实验中，我们使用了mCRL 2工具集，它与ACP进程代数密切相关已使用该工具分析了非确定性协议和轮询协议两个示例的ACP规范。mCRL 2已自动生成完整的状态空间以供进一步检查。我们已经运行了模型检查器，并检查了几个感兴趣的属性。结果证实了Paradigm模型的正确性。注意到，虽然翻译成ACP，引入状态和步骤信息的显式交换本身提供了语义定义。除了通过模型检查其PA转换来确认Paradigm模型的正确性外，模型检查器发现的反例也可以转换回Paradigm设置。生成的迹反驳所考虑的属性，可以在范式的水平上重建。我们在这里介绍了这种逆转换的概述：当映射到PA时，每个Paradigm模型最终都被转换为协作过程CNOH（... 我... ǁ.. . ），如上文所解释的那样指定的组成过程的并行组合。事实上，每个这样的组成过程唯一地对应于一个范式STD。此外，一个这样的STD的动态S. Andova等人/理论计算机科学电子笔记229（2009）319根据该进程的规范采取的相当类似的原子动作序列（），at！（），好！（）.这两种类型的序列的相似性在于保留原始步骤顺序的属性如果是员工薪级，在非细化全局STD的情况下，用通信指示符emp装饰步骤，或者在管理器步骤的情况下用通信指示符man装饰。注意，后面三个通信动作可以吗？（）、emp（）、man（）确实一一对应于范式STD转换;前三个通信动作在？（），at！（），好！（）是额外的，出于技术PA原因需要。因此，一个特定的反例可以追溯到每个STD的类似步骤序列的特定组成，以澄清在原始范式模型中问题发生的位置。在范式语义学的基础[7]中的附录），那么问题发生的原因是可见的。正如预期的那样，理解为什么Paradigm模型 在范式领域，错误或不充分的沟通是反映在错误选择的阶段（在？，at！通信）或陷阱（好吗？，好！通信）或一致性规则（EMP，MAN通信）。最后但并非最不重要的是，我们基于mCRL 2工具集支持的等价性检查进行了一些验证。分支互模拟reduc- tion的实验产生了大量减少的状态空间。特别地，对于非确定性协议，我们得到了一个非常简单的约简结构.然而，由于内部活动的交错，对于轮询协议，仍然相当复杂。在我们未来的工作中，我们将研究如何进一步简化。为此，我们希望制定适当的过程等效性，可能取决于Paradigm其他未来的工作是扩展这里提出的翻译，Paradigm因此，对这种自适应系统的验证应该是直截了当的。引用[1] R.J.艾伦软件体系结构的形式化方法。博士论文，卡内基梅隆大学，1997年。[2] JCM Baeten和W.P. Weijland。进程代数CUP，1990年。[3] M.A. Barbosa 和 L.S. 巴 博 萨 一 种 用 于 软 件 组 件 动 态 互 连 的 协 调 器 。 In G. Boella 等 人 ， 编 辑 ，Proc.Coordination2006和MTCoord 2006，第49-61页。ENTCS 181，2007年。[4] J.A. Bergstra，A.Ponse和S.A.斯莫尔卡过程代数手册。Elsevier，2001年。[5] 布拉德菲尔德和C.斯特灵模态μ结石。《模态逻辑手册》，第721-7