随机对象图文法的模型分析和性能评估

理论计算机科学电子笔记184（2007）151-170www.elsevier.com/locate/entcs基于随机对象的图文法奥多里科湾1Fernando L. 多蒂Pontif'apriciaUniversidadeCato'licadoRioGrandedoSul，PortoAlegre-Brazil电子邮件：{omendizabal，fldotti}@ inf.pucrs.br莱拉·里贝罗2Universidade Federal do Rio Grande do Sul，Porto Alegre-BrazilEmail：leila@inf.ufrgs.br摘要基于对象的图语法（OBGG）是一种形式化的可视化语言，适用于基于消息传递的实时分布式系统。目前支持OBGG模型的模型检查，并开发了一系列案例研究。然而，在许多情况下，人们必须评估非功能方面，如所考虑的系统的可用性和性能。在这种情况下，需要对系统进行随机分析。本文是对OBGG模型随机分析的首次贡献。OBGG模型的发生率与规则相关联的随机自动元网络（SAN）。SAN是一种马尔可夫链等价形式主义，其优点是在表示和紧凑的数学解决方案方面具有模块性，允许分析具有更大状态空间的模型。保留字：基于对象的图文法，异步系统，随机自动机网络1介绍在复杂系统的开发过程中，一个非常重要的方面是尽可能早地评估系统的功能和非功能属性的能力。这种能力通常会带来重要的节省，以及最终系统质量分布式系统的开发被认为是一项艰巨的任务。除了处理并发系统固有的复杂性之外，开发人员还必须考虑分布方面。在这种情况下，通信延迟以及节点和服务的可用性等成为需要考虑的重要方面，这可能导致应用程序的成功与否1作者部分由HP-Brasil/PUCRS协议赞助。2作者部分由CNPq赞助，项目PLC101571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.03.020152O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151基于对象的图文法（OBGG）[5]是一种图形形式化规范语言，适用于异步分布式系统的规范。用这种形式主义定义的模型可以使用验证（通过模型检查）进行分析[4，12]。虽然模型检查是一种重要的分析方法，但在许多情况下，必须在开发过程中尽早评估非功能性方面，如所考虑系统的可用性和性能此外，在许多类别的应用中，不可能确保某些特性。在这种情况下，重要的是能够将概率与推理中的属性的满足与否相关联。随机过程允许人们对不同现象的相互作用进行建模，每个现象都由不同的概率分布描述在各种随机过程中，马尔可夫链[13]已被广泛研究并用于计算机科学和工程。马尔可夫链是一种离散状态随机过程，可以是连续的，也可以是离散的，具有无记忆性。这个属性确保了到下一个状态的转换只依赖于系统的当前状态，而不依赖于之前的状态。使用指数和几何概率分布相关联的转移，确保了无记忆的prop-连续和离散时间马尔可夫链，分别。马尔可夫链的解决方案导致链的每个状态的概率，考虑稳定状态的情况。由于马尔可夫链是一种带有概率分布的转移系统，因此它们被用作各种方法的基础模型。这是随机Petri网（SPN）的情况，其中网的可达图是用相关转移的概率分布注释的转移系统[1]。类似地，对于随机过程演算，其中过渡系统由一些过程演算描述，例如π演算[11]。文[7]给出了图变换系统随机分析的第一步。在这篇文章中，作者将（指数）概率分布与规则联系起来。由此，从图文法获得的转移系统产生了可以用现有工具分析的连续时间马尔可夫链。在本文中，我们提出了一种方法的OBGG模型的随机分析。OBGG是图语法的一种受限形式，因此[7] 也适用于OBGG。然而，由于状态空间爆炸的问题，我们避免使用马尔可夫链，更喜欢一个等效的方法，具有更好的可扩展性。随机自动机网络（SAN）[10]是一种马尔可夫链等价形式主义，在表示和紧凑的数学解决方案方面具有模块化的优势，如果与马尔可夫链[6]相比，则允许分析具有更大状态空间的模型。一旦模型在SAN中表示，就可以使用PEPS工具（并行系统的性能评估）[9]导出与感兴趣状态相关的概率。本文的主要贡献是：（i）提出了一种随机扩张的方法，O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151153sion到OBGG;以及（ii）扩展OBGG到SAN的翻译，导致OBGG的随机语义。本文的组织如下：下一节介绍了OBGG和运行的例子-令牌环网络的模型。第三部分介绍了SAN的主要特点。在第4节中提出了OBGG的扩展。第5节讨论了从OBGG到SAN的转换。第6节分析了例子，最后的评论在第7节。2基于对象的图文法在本文中，我们考虑具有以下特征的基于对象的系统：• 一个系统是由许多对象组成的。 每个对象的状态定义为： 它的属性，可以是抽象数据类型的元素或对其他对象的引用。一个对象不能读取或修改其他对象的属性• 对象是类的实例，包含属于该类的对象的属性和行为的• 对象是通过异步消息传递进行通信的自治实体基于对象的系统的规范是通过（基于对象的）图形语法完成的。我们将介绍用于指定基于对象的系统的图形和规则。这些图被称为基于对象的图，并在[5]中介绍。基于对象的图语法中的每个图可以由图1（a）中所示的顶点和边的实例组成。顶点表示类和抽象数据类型，而类的消息和属性被建模为超边（具有一个目标和许多源顶点的边）。我们为这些图表定义了一个独特的图形表示，以增加规范的可读性这种表示如图1（b）所示抽象数据类型的元素被允许作为类的属性和/或消息的参数请注意，图1中的图只定义了可能出现在规范中的顶点和边的类型，并没有强制实体或消息具有属性。例如，这个图指定，如果一个类有属性，它们必须是ADT类型或Class类型。规则将表示对象对收到消息的反应。基于对象的图形语法的规则包括：• 左手边L：描述了在当前状态中必须存在的项目，以使得能够应用规则。规则左侧的限制是：· 必须只有一个消息顶点，称为触发消息（这是此规则处理的消息）。· 只有作为触发消息目标的对象的属性才可能出现。· ADT类型的项可以是变量，其将在154O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151PAR1PAR2ADT（一）（b）第（1）款图1. (a)基于对象的图形方案（b）基于对象的图形规则应用。 可以使用ADT中定义的操作。• 右侧R：描述了在应用规则之后将出现的项目它包括：· 对象：出现在规则左侧的所有对象和属性，以及新对象（由规则应用程序创建）。属性的值可以更改，但属性不能删除;· 消息到R中出现的所有对象。• 一个条件：必须满足该条件才能适用该规则。这个条件是关于左侧和右侧属性的等式。形式上，我们使用类型化属性超图，规则是一个（部分）图同态与应用条件。正式定义见第4节。现在我们可以定义一个基于对象的系统。该委员会的组成如下：• a类型图：包含关于该系统中涉及的所有类的所有属性（属性可以是ADT类型或对其他类的引用）和由每种对象发送/接收的消息的信息的图。该图可以看作是上述基于对象的图方案的实例化。• 一组规则：这些规则指定对象在接收消息时的行为对于同一类型的消息，可能有许多规则指定预期的行为。取决于这些规则所施加的条件（取决于消息的属性和/或参数的值），它们可以是互斥的或不互斥的。在后一种情况下，其中一个将被非确定性地选择执行。 请注意，当接收消息时，对象的行为并不是指定为一系列应执行的步骤，而是作为对象属性值的原子更改以及可能向其他（或相同）对象创建新消息。也就是说，没有控制结构来管理指定实体行为的规则的应用。我们的方法是数据驱动的。这样做的优点是避免了计算步骤的不必要的序列化，因为规范只需要关心事件之间的因果依赖关系。• 初始图：该图指定了对象属性的初始值，以及在创建这些对象时必须发送给它们的消息类属性atr 1atr 2消息ATR1类atr2：PAR1消息PARADTO.M. Mendizabal等人理论计算机科学电子笔记184（2007）151155这个图中的消息可以看作是对象执行的触发器。OBGG的行为由状态转换系统给出，该状态转换系统通过应用从初始状态开始的语法规则而2.1示例：令牌环协议在本节中，我们将介绍OBGG的使用。令牌环协议相对简单，可以让读者快速理解，并在第5节中举例说明翻译过程。令牌环协议用于控制环形拓扑网络中各个站对共享传输介质的访问[14]。根据该协议，一种称为令牌的特殊位模式仅在一个方向上从站传输到站。当一个站点想要通过网络发送一些内容时，它等待令牌，持有它，并在环上发送消息。 帧在环中循环，目的站可以复制其内容。当帧完成周期时，它被始发站接收。然后，始发站从环中移除帧，并将令牌发送到下一站，下一站然后可以如已经描述的那样起作用。由于只有一个令牌，在给定时间内只有一个站可以进行传输。图2（a）是一个类型图，定义了类型Node。Node的Node有一个布尔属性sent，可以接收两种消息：Msg表示数据帧，Token表示令牌。到下一个Node的链接由对象引用next3给出。(a)（b）第（1）款图2. (a)节点的类型图和（b）令牌环模型的初始图。定义此模型行为的规则如图3所示。如果节点接收到令牌，则它可以发送消息（规则发送）或传递令牌（规则令牌传递）。如果Node决定发送Msg，则sent属性被分配为true。当节点接收到消息并且它是发起节点（如果其属性发送为真），则应用规则Complete，从环中删除Msg并生成3图形符号：在图2（a）中，矩形是顶点，圆圈内的数字是这些顶点的名称（这些符号用于指示图2（b）和3中每个顶点的类型）。顶点中的项是顶点属性。图2（a）和图3中出现的消息符号是超弧。156O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151将令牌（Token）复制到（下一个）节点。如果接收节点不是发起节点（其属性sent为false），则应用规则Transmit，并将Msg传递给下一个节点。图3. Node类的规则。初始图如图2（b）所示，定义了启动情况的各种实例、定义了一个有四个节点的环，称为Node1，Node2，Node3和Node4。每个实例的属性next指向下一个Node。所有发送的属性最初都是false，只有一个节点（Node1）具有令牌。此模型是有限状态的，并在有限计算中生成，允许对生成的SAN模型进行稳态分析。O.M. Mendizabal等人理论计算机科学电子笔记184（2007）1511573随机自动机网络在随机自动机网络（SAN）形式主义中，系统由相互作用的子系统建模，这些子系统又由可能独立行为或可能具有依赖性的自动机表示根据[13，2]，SAN具有与马尔可夫链完全相同的应用范围，其优点是模型是按组件构建的，并且数学解是根据状态空间优化的[10]。SAN模型可以是离散时间的，也可以是连续时间的。在本文中，我们专注于连续时间的情况下。在这里，我们将使用SAN的一个不太一般的定义，因为我们不需要这种形式主义的所有特征来描述OBGG的stochastic扩展。自动机由状态和转换组成，并标有事件名称。一个SAN模型是由各种自动机组成的。这些自动机可以独立地与本地事件（可能只考虑参与该事件的自动机的本地状态）一起进化，而同步事件用于模拟两个或多个自动机的联合进化。将分布概率与事件联系起来，由SAN产生的带标号转移系统就产生了一个马尔可夫链，从而可以计算SAN的每个状态的稳态概率。更具体地说，每个事件都有一个相关的发生率。发生率的倒数是指数分布函数的平均值，该函数调节事件两次发生之间的时间间隔。定义3.1（自动机）自动机是一个元组A=（S，T，E，i），其中S是有限的状态集，E是有限的事件集，T<$S×2E×S是转移关系，i∈S是初始状态。给定一个自动机A，我们用 SA， TA， EA和 iA表示它的组件。给定一个状态s∈S，我们用outputEvents（s）={e|（s，ES，SJ）∈T和e∈ES}，以及可达集给定事件的状态由outputStates（s，e）={sJ|[1][2][3][4][5][6][7][8][9][9][10][10][11]定义3.2（随机自动机网络（SAN））随机自动机网络（SAN）是一个元组SAN=（SE，AL，τ），其中SE是事件，称为同步事件，AL是自动机列表，τ：E→R+是速率函数，其中E = SEi∈{1. |}（E Ai − SE）.|}(E Ai− SE). SAN的状态是元组s =（s1，.得双曲余切值.|AL|），其中si∈ S Ai.SAN定义了一组事件，用于在执行过程中同步不同的自动数据。SAN的状态变化是可能的，当所有不同的自动机，可能从事一些事件是在一些状态，其中标记为该事件的转换是可能的。注意，由于可能存在标记有相同事件的不同transition，因此可能存在以相同状态开始并执行相同事件的不同可达状态。定义3.3（启用事件，状态更改）给定SAN SAN =（SE，AL，τ），|AL|= n和状态s =（s1，.，s n），我们说事件e在s中被启用，如果158O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151(i) i∈ {1.. n}.e∈outputEvent（s i）或ei ∈EAi;以及(ii) τ（e）/= 0。如果 一个 事件 e 是 启用 在状态s=（s1，. ，s n），状态改变你可以把你的名字写下来，让它变成一个状态 SJ=（SJ， . . ，sJ）where sJ=1ni如果x∈outputState（si，e）且e∈outputEvent（si），i，否则图4描绘了说明性SAN示例。有两个自动机表示，Aut1和Aut2。它们的初始状态分别是st1和st2（灰色圆圈所示的状态）。同步事件由sync 1和sync 2指定，而本地事件由loc1和loc2指定。注意，只有Aut1在st2中，Aut2在st1或st2中时，sync2才有效。本地事件独立于其他自动机，例如，当Aut1处于st1时，loc1将处于活动状态，独立于Aut2状态。Aut1 Aut2Sync2Sync2图4. SAN示例。4基于随机对象的图文法在本节中，我们将定义基于随机对象的图文法。在图语法中将发生率与规则相关联（例如，如针对SAN中的事件和针对SPN中的转换所做的那样），可以获得转换系统语义，其中系统的每个状态将具有相关的概率，它是系统在稳态情况下处于该状态的概率（即，转换系统语义产生连续时间马尔可夫链）。这些信息在并发系统的分析中是非常有用的，并且是对基于模型检测的分析的补充。一些非功能性的方面可以通过随机的形式主义，如性能和依赖性进行评估。因此，这些信息有助于指导开发人员调整复杂系统中特定需求的界限。ST1loc2Sync2sync1ST3ST2sync1sync1ST1loc1ST2O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151159G在下文中，我们扩展了[5]将发生率与规则相关联。假设读者熟悉代数规范的基本概念我们将定义随机OBGG，短SOBGG，超（类型和属性）超图，即，图中的边可以连接到任何（有限）数量的顶点。在图形上，边被描绘成一个盒子（其形状可能会有所不同），与顶点的连接被绘制为细线，称为触角。边的触角基于对象的图形的主要特征是：• 每个基于对象的图对一组对象进行建模，其中对象的内部状态（其属性集）通过引用其他对象和/或预定义数据类型的值来描述。• 每个对象都有一个相关的代数，携带着可以用作对象属性的• 顶点集被划分为两个，分别建模对象身份和数据值。• （超）边的集合被划分为两个，分别建模对象的消息和每条边都有一个目标（接收消息/属性所属的对象），并且可以有许多源（消息的参数/对象的属性）。OBGG的定义基于一类图和部分态射。定义4.1（弱交换性）给定两个部分函数f，fJ：A→B，我们说f比fJ定义得更少（我们写f≤fJ），如果dom（f）不等于dom（fJ）且f（x）=fJ（x），对所有x∈dom（f）。给定两个部分函数f：A→B和FJ：AJ→BJ，以及两个全函数a：A→AJ和b：B→BJ，我们说如果FJ<$a≤b<$f，则所得图弱交换。现在我们介绍基于对象的图和部分态射。如上所述，每个超边具有一个目标顶点，并且可以具有许多源顶点。源顶点由不同数量的触角标识，也就是说，超边与顶点列表相关联。定义4.2（基于对象的图，基于对象的图态射）给定一个代数规范Spec，一个基于对象的图（OB图）G=（VG，EG，sG，tG，AG，aG）由一个顶点集的集合VG组成，该顶点集被划分为（分别为对象和属性的）集合oVG和aVG，一个集合EG=（mEG，aEG），的（超）边划分成集合mEG和aEG（分别为消息和属性），总源函数sG：EG→VG，分配给每个边的顶点列表，总目标函数tG：EG→oVG，分配给每个边的对象顶点，Spec上的代数AG，以及属性函数aG：aVG→ U（AG），分配给每个属性顶点的值来自AG4的载体集合。4U：Alg（SPEC）→Set是赋予每个代数其载体集的不交并的遗忘函子。160O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151VEEE21EEE一个（部分）OB-图态射g：G→H是一个元组（g V，g E，g A），其中第一个分量是部分函数g V= g oV<$g aV，其中g oV：oV G→oV H，g aV：aV G→aV H，g E= gmE<$g aE，其中g mE ：mE G→ mE H 和gaE：aEG^aEH;第三个分支是全代数同态它们是弱同态的，即gVsG≥sHgE，gVtG≥tHgE，U（gA）aG≥aHgV（如果映射了一条边，则对应的顶点（如果映射了）必须具有相同的源/目标顶点，如果映射了一个顶点，则属性必须相同）。一个态射被称为全态射，如果两个分量都是全态射。OB-图和部分OB-图态射的范畴用OBGraphP表示（恒等式和合成是按分量定义的）。GE_G_HGE_G_HGV_G_HsG≤JsHtG≤J JtHaG≤aHJ J JV）VVGVU（AG）U（A）VHVU（gA）H为了区分不同类型的顶点和边，我们将使用类型图的概念[3，8]：每个图都配备了类型5的固定图的态射类型。由于类型将构成类定义的静态部分，我们将把类型图称为类图，并且将施加一些限制以保证它对应于对象范式意义上的类（第一个限制是说类图中没有数据值，它们由数据类型的名称表示，第二个限制是每个类只能有一个属性列表）。定义4.3（类型化OB-图）设Spec是一个specification。 一个OB-图C称为一个类图i∈（i）AC是Spec上的一个最终代数，（ii）对于每个对象顶点v∈oVC，恰有一个属性超边（ae∈aEC）具有目标v.C上的类型OB-图是一对OGC=（OG，typeOG），其中OG是一个被称为实例图的OB-图，而类型OG：OG→C是一个全OB-图态射，称为类型态射。类型OB-图OGC关于OGC是一个部分OB-图态射f：OG1→OG2使得 OG1 型≥OG2 型 <$f.类图C上的类型化OB-图的范畴，记为OBGraphP（C），以C上的OB-图为对象，类型化OB-图之间的态射为箭头（恒等式和合成是部分OB-图态射的恒等式和合成）。规则定义了对象在接收消息时的反应每个规则表示如何处理一个特定的消息（可能需要许多规则来描述对一个消息的所有可能反应）。定义4.4（规则）设C是一个类图，Spec是一个规范，X是一组Spec类型的变量。规则是一个对（r，Eq），其中Eq是规范Spec上的一组方程，r：L→R是C型OB-图态射s. t。[5]请注意，由于使用了部分态射，这不仅仅是一个逗号范畴的构造：态射类型是全态射，而图之间的态射是部分态射，我们需要弱交换性而不是交换性。GGO.M. Mendizabal等人理论计算机科学电子笔记184（2007）151161(i) L和R是有限的;(ii) 删除了一条消息超边缘：删除！e∈mEL，称为trigger（r），trigger（r）/∈int n（r）;(iii) 只有消息的目标的属性可以出现在L：（aEL=）中（（！e∈aEL）<$tL（e）=tL（trigger（r）;(iv) 现有对象的属性不能被删除也不能被创建：o ∈ oV L。（e∈aEL.tL（e）=oeJ∈aER.tL（eJ）=rV（o））;(v) 对象不能被删除：o∈oVL.o∈dom（rV）;(vi) r的代数是指定Spec上的项代数TSpecJ（X），包括一组方程Eq;(vii) 出现在L中的属性只能是X的变量：<$v∈（aVL<$aEL）.aL（v）∈X的;(viii) R的代数同态分量是单位元。我们用规则（C）表示类图C上所有规则的集合。为了定义SOBGG，我们首先定义一个类图，对系统中可能存在的对象、消息和属性的类型进行建模。然后我们使用规则定义系统的行为，以及可能的初始状态（即包含类图中类型实例的定义4.5（随机对象基图文法（SOBGG））给定一个C型图。基于随机对象的图文法是一个元组SOBGG=（Spec，X，C，IG，N，n，ρ），其中Spec是一个代数规范，X是一组变量，C是一个类图，IG是在C上类型化的图，称为起始图，N是一组规则名，n：N→Rules（C）为每个规则名分配一个规则，ρ：N→R+为每个规则分配一个速率。SOBGG的行为是通过将规则连续应用于开始图来获得的。每个规则应用程序删除一个消息（规则的触发器），并可以更改内部属性的值，创建新的消息和/或对象。形式上，规则应用程序的结果是通过相应类别（基于类型对象的图）中的推出获得的。定义4.6（推导步骤，衍生）让SOBGG=（Spec，X，C，IG，N，n，ρ）是SOBGG，（r ：L→ R，Eq）∈ n（N）是一个规则，并且IN是在C上类型化的图。IN中r的匹配是全态射r，mm：OBGraphP（C）中的L→IN。 使用规则的推导步骤IN=OUTr和matchm是OBGraphP（C）类别中的推出。态射rJ：IN→OUT称为派生规则。SOBGG的推导序列是推导序列我，我R步骤G i=<$G i+1，i∈ {0，.，n}，n∈N，其中G0 = IGL_Rm（PO）mJ和r i∈规则对于所有i∈ {0，.，n}。一个SOBGG的所有导序列的类记为SDerSOBGG.J J在J 出来SDer中的所有可达图类r，mSOBGG 定义为：r状态SOBGG={G|G = IG<$IG =<$G∈ SDer SOBGG}162O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151SOBGG的计算与底层的OBGG（没有tax函数的语法）完全相同。以下行为语义的定义描述了这些计算，不考虑随机行为（将在第5.2节中考虑）。定义4.7（SOBGG行为语义）给定一个随机的基于对象的图语法SOBGG=（Spec，X，C，IG，N，n，ρ），其行为语义BehSem（SOBGG）由标记转移系统TS=（S，L，q0，→）定义，其中：• S=状态SOBGG是状态的集合;• L=N是转换标签的集合;• q0=IG是初始状态;• →由以下规则给出：nr，mJG=G∈SDerSOBGG数量，mG −→G5OBGG的随机语义为了将概率与行为语义的状态相关联，我们必须求解相应的随机模型。为此，我们将SOBGG转换为随机自动机网络（SAN），求解相应的SAN，然后最终完成SOBGG的随机语义。5.1将OBGG转换为SAN在从SOBGG到SAN的转换中，SOBGG对象的属性和消息来源于SAN自动机状态，规则被映射到转换、事件和速率。每个对象的状态与一组自动机相关联：每个属性有一个自动机;每个对象引用有一个自动机;对象可能接收的每种类型的消息有一个自动机。与对象相关的所有属性和消息都由类图定义。 给定一个类CG=（VCG，ECG，sCG，tCG，ACG，aCG），集合oVCG和aVCG的元素表示系统中允许的类型（分别为对象和数据）。集合mECG描述系统的消息类型，并且集合aECG具有属性超弧（其将每个属性连接到每个对象顶点）作为组件。mECG的元素可以在系统执行期间被删除或创建，而aECG的集合必须是稳定的（因为对象不能丢失或获得属性）。然而，由于我们处理的是有限状态模型，mECG可能不会无限增长。对于每种类型的消息msg∈mECG，让max（msg）表示可能存在于SOBGG的某些状态中的此类消息的最大实例数。另一个限制是我们不允许创建对象。后一种限制可以通过允许有限数量的对象被JO.M. Mendizabal等人理论计算机科学电子笔记184（2007）151163已创建，但这取决于未来的工作。基于SOBGG的类图和初始图，我们将构造用于构建相应SAN的自动机状态集。在下面的定义中，我们将使用n个元素的消息列表作为类的属性和参数，但请注意，n可能为零，导致空列表。初始图将用于获取有关数据值（在代数组件中定义）和系统中可能存在的对象的信息。我们将使用一个函数声明，给定一个顶点，返回该类型的值集。如果这个顶点是数据类型的名称，则结果是代数的对应载体集。如果它是一个对象类型，它返回初始图中该类型的顶点集（对象id）。图语法的规则将提高SAN的转换和事件，并且相关联的速率将成为相应事件的速率首先，我们将定义如何获得结果SAN的事件集，然后如何构造每个单独的自动机。定义5.1（将规则应用转换为事件）设SOBGG=（Spec，X，CG，IG，N，n，ρ）是一个随机的基于对象的图文法。我们定义由SOBGG引起的事件集合E，记为事件（SOBGG），事件（SOBGG）={e ∈事件（规则名称）|规则N ame ∈ N}其中events（rn）={（rn，dr：IN→OUT）|与IG具有相同代数的CG型图IN，m：L→IN是满射匹配，dr是n（rn）应用于m的导出规则。对于每个事件e=（rn，dr）∈E，我们定义message（e）为dr删除的消息超边，msgType（e）=typeG（message（e）），object（e）=tG（message（e）），ruleName（e）=rn，param（e）=sG（message（e））。在类的实例中，将为每个属性创建一个自动机，这些自动机中的每个自动机的状态表示这些属性可能假定的值，并且转换描述由某些规则应用程序执行的可能的状态更改定义5.2（生成的属性自动机）让 SOBGG =（Spec，X，CG，IG，N，n，ρ）是一个随机的基于对象的图文法，obj∈oVIG是一个对象恒等式。为objAutAttrobj生成的属性自动机定义为AutAttr obj={AutAttr（v1）obj，.，AutAttr（v n）obj其中，s IG（ae）= 1，.，. ，v nn，ae是o b j 的属性hyperedge，并且每个AutAttr（vi）obj=（Si，Ti，Ei，inii）是一个自动机，定义为：• Si=states（typeIG（vi）），• inii=vi，164O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151Node1• 转 换 集 Ti 如 下 获 得 ： 对 于 每 个 事 件 e = （ rn ， dr ： IN →OUT ） ∈Events（SOBGG）），如果obj = object（e），则IN中obj的属性顶点ae被dr删除，并在OUT中重新创建为aeJ，其中s IN（ae）=1，.，.。，v nn，并且sOUT（aeJ）= sOUT，J，.，.，vJ，过渡v{e}个 vJ在T中。1ni−→ii• Ei是用作Ti中的转换的标签的事件集合的并集。在图5中，sent Node1和next Node1属性自动机表示根据我们的转换方法的令牌环OBGG模型的对象Node1的sent和next属性用于标记转换的事件名称由应用规则的名称（引发此事件），属性名称列表和构建匹配所需的相应值以及接收消息的对象组成 有一个规则名和一个匹配唯一地指定了一个规则应用程序，即一个事件，因此我们不会在图形表示中使用派生规则本图中描述的其他自动机将在本节中解释。发送节点1Transmit_next_Node2_Node1假Send_next_Node2_Node1Complete_next_Node2_Node1真Send_next_Node2_Node1next_Node1Node2Node3Transmit_next_Node2_Node1发送_next_Node2_Node1完成_next_Node2_Node1令牌节点10Token_Pass_next_Node1_Node4完成_next_Node1_Node4Send_next_Node2_Node1令牌Pass_next_Node2_Node11Msg_Node10Send_next_Node1_Node4传输_next_Node1_Node4Complete_next_Node2_Node1传输_next_Node2_Node11图5. 令牌环模型已翻译。在生成的SAN中，对象可能接收的每种消息和参数值都有一个自动机，每个自动机的状态将表示系统当前状态中存在的每种消息的数量转换将对消息的删除和创建进行建模。定义5.3（生成的消息自动机）让 SOBGG=（Spec，X，CG，IG，N，n，ρ）是一个随机的基于对象的图文法，obj∈oVIG是一个对象恒等式。为objAutMsgobj生成的消息自动机定义为AutMsgobj=（（A i） i∈ M Attr） obj节点4O.M. Mendizabal等人理论计算机科学电子笔记184（2007）151165−→其中，MAttr ={msg} ×states（tv1）×. ×states（tv n），msg∈ {m∈mE CG|tCG（m）= class，type IG（obj）= class}（即，msg是可以由对象obj接收的消息类型）， ，tv n。 每个自动机A i=（S i，T i，E i，ini i），其中i =（msg，v1，. ，v n），定义如下：• S i={0.. max（msg）}，• ini i是msg类型的消息的数量，参数是msgv1，..，...，v n存在于IG中;• 转换集Ti如下获得·删除类型（msg，v1，...，v n）：对于每个事件e =（rn，dr：IN→OUT）∈SE，其中msgType（e）= msg，object（e）= obj，参数param（e）=parv1，.，v n，则将以下转变添加到Ti：{i−→ei− 1 |0 1;在这种情况下，函数nb在状态1中同时返回从令牌节点1到令牌节点4的自动数据的数量。整个表达式返回多个节点具有令牌的概率。这个概率是0.0%。对于属性2，分析是类似的，但是我们看对于多个节点发送的attribute为真的概率。正如预期的那样，这个概率也是0.0%。