Q-自动机：并发组件的质量建模

理论计算机科学电子笔记175（2007）153-167www.elsevier.com/locate/entcsQ-自动机：并发组件的资源使用建模1汤姆Chothia2CWI，Kruislaan 413，阿姆斯特丹，荷兰3号码头LIACS，莱顿大学，邮政信箱9512，NL-2300 RA莱顿，荷兰摘要Q-自动机被引入到基于构件的软件的质量方面的模型。我们提出Q-代数作为一个通用的框架，使我们能够结合和选择质量值。 这些值被添加到自动机的转换中，自动机代表组件或通道。这些自动机可以由一个产品结构组成，产生一个更复杂的Q-自动机，标记有其组件的组合成本。因此，我们建立组合的服务质量的基础上代数的质量属性与自动机表示的过程。保留字：Q-Automata，组件系统，并发，服务质量，组合性1引言本文介绍了Q-自动机，这是设计的信任和基于组件的软件质量方面的模型。服务质量（QoS）方面关注非功能属性，如可用性，响应时间，内存使用等。在约束半环[10，15]的工作之后，我们提出了一个一般框架，用于一系列信任和质量值，我们称之为Q-代数。这些代数定义了一个质量值的框架，可以与许多类型的自动机或演算相结合为了使我们的系统适合于我们期望建模的各种应用程序，并使我们的系统更容易理解，我们选择将我们的工作基于自动机。这些提供了一个具体的、直观清晰的计算模型，以及分析行为的结构方法1由ITEA项目Trust4All2电子邮件：Tom. cwi.nl3电子邮件地址：kleijn@liacs.nl1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.03.009154T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153组件及其组成。 也有大量的理论和实现工作，使用自动机表示组件的分布式和反应式系统，这可能是有用的。组件将以与其他工作类似的方式由自动机表示[7，14，17，20，21]，但我们的自动机的转换将具有额外的成本标签，以指示采取该转换对系统质量属性的影响。由此产生的Q-自动机可以组成使用产品的构造，导致一个新的（更高级别的）Q-自动机。大多数自动机模型不区分两个动作的交错和它们可能的并发发生，然而在这里提出的模型中，并发组件可能在通信中）。这是因为，对于多线程程序，应用程序的资源使用可能会非常不同，这取决于最小的抽象单元是同时发生还是一个接一个地发生。例如，给定两个转换，它们都“消耗”一定量的带宽，以kbit/s为单位测量，同时运行这两个转换将需要（或“消耗”）两个单独成本的总和，而一个接一个地运行它们将仅消耗两个单独成本中的最大值。另一方面，时间成本将按顺序求和，但不是同时求和，我们可以选择通过同时和按顺序求和来建模内存分配成本。半环已经被提出作为用于构成和关联QoS参数的框架[10，15，19]。假设用于管理QoS约束的适当抽象级别和用于实际QoS值的度量，约束半环提供具有两个操作的代数结构，一个操作用于在值之间进行选择，另一个操作用于将值组合成新的QoS值。因此，QoS值的组合性在这种方法中是有保证的。我们将约束半环推广到Q-代数上，使Q-代数多了一个组合QoS值的算子。通过这种方式，既可以合并按顺序发生的成本，也可以合并同时发生的成本此外，这种不同实现的成本可以在算法内进行比较。一般来说，QoS值是元组，每个组件代表一个特定的方面：条目可以是不同的种类（数字表示延迟，服务的访问权限，内存使用等）。并且，与约束半环的情况一样，有限个Q-代数可以组合成值的元组，因为Q-代数的乘积也是Q-代数。我们认为自动机的QoS值作为额外的标签添加到individual转换，指示其使用的资源时，执行。乘积构造被定义为将所得的Q-自动机组合成更复杂的Q-自动机。该产品可以同时执行原始自动机的任何动作组合，并且可以同步匹配的输入和输出动作，以成为内部动作。这个最通用的产品适应组件之间的许多不同类型的通信;为了实施一种特定类型的通信，例如要求每个通信信道具有单个端点，可以应用限制运算符来移除某些转换。组件的转换组合成新的转换，T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153155都是从其组成转变的成本中计算出来的成本域的代数结构使得可以比较成本，计算Q-自动机中的转换路径的成本（计算），以及组合复合自动机中同时进行的多个转换的成本。本文的贡献是：• 一种新的组合自动机模型，其中包括一个概念的并发转换建模并发，通信组件，• 一个扩展的成本代数来计算不同的成本组合，• 将自动机与代数相结合，得到Q-自动机的框架，• 并展示了如何在这个框架中对普通组件和不同类型的加权自动机在每个转换上都有一个简单的权重或成本，并且自计算机科学早期以来一直被广泛研究[16，26]。这些自动机已被证明具有实际应用，其中一个例子是Mohri等人的工作关于语音处理[23，24]。布赫霍尔茨和肯珀[12]描述了一种模型检查这些自动机的类的方法，这些自动机只使用正权重。我们在这里提出的工作通过使用Q-代数来提供成本，从加权自动机中分离出来;这使我们能够定义组件资源使用的真正时间自动机模型用代表它们所花费的时间的成本来标记转换[1]。概率值也与自动机很好地结合在一起，例如Segala[27]增加了简单的概率转换，最近，拜尔和沃尔夫着眼于马尔可夫风格的概率时间延迟作为约束自动机的标签[6]。我们希望这些成本中至少有一部分可以归入我们的成本代数框架。定价或加权时间自动机[2，9]使用时钟对时间进行建模，并对状态和转换进行每次转换的成本在每次转换时支付，而每个状态的成本在自动机在该状态中花费的每个时间单位支付一次 这提供了一个成本和时间的表达模型，在许多情况下，这是不可判定的[11]。我们提出的自动机模型类似于团队自动机[7，8，17]以及I/O自动机[20，21]和接口自动机[14]等相关模型许多系统试图通过将半环成本添加到过程演算来模拟计算的定量方面，[5，15，25]，这些并不区分成本的并发和顺序组成。本文旨在首次介绍我们的概念和想法，因此，由于篇幅有限，它相对非正式，仅对初步结果进行了初步概述。在下一节中，我们将介绍我们的成本代数，然后在第3节中，我们将定义我们的自动机。第4节讨论了限制和通道通信，其中显示了自动机之间的同步通信方式如何用于对各种通道进行建模。最后，在最后的第5节中，我们简要讨论了如何作为未来的工作，可能的无限大成本156T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153可以在有限时间内计算出一个自动机的成本，以及两个自动机的乘积的最大成本如何受到它们各自成本的限制2Q-代数为了以标准方式计算和分析QoS值，我们开发了一个通用框架，如De Nicola等人的方法。[15]。首先，我们回顾一下约束半环的概念：定义2.1一个约束半环是一个结构R=（C，n，n，0，1），其中C是一个集合，0，1∈C，n和n是C上的二元运算，使得：— n是交换的、结合的、幂等的，并且具有单位元0— 是关联的，标识为1— λ分布在λ上，0作为吸收（零）元素注意，对于如上所述的约束半环（或简称为c-半环），运算a在C上导出偏序≤，定义为a≤b当且仅当aa≤b =b。此外，两个元素在≤方面是可比较的，当且仅当对这些元素应用ε产生一个（较大的w.r.t.（二）两者。实际上，它总是产生它所应用的元素的最小上界。约束半环可用于组合QoS值，其中给定一个成本为c1的动作和另一个成本为c2的动作，那么这两个动作的成本加起来是c1c2，而返回c1和c2的最小上界。0元素，作为标识符，是最小可能的成本值，1元素，作为标识符，是中性成本值。举几个例子：- （最短）时间：（R+∞ {∞}，min， +，∞，0）— 带宽：（N{∞}，min，max，∞， 0）— 数据加密：（{true，false}，true，false，true）— 访问控制：（2U，U，U，U，U），其中U是所有用户的集合，2U是所有用户当只有一种方法组合质量值时，约束半环工作得很好。我们可以使用这些值来表示方法调用的成本，一系列减少步骤或执行整个程序的成本。当处理多个并发进程时，这些步骤可以顺序地或并行地发生例如，两个进程都需要每秒一定数量的CPU周期，当它们同时运行时，每秒所需的周期数将比一个接一个运行时更高。 我们可以通过添加一个新的乘法运算符来模拟这些不同的组合值的方式：定义2.2一个Q-代数是一个结构R=（C，N，N，N，0，1）使得RN=（C，N，N，0，1）和RN=（C，N，N，0，1）是c-半环。C被称为domainR.T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153157c2运算符用于同时合并两个值，c1c2是c1和c2同时的成本。c2运算符按顺序组合值;c1<$c2是c1后跟c2的成本。同时或按顺序组合成本不会影响最小或中性成本要素，因此两个操作共享其身份。和前面一样，使用R2在值之间进行选择。举例来说— （最短）时间：（R+∞ {∞}，min， +，max，∞，0）— 带宽：（N{∞}，min，max， +，∞，0）两个Q-代数的乘积按分量定义：定义2.3给定两个Q-代数R1=（C1，R1，R1，R1，R1，01，11）和R2=（C2，R2，R2，R2，R2，02，12），它们的乘积R=（C，R2，R2，R2，02，12）是Q-代数，定义如下：- C=C1×C2，- （c1，c2）<$（cJ，cJ）=（c1<$1cJ，c2<$2cJ），1 2 1 2- （c1，c2）<$（cJ，cJ）=（c1<$1cJ，c2<$2cJ），1 2 1 2- （c1，c2）（CJ，CJ）=（c11CJ，c22CJ），1 2 1 2- 0=（01，02），- 1=（11，12）。很容易看出两个Q-代数的乘积确实是一个Q-代数。有时，两个不同Q-代数的乘积的元素表示相同的资源。当我们取这些代数的乘积时，我们不想复制这些条目，而是将它们组合起来。这可以通过使用成员是标记元素的元组的Q-代数来实现。下面的定义给代数添加了标号，当计算两个（标号的）Q-代数的乘积时，这些标号可以 用 于 比 较 。 这 些 定 义 允 许 我 们 写 这 样 的 值 ： （ power ： 2 ， cpu ： 10 ） 和（power：7，errors：1），而不是（2，10）和（7，1），并且它们的乘积是（power：9，cpu：10，errors：1）而不是（2，10，7，1）。这些乘积只有在同标号代数上的运算相同时才被定义。定义2.4设n≥1，且对每个1≤i≤n，Ri=（Ci，i，i，i，0i，1i）是一个Q代数 我们将不同的标签li与每个Ri相关联（如果i j，则lii=lj）。则R =（C，n，n，n，0，1）是（l1：R1）上的标号Q-代数，.，（ln：Rn）），如果— C =（{l1}×C1）×. ×（{l n}×C n）;因此每个元素c∈C是形式c =（l1：c1，.，ln：c n），其中对于所有的1 ≤i≤n，c i ∈ C i，- 0 =（11：01，.，1 n：0n），- 1 =（11：11，.，1 n：1n），-（l1：c1，. .. .. ，l n：（c n<$ncJ）），1n1n-（l1：c1，. .. .. ，l n：（c n<$ncJ）），1n1n- （l1：c1，. .. ..，l n：（c n<$ncJ））。1n1n一个标号Q-代数也是一个Q-代数。给定如上所述的标号Q-代数R，其标号集合{l1，.，l n}由标号（R）表示。我们使用符号projl，其中l∈labels（R），从R中提取由标签标识的Q-代数l，例如projli（R）=Ri。 注意，排序是任意的;直到基础Q-代数和它们的标号，标号Q-代数如刚才定义的158T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153是独一无二的.因此，我们将确定任意两个n维标号Q-代数brasRandd R，其中n个标号s（R） =标号s（R）anddprojl （R） =projl （R），对于所有标号l∈标号（R）.我们有两个选择，一个是让Q-alge带来R和R，无论何时都是一致的对于nlabell∈label s（R）∈ label s（R）的任意余项，pro j l（R）= proj l（R）。定义2. 5LetRanddR是两个相容的标号Q-代数 则R和R的一个简单的预处理，由RdaR表示，是一个简单的Q-代数带标号s（R）的代数带标号s（R），它是一个由prol（R d a R）= pro l（R）i f l∈LABELS（R）和DPROJL（RDaR）=projl（R）ifl∈label s（R）定义的代数带标号s（R）的代数带标号s（R）的代数带。观察到RDaRaboveis a labelledQ-algebra. 此外，还证明了当取两个相容的标号Q-代数的乘积时，具有相同标号的基础Q-代数是不重复的.最后，应该注意的是，（未标记的）QoS代数的普通乘积可以被视为标记乘积的特殊情况，即通过给每个代数自己的标签。在本文的其余部分，我们将只处理标记的Q-代数，即使没有明确提到标签。3Q-自动机在本节中，我们介绍Q-自动机。这些包括一个初始化的标记的过渡系统连同一个（标记）Q-代数，以指定每个过渡的成本。注意，每个转换都标记了一个动作的多重集合，作为动作同时和多次出现的表示：集合X上的多重集合是一个函数m：X→N，X上所有多重集合的集合表示为M（X）。对于X上的两个多重集m1和m2，它们的和m1+m2是X上的多重集，定义为：（m1+m2）（x）=m1（x）+m2（x），对所有x∈X。定义3.1 Q-自动机是一个结构P=S，t，A，R，T，其中：— S是一组状态，— t∈S是它的初始状态，— A是一组（有限的）动作名称，— R=（C，n，n，n，0，1）是一个带标号的QoS代数，其代价域为C，— TS×M（Act）×C×S是变迁集P的动作集合，写作Act，是以以下方式从动作名称集合A导出的：每个名称a∈A可以作为输入动作出现（记为a？），输出操作（表示为a！）或者作为内部动作（也由a表示）。因此，我们得到AO={a！：a∈A}，P的输出动作集，AI={a？：a∈A}，P的输入作用集，Aτ=A，P的内部作用集。假设集合AO、AI和Aτ是成对不相交的。最后，我们设置Act=AO<$AI<$Aτ。Q-自动机的（有限）计算以标准方式定义。定义3.2设P是一个Q-自动机，如定义3.1所述。从状态s0 ∈ S开始的计算（长度n≥ 0）是一个序列（s0，m1，c1，s1），.、T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）1531592（sn−1，mn，cn，sn）且（si，mi，ci，si+1）∈T对所有0≤i≤n− 1。如果n=0，则计算是空序列。基于Q-代数和转换的成本，我们可以计算每次计算的成本。定义3.3设γ =（s0，m1，c1，s1），.，（s n−1，m n，c n，s n）是定义3.2中规定的计算。则γ的成本是1，如果n = 0且c1≠... 如果n≥1，则n= n。因此，计算（一系列转换）的成本是使用“顺序乘法”运算符来计算的。请注意，为了比较不同计算的成本，可以使用加法（选择）运算，因为它产生给定值的最小上限。“Concurrent multiplication” 这个乘积自动机的Q-代数是它的分量的Q-代数的乘积。它的状态空间是它的组件的状态空间的笛卡尔积，它的转换是组件转换的组合与传统的应用于I/O自动机和接口自动机的合成及其在团队自动机中的推广的同步乘积相比，Q-自动机的乘积不是基于单个动作的组合执行（同步），而是允许多个动作同时发生此外，类似于CCS [22]或CSP [18]的通信设置，输入和输出动作对a？和一个！可以同步（通信）并且一起成为内部动作A。产品自动机具有其组件转换的所有可能组合。因此，当处于特定状态组合中的两个组件可以执行匹配的输入和输出动作时，它们的产品将从该组合状态具有通信转换，但也具有这两个动作分离且不通信的转换（因此仍然可用于与其他组件通信）。此外，只有一个组件处于活动状态（具有输入或输出操作）的转换也将出现在产品中。对于作为组件转换的组合获得的每个新转换在乘积自动机的形式定义中，我们使用了一个辅助函数sync，它反过来使用了一个对多个动作集的关系，使得左边的一对等于右边的一对，除了一个多集中的一个名字上的一个输入。并且在另一个多集中的相同名称的一个输出已被删除，并且在该名称上的通信已被添加。定义3.4设A是一组动作名称，Act是与之相关的一组动作名称。如定义3.1中所定义的，并且 m1和 m2是Act上的两个多重集。则（ m1， m2）<$（MJ，MJ）如果存在a∈A使得：1 2-m1 （a？）≥1且m2（a！）≥1-MJ （a）=m1（a）+1和MJ（a？）=m1（a？）-1，1 1-mJ （a！）=m2（a！） -1，160T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）1531122P1：{stdout？}联系我们m：6，c：1 m：-6，c：5P2：{process}m：10，{stdout！}m：1，PP：{process}m：10，c：25{stdout！}m：1，c：1{pt}− 6.5{ps，pt}{s！，s？}{s}七二{s？}6.1{stdout？}m：6，c：14,30{s？}6.1{pt}−6.57,2{print}m：−6，c：5{process}m：10，c：25{stdout！}m：1，c：1{ps，s？}{s！，pt}m：16，c：26 m：-5，c：6Fig. 1. 简单自动机及其乘积— 并且对于所有其他动作b∈Act，MJ（b）=m1（b）和MJ（b）=m2（b）。1 2或者如果（m2，m1）<$（MJ，MJ）如上所述。2 1设是的自反传递闭包。然后sync（m1，m2）={MJ+MJ：对于所有MJ，MJ使得（m1，m2）≠（MJ，MJ）}。1 2 1 2 1 2因此sync（m，mJ）是所有多重集的集合，可以通过添加m和MJ之间的任何可能的通信组合。定义3.5设P1=S1，t1，A1，R1，T1和P2=S2，t2，A2，R2，T2是两个Q-自动机，使得R1和R2是相容的.则它们的乘积，记为P1<$P2，是Q-自动机，定义为P1<$P2=<$S，t，A，R，T<$，其中- S=S1×S2，- t=（t1，t2），- A=A1<$A2，— R=R1DaR2，— T=T新接头T新接头T其中：1 2• Tnew={（（s，t），m，c，（sJ，t））：（s，m，c，sJ）∈T1andt∈S2}，• T新={（（s，t），m，c，（s，tJ））：s∈S1和（t，m，c，tJ）∈T2}，并且T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153161• Tjoint={（（s，t），m，c，（SJ，TJ））：<$（s，m1，c1，SJ）∈T1，（t，m2，c2，TJ）∈T2使得m∈sync（m1，m2）且c=c1<$c2}.作为Q-自动机及其乘积的一个例子，我们给出了一个简单的系统，162T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153图1.自动机P1监听通道stdout，然后打印到屏幕上（一个内部动作）.自动机P2进行一些内部处理，然后通过标准输出通道发送一条消息.这些操作中的每一个都分配了一定量的内存，并需要一定量的CPU。P1自动机在收到请求时分配它所需的内存，并在打印时释放此内存P1和P2的乘积也显示在图1中，为了使其更具可读性，我们删除了标签并缩短了图中心的动作名称。自动机P1和P2仍然可以在通道stdout上接收来自其他自动机的消息. 这是应该的;所有组件都应该能够打印到屏幕上，而不仅仅是要添加的第一个组件。产品自动机包含并发操作，我们看到，如果P1收到来自某个第三方的调用，那么P1和P2可能同时处理和打印。这是特别有趣的，因为它产生了整个系统中CPU开销最大的转换，因此在测试这些自动机的实现时可能是一个很好的测试用例。我们还注意到，即使自动机P1在通道stdout上发送消息，同时P2在stdout上接收消息，也不自动意味着P1和P2已经通信。实际上，P1可以在信道stdout上从某个其他组件接收消息，而P2通过同一信道向某个其他组件发送消息这是{stdout}和{stdout？，stdout！}动作集，并证明了Q-自动机的乘积是结合的。4限制与渠道在某些情况下，我们可能希望对自动机施加更严格的通信模型，例如，我们可能希望要求只有一个自动机可以在给定的信道上接收，或者我们可能希望测试我们的自动机，因为我们知道没有其他自动机会在某个信道上侦听。我们可以通过阻塞所有涉及给定（内部、输入或输出）操作的转换来实现这一点。定义4.1设P=<$S，t，A，R，T<$是一个Q-自动机，设α∈AO<$AI<$Aτ是P的一个动作。 则P\α，P关于 α的限制，是Q-自动机<$S，t，A，R，TJ<$TJ={（s，m，c，sJ）：（s，m，c，sJ）∈TP且m（α）=P P0}。 对于一组动作X ={α1，α2，...， α n}，我们将P\X定义为（. （P\α1）\α2）.n）。图2中给出了限制的示例（未绘制不可达状态第一个乘积自动机是受标准输出限制的！输出，以模拟只有P1在stdout通道上接收的情况。因此，P2第二个例子限制了stdout的输入和输出，并演示了“封闭”产品P 1和P 2如何这导致一个小的自动机，可能更有用的测试目的。T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153163丙：3{src？}C5颈7{ask！}{src？}C5颈7{ask！}SRCSK{process}m：10，联系我们{print}m：P1 P2\stdout！：{process}m：10，c：25{stdout？}m：6，c：1{pt}−6.5{ps，pt}4,30{s？}1、1个{pt}五，五{stdout？}6.1{stdout}7，2{print}m：−6，c：5{process}m：10，c：25{ps，s？}男：16，女：26P1 P2\{stdout！，stdout？}：P1：图二. 限制的产品P2：{asrc！}C1{asrc！}C2{ask？}C3{ask？}C4C1：{a ？，a！}C5C6c6c6图三. 自动机作为通道{src？}C5C2：{ask！}164T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153信道通信自动机的产品构造强制同步通信：输入和输出只能通信并成为内部动作，如果两者都T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153165同时发生。此外，仅一个输入可以与仅一个输出同步。为了对更广泛的通信风格（包括异步，有损和多播）进行建模，我们显式地将通道建模为自动机（与约束自动机类似[3]）。组件自动机将写入通道的以及在具有动作Ask？的A的接收器上的其它输入。在这里，src和sk是不同的名称，仅通过命名约定相关联，因此产品操作不允许它们彼此同步。为了使通信发生，组件必须使用一个表示在它们之间运行的通道的自动机。这样的通道自动机将监听它所代表的通道的源端，并在其接收端发送：一个SK！然后，这两个组件可以通过该通道进行通信。大多数信道类型具有一个源端和一个接收端，但是一些信道类型（诸如可以用于同步两个动作的同步漏极）具有两个源端或两个接收端，并且多播信道可以具有任意数量的接收端。通道和组件自动机如图3所示。组件自动机P1在通道a的源上重复发送，成本为c1或c2。另一个组件自动机P2可以在信道a的接收器上以成本c3或以另一种方式以成本c4进行接收。自动机C1、C2和C3定义了三种类型的通道，组件可以使用它们进行通信。通道自动机C1有一个单一的转换，它在通道的源上接收，同时在其接收器上发送，即， 该自动机定义了同步通信信道。通道自动机C2首先在a的源端接收，然后，一段时间后，在其接收端发送。 因此，这定义了一个异步通道，其缓冲器足够大，可以容纳一条消息。最后，通道自动机C3定义了一个有损的、两层的、异步通道。丢失消息的可能性由τ动作表示，τ动作允许在信道的源上接收到的消息不被转发到其接收器。作为使用这些通道之一的示例，图4显示了产品P1C1P2的封闭版本。这表示使用通道C1的两个分量P1和P2。双内部动作{asrc，ask}表示通过a的通信。根据组件P1和P2如何执行其通信，存在四种可能的组合。这些不同的可能性产生不同的成本。（开放）产品P1<$C1<$P2将具有标签为{asrc？，ask！}，成本为C5。这个产品自动机也可以执行src的操作！和一个sk？，从而使得组件可以使用稍后可能添加的某个其他信道进行通信。此外，独立的操作可能会同时发生，从而向产品添加更多的转换。一般来说，为乘积自动机定义的大量转换是必要的，以避免然而，通过自动地将通信限制为仅一种通信是可能的。166T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153{ask，asrc}c2 c5 c4{ask，asrc}{ask，asrc}c1 c5 c3c1 c5 c4{ask，asrc}c2 c5 c3见图4。 P1<$C1<$P2\（输入输出）对产品进行限制。作为示例，我们可以考虑其中每个信道具有唯一端点的系统，即，只有一个组件可以从信道的接收器读取，并且只有一个组件可以向信道的源写入。正如我们所知，输入和输出是唯一的，我们可以关闭一个输入和输出动作，一旦它有机会同步。这是通过对产品定义的以下细化来实现的：定义4.2给定Q-自动机P1和P2，它们的点对点乘积是Q-自动机P1<$pP2= P1<$P2\（{a！：<$（s，m，c，t）∈（TP1<$TP2）使得m（a？）≥1}{\fnSimHei\bord1\shad1\pos（200，288）}：<$（s，m，c，t）∈（TP1<$TP2）使得m（a！）≥1}当对这样的系统建模时，使用这种乘积的定义会自动删除许多我们知道不会同步成为通信的输入和输出，从而使我们的状态空间更小，更容易进行模型检查。限制运算符也可以用来为其他类型的通信定义类似的限制性乘积运算符。移动渠道移动信道，例如在MoCha移动信道通信包[4]中实现的那些信道在这种设置中，组件具有许多唯一的端口，它们可以在这些端口上发送和接收消息，并且信道链接这些端口以允许进行通信。我们可以使用自动机对这些系统进行建模，以模拟组件和通道，如上一小节所述，并且我们可以通过允许通道在链接不同端的状态之间移动来T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153167一个！走！一{a？，b！C{move？}C2动？C2{a？，c！C图五. 在B和C点例如，在图5中，组件B和C监听端口b和c上的输入，另一个组件A在端口a上发送消息，也可能发送移动信号。这些组件中的每一个都将由合适的自动机表示，为了简单起见，我们在图中抽象出它们的细节。图中央的自动机表示一个通道，该通道通过将A的输出端口链接到B的输入端口，使用带有标签{a？，b！}。这执行与上一节中描述的同步通道相同的功能，但是该通道也可以从组件A接收移动信号，此时它将改变为将a上的输出连接到c上的输入，从而将通道端从组件B移动到组件C。通过这种方式，我们可以定义各种各样的通道，这些通道可以在任意数量的预定义端口之间移动它们的端点5结论和进一步工作我们已经提出了一个自动机模型，其中的行动与信任或质量值的标签。我们已经定义了Q-代数作为这些值的一般模型，并且我们已经展示了这些自动机和转换上的值如何有意义地组合在一起。Q-自动机被认为是Trust 4All项目中开发的分析方法的一部分。这是一个ITEA项目，旨在为“可信”组件开发一个编程环境，这些组件将提供有关其资源使用情况的信息。我们希望这里提出的自动机模型将适合于模型检查这些组件，最终我们将能够自动生成测试数据。我们对自动机的最大可能成本以及导致该成本的计算特别感兴趣。一般来说，在一个给定的状态下，可能有无限多的计算开始，因此，为了找到最大值，需要应用无穷多的成本。然而，在有限状态集合的情况下，c？ Cb？B168T. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153无限数量的计算只能通过循环产生。单个循环可能会给计算增加一个固定的成本（导致潜在的无限成本），或者可能会设置一个新的水平成本，或者可能根本没有效果。因此，绕一个循环的一次遍历就足以告诉你无限次遍历该循环的结果是什么。这意味着我们可以在有限时间内计算出最大成本，即使成本是无限的。我们还希望开发出从产品的各个部件预测产品性能的方法例如，我们期望两个自动机的最大成本的并发和顺序组合的最小上界是其产品的最大成本的上界，即，如果 P1 和 P2 具 有 最 大 成 本 c1 和 c2 ， 则 P1<$P2 的 最 大 成 本 小 于 或 等 于 （ c1<$c2 ）<$（c1<$c2）。Maude [13]是一种基于等式和重写逻辑的高级语言。它提供了一个简单的框架，在其中实现Q-自动机和模型检查一些基本属性4。 我们为每种成本定义一个Maude模，对于每个自动机。成本模块包括成本、成本和成本的等式定义。我们在Maude中定义自动机，使用构造函数给出状态，然后使用rl命令定义这些状态之间的重写规则。然后，我们可以使用Maude的搜索命令检查基于成本的属性例如，我们可以检查给定程序分配的内存从未超过100k。我们将继续这项开发工作，目的是使我们的原型更加强大和用户友好。确认我们非常感谢当地的同事在这个项目中进行了许多富有成效的讨论，特别是FarhadArbab 、 Frank de Boer 、 Marcello Bonsangue 、 Andries Stam 和 FrankAtanassow。我们也感谢裁判们的批评。引用[1] R. Alzheimer和D. L.迪尔 时间自动机理论。 Theor. Comput. Sci. ，126（2）：183[2] R. Alberr，S.拉托雷和G·J·帕帕斯加权时间自动机中的最优路径。Theor. Comput. Sci. ，318（3）：297[3] F.阿巴布角Baier，J.J.M. M. Rutten和M. Sirjani. Reo中组件连接器的约束自动机建模：（扩展抽象）。电子笔记理论Comput. Sci. ，97：25[4] F. Arbab，F. de Boer，J. Guillen Scholten，and M.你好Mocha：基于移动通道的中间件。COMPSAC，第667-673页，2002年[5] B.阿齐兹基于半环的移动系统定量分析。电子笔记理论Comput. Sci. ，157：3[6] C. Baier V.沃尔夫随机 推理 关于基于通道的组件连接器。在Coordination 2006，Volume 4038 ofLectures Notes in Computer Science，pages 14.本文所述自动机实例的Maude代码可在以下网址在线获得http://homepages.cwi.nl/www.example.comT. Chothia，J.Kleijn/Electronic Notes in Theoretical Computer Science 175（2007）153169[7] M.H. Ter Beek，C.A.埃利斯，H.C.M. Kleijn和G.罗森伯格群件系统中团队自动机的同步。CSCW - TheJournal of Collaborative Computing，12（1）：21[8] M.H.特尔·贝克和H.C.M.克莱恩满足组合性的团队自动机。在Formal Methods[9] G. Behrmann，A. Fehnker，T. Hune，K. Guldstrand Larsen，P. Pettersson，J. Romijn，and F.W.凡德拉格定价时间自动机的最小成本可达性。 在第四届国际混合系统研讨会，计算机科学讲义第2034卷，第147[10] S.比斯塔雷利大学Montanari和F.罗西基于半环的约束满足与优化。J. of the ACM，44（2）：201[11]P. Bouyer，T. Brihaye和N.马基 改进加权时间自动机的不可判定性结果。信息处理。Lett. ，98（5）：188[12] P. Buchholz和P. Kemper。一类加权自动机的模型检验。CoRR，cs.LO/0304021，2003年。[13] M. Clavel，F. 杜兰，S。 Eker，P. Lincoln，N. 我的天啊，J。 M e s e gu err和DC. Tal cottt. 这是一个2。0系统。在重写技术和应用2003年，在计算机科学讲义，第76-87页[14] L. de Alfaro和T. A.亨辛格接口自动机。在第九届软件工程基础年度研讨会论文集，第109-120页。ACMPress，2001.[15] R. De Nicola ， G. 法 拉 利 ， 美 国 蒙 塔 纳 里 河 Pugliese 和 E. 托 斯 托 QoS 感 知 应 用 程 序 的 进 程 演 算 。 在Coordination 2005，卷3454的Lectures Notes in Computer Science，第33-48页[16] S.艾伦伯格 自动机、语言和机器 学术出版社，一九七六年[17] C.A.埃利斯 群件系统的团队自动机。 在GROUP ACM Press，1997.[18] C.A.R. 霍尔通信顺序进程。Commun. ACM，26（1）：100 -106，1983.[19] W. Kuich和A.萨洛马 半环，自动机，语言。 Springer-Verlag，1986.[20] N.A.林奇 分布式算法 摩根·考夫曼，1996年。[21] N.A.林奇和MR塔特尔输入/输出自动机简介。 在CWI-Quarterly，第2（3）卷，第219-246页[22] R.米尔纳 通信系统的微积分。 Springer-Verlag，1982.