受控图文法到普通图文法的转换与系统可靠性的研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记324（2016）15-30www.elsevier.com/locate/entcs受控图文法到普通图文法的转换Alex Bertei1 Luciana Foss2 西蒙娜·A Costa Cavalheiro3技术开发中心（CDTec），佩尔蒂埃佩尔蒂摘要图语法（GG）是描述复杂系统的一种合适的形式化语言。 在GG中，系统状态由图表示，状态之间的变化由规则描述。 GG的使用是有趣的，因为有几种技术用于指定和验证系统，都是用这种语言描述的。除此之外，GG有一个非常直观的图形表示，使得语言即使对于非理论家也很容易理解。受控图文法（CGG）允许定义规则应用序列的GG，考虑辅助控制结构，允许控制这种形式主义的内在非确定性。 然而，对于这种类型的语法，不是验证属性的工具。因此，本文的目的是将受控的图文法转换为普通的图文法，从辅助结构转移流程控制给国家 因此，本文的主要贡献是允许使用罗丹定理证明器，执行CGG规格的属性验证。 这是可能的，通过一种机制，使用规则之间的依赖性和连接性将受控图语法转换成规则图语法。关键词：图文法，控制图文法，依赖与约束规则1介绍软件和硬件系统随处可见，每天我们都面临着更复杂和复杂的系统。系统的开发一直是一项艰巨的任务，需要一个完整的规范，没有错误。每天，这些系统的规模和范围都在增长，经常需要与其他复杂和独立的环境进行交互随着复杂性的增加，错误的可能性也在增加，这可能导致灾难性的损失，无论是在时间、金钱还是甚至生命方面。因此，帮助开发可靠和正确的系统的技术变得越来越必要[1]。一1电子邮件地址：abertei@inf.ufpel.edu.br2电子邮件地址：lfoss@inf.ufpel.edu.br3电邮地址：Simone. inf.ufpel.edu.brhttp://dx.doi.org/10.1016/j.entcs.2016.09.0041571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。16A. Bertei等人/理论计算机科学电子笔记324（2016）15达到这一目标的方法之一是通过使用形式化方法，即基于数学形式主义的技术，它可以提供更严格和有效的措施来规划、建模和分析计算机系统[2]。一个规范必须是紧凑的，准确的，没有歧义，也就是说，它必须通过一种具有良好定义的语法和语义的语言给出，其中使用数学概念。这些概念很重要，因为它们可以说明计算系统是否呈现某种属性或满足其规范[3]。在过去的十年中，一些案例研究和工业应用证实了使用形式化方法来提高质量的重要性。硬件和软件系统。然而，使用形式化方法的高成本导致它们通常仅用于高完整性系统的开发，其中错误导致生命损失或严重损害的可能性很高。定义良好的规范，在关键属性方面得到验证，为正确和有效的源代码生成提供了基础。巴黎地铁系统就是一个典型的例子[4]。 系统 全自动驾驶，其关键安全部件由MatraTransport International使用B方法正式开发[5]。图语法（GG）是一种形式语言，自20世纪70年代以来一直在研究[6]，并应用于需要动态图模型的计算机科学领域，即可以在其结构中支持转换或操作的图。GG是一种可视化语言，它允许形式化地描述和验证具有复杂特性（如并行性、并发性和分 布性）的 系统。 除此之 外，还有 不同的 技术和 工具允许 使用模 型检查[7][8][9][10]和定理证明[11][12][13]，用于分析这种语言描述的系统的属性。 在图语法中，系统的状态由图表示，状态的行为或变化由图变换规则定义。这种语言允许形式语言的规范化，模式识别，图像识别和生成，编译器的构造，并发和分布式系统的建模，软件工程，数据库项目等[15]。在通常的图语法方法中，规则应用的顺序不是由控制结构定义的，而是由当前状态下可用的资源（数据）定义的另一方面，受控图语法允许在规则应用中定义序列，不仅考虑状态，而且考虑辅助控制结构，例如正则表达式或状态机。但是，没有工具可以对这种类型的属性进行正式验证 语法。 在[11]中，提出了一种用于GG的关系方法，使用罗丹工具的定理证明器[14]。 该工具使静态（语法）和动态验证，使用Event-B语言。因此，本文提出了一个建议，将受控图文法集成到GG的定理证明技术中，然后允许分析使用具有控制结构的GG指定的系统的属性，以应用规则。在本文中，我们考虑的图形语法，其中控制是通过正则表达式。正则表达式（RE）所施加的限制可以A. Bertei等人/理论计算机科学电子笔记324（2016）1517→不能直接翻译成Event-B语言。这种不可能性是由于Event-B上没有一种控制结构允许定义事件的执行顺序。一个事件在它的守卫被填满时被启用。然后，由RE施加的控制结构被转移到数据。为了做到这一点，定义了从CGG到GG的转换，其中规则应用的顺序由这些规则之间的连接和依赖关系给出2图文法图文法（GG）已经被用于指定各种类型的软件系统[15]，其中图形用于表示状态和图形转换规则，用于系统的操作或状态更改。由于图文法是在同一时间，直观和形式化，并允许以简单的方式处理并发和分布方面，他们成为可靠的软件开发的一个有前途的方法。GG是一种形式化语言，适合于描述各种计算系统。它是一种可视化的语言，这使得它非常直观，即使对于非理论家也可以轻松理解模型。GG使用图而不是字符串来推广Chomsky文法。定义2.1[图和图态射]一个图G =（VG，EG，o G，d G），由一组顶点VG，一组边EG，源函数和目标函数o G，dG：EG→VG。从图G到图H的（部分）图态射g：G→H是由两个弱同态的部分函数gV：VG→VH和gE：EG→ EH组成的元组g=（gV，gE）. e.gVoG≥oHgE和gVdG≥dHgE。这些限制可以定义为弱交换性，EGGEH.E.HEGGEH.E.H右边的图表。一个态射g称为全射或内射，如果两个都是复合的。oG≥oHCcdG≥dHCc项分别是全项或单射项。VGgVH.V.HVGgVVH通常使用图中的一些类型化机制来代替仅具有顶点和边的简单图。图形类型可以通过标签、属性或类型图来完成。 在本文中，类型是由类型图提供的。一个文法的类型图刻画了系统中允许的所有类型的顶点和边，并且文法的所有图都被限制在这些类型中。这个限制由映射类型图中每个图的图态射定义。定义2.2[类型图和类型图态射]类型图GT是一个元组GT=（G，tG，T），其中G和T是图，tG：G T是一个全图态射，称为类型态射。具有类型图T的图GT和HT之间的类型图态射是态射g：G→H使得tG≥tHg（即g可以只映射相同类型的元素在图文法中，系统的状态由图表示，状态的可能变化由规则描述规则定义的元素18A. Bertei等人/理论计算机科学电子笔记324（2016）15应该出现在图表中，这样它就可以被应用，并且由它的应用程序进行更改，其中一些元素被删除，另一些元素被创建。 图转换系统的行为由重写规则的应用确定，也称为图产生[15]。遵循双推出方法（DPO）[15]，规则由三个图组成：左侧L，右侧R和接口K，接口K表示L和R共有的元素。它规定，一旦在当前状态中找到图L的出现，它可以被图R替换，保持K。定义2.3[规则] T型（图）规则是一个元组q：LqLQ←−KqRQ−→Rq其中q是规则的名称，Lq，Kq和Rq是T-型图，lq是包含，rq是内射态射.所有T型图规则的类用Rule（T）表示。一般来说，图语法描述了一个系统，它由一个类型图组成，它表征了系统中允许的顶点和边的类型;一个初始图，它表示系统的初始状态;和一组规则，它描述了系统中可能发生的可能状态变化。除此之外，规则可以具有关联的名称。为此，定义了一组规则名称，每个名称都通过一个函数与一个规则相关联定义2.4[图语法]一个（类型化的）图语法是一个元组GG=（T，I，P，π），使得T是一个类型图（语法的类型），I是一个在T上类型化的图（语法的初始图），P是一组规则名称，π：P→Rule（T）是一个全函数，它将P中的每个名字与T上的一个规则相关联。示例2.5给出一个示例来说明图语法规范。该示例描述了一个系统，其中超市顾客进行购买并进行支付。此外，客户可能必须排队才能完成付款。图1和图2分别显示了类型图和初始图。图3显示了SuperMarket图语法的规则集。由于空间的原因，图3中的K图被省略了，但是它们可以通过L和R的交集来重建。指定系统的所有图只能有顶点和边，其类型出现在类型图中Fig. 1. 超级市场图文法的类型图类型图有两种类型的顶点，一种代表顾客，另一种代表收银员。免费，购物和下一个边缘有作为源A. Bertei等人/理论计算机科学电子笔记324（2016）1519图二. 超级市场图文法的初始图图三. 超级市场图语法规则和目标Customer顶点，其中前两个描述客户状态，最后一个将客户连接到收银员行。 收银员顶点有循环边free，busy，emptyLine和no-emptyLine，它们描述收银员和行的状态.第一条和最后一条边的源在Cascade顶点中，目标在Customer顶点中，它们表示20A. Bertei等人/理论计算机科学电子笔记324（2016）15收银台线，分别。初始图描述了超级市场系统的初始配置，该系统由两个收银员和两个客户组成。一个收银员（收银员2）是空闲的，没有排队;另一个收银员是忙碌的，只有一个顾客（顾客1）在相应的排队中（那么这个顾客是排队中的第一个也是最后一个）。另一位顾客是免费的，可以随时开始购物。规则描述了客户的行为。到达超市后，顾客开始购物（开始规则）。最后，他可以去收银员那里。如果收银员中有一行，客户必须最后输入（输入1和输入2规则），否则他将立即得到服务，收银员将其状态更改为忙（支付1规则）。当收银员空闲并且在队列的开始处有一个客户时，该客户离开队列并被服务，队列的连接和状态被重新安排，并且收银员的状态被更改为忙（支付2和支付3规则）。顾客在付款后离开收银员，收银员成为自由人（付费规则）。当客户结束购物时，他将其状态更改为免费（完成规则）。使用图语法指定的系统的行为可以被描述为通过在表示系统状态的图中应用图语法规则，因此，语义由从初始图导出的一组图给出。只要在当前状态图中存在规则的左手侧的出现，即，如果存在将规则的左手侧映射到状态图中的全图态射，就能够将规则应用于图（导出步骤）。在双重推出方法中，通过直接求导给出了一个产生式的应用。在这种方法中，直接派生由两个推出定义：第一个删除所有应该被消费的项目，第二个包括所有应该被创建的项目。直观地说，两个图相对于另一个图的推出，称为接口图，是通过将这两个图粘合在一起来给出的，识别接口中的项。一个导子是直接导子的有限或无限序列，其中一个导子的最终图是另一个导子的开始图定义2.6【直接推导】给定一个T型G，一个T型图规则q：Lq←−Kq−→Rq和匹配（即内射T型图态射）m：Lq→G，存在使用q（基于m）从G到H的直接导子i，则可以构造右边的图，其中两个正方形是T-图中的推出（图的类别和Lq，L KQrRq图态射）。在这种情况下，（1）（2）mq，m qCc c表示为δ：G=H或δ：G=H，如果我们不G、D和H使明确M.勒什尔河上图的构造依赖于D的存在，称为推出补。为了确保这种存在性，匹配m必须满足关于l的胶合条件。该条件分为两部分：悬挂条件，即，如果顶点被删除，则不可能有到达或离开该顶点的边;并且识别条件，即，两个顶点只有在保持不变的情况下才能被mA. Bertei等人/理论计算机科学电子笔记324（2016）1521定义2.7【悬挂条件】设l：K→L和m：L→G是两个图态射，其中m是内射。则存在推出补满足悬挂条件，即：没有边e∈EG−mE（EL）与gv（VL−lv e（VK））中的任何顶点关联。这些规则可以顺序或并行应用。图语法的顺序语义由使用GG规则的所有推导步骤的序列提供，其中一个步骤的每个最终图是下一个步骤的初始图如果有一条规则创建了另一条规则所需要的某个项目，那么可以认为它导致了第二条规则。这强调了这样一种观点，即原因为某种行为提供了必要条件。此外，由于某些规则可以同时（并行）应用，因此这些规则必须不冲突，即一个规则不能删除其他规则使用的某些项。以下定义回顾了因果依赖关系和冲突关系。定义2.8[（因果）依赖和冲突关系]如果规则p创建了q需要（保留/删除）的某个项，则规则p是规则q的（直接）原因。这意味着q只能在p发生之后才能发生如果规则p删除了q所需要的（保留/删除的）某些项，则规则p与q规则相冲突。这意味着如果p发生了，q就不会发生（p排除了q的发生）。3图文法允许基于规则指定图变换的形式通常不是确定性的，即，当存在可以同时应用的若干规则时（即，在状态图中存在语法规则的若干出现），以非确定性方式选择要应用的规则这种非确定性可能有两个原因：可能有一个以上的规则可以应用于给定的图;或者，一个规则可以应用于图的不同部分。因此，为了设置或指定图的变换，通常期望调节该过程。例如，根据优先级选择规则，或者定义特定的步骤序列[10]。控制条件可以用来限制文法规则应用的不确定性一个典型的例子是只允许派生，其中允许的规则应用序列属于一种特殊的控制语言。正则表达式（RE）可用于指定这些条件，也就是说，它们可用于规定规则必须应用的顺序这里考虑由ε∈EXP，ε ∈EXP和（E1; E2），（E1 + E2），（E1）ε，∈EXP定义的词汇表上的正则表达式类EXP，如果E1，E2∈EXP.为了省略括号，假设以下优先顺序：首先是，然后是;最后是+。直观地说，表达式ε描述了没有规则的应用，p∈ E1指定规则p的应用，仅一次，（E1; E2）描述了E1的应用，然后是E2的应用，（E1+ E2）指定了非确定性选择22A. Bertei等人/理论计算机科学电子笔记324（2016）15Σ在E1和E2之间;（E1）是E1的任意但有限的连续迭代。由正则表达式E表示的语言由L（e）表示，并且包含满足由RE E定义的“scheme”的所有单词导子ρ的路标号为：H0<$p1，m1H1<$p2，m2. npn，mnH n，记作path（ρ），由p1; p2;...给出。;pn.受控图文法由一对CGG=（G，exp）定义，其中G是一个图文法，exp是G文法规则集上的一组正则表达式。定义3.1[受控图文法]受控图文法由一对CGG=（GG，exp）给出，其中GG=（T，I，P，π）是一个图文法，而Exp={e|e ∈ EXP}是P上的一组正则表达式。CGG的所有导子的集合，记为DerC（CGG），由所有导子的集合ρ∈Der（GG）定义，其中path（ρ）∈ L（e），对于所有e ∈Exp。例3.2在例2.5中描述的超级市场图语法中，客户的一个不受欢迎的行为，但被GG允许：客户可以拿起货物，然后不付钱就离开（首先应用开始规则，然后应用完成规则）。为了避免这种情况，可以添加控制结构以仅允许期望的行为。使用 正 则 表 达 式 （ Start; （ Pay1+ （ Enter1 +Enter 2 ） ; （ Pay2 +Pay3 ） ） ;Paid;Finish ）， 顾 客 必 须 开 始 购 物 （ Start ） ， 去 收 银 员 （ Pay1+（Enter1+Enter 2）;（Pay2+Pay 3）），付款（Paid），然后他可以离开超市（Finish）。这一系列步骤（规则应用）可以无限地应用。在这种受控图语法中，很明显，顾客在离开超市时必须经过某个收银台并支付所购物品的费用。3.1翻译由于由RE施加的限制不能被转换为事件B的控制为了做到这一点，CGG到GG的翻译是通过在语法规则中添加依赖项和连接项来定义的这些依赖关系和联系对于保持RE定义的规则的应用顺序是必要的。为了引入依赖关系和冲突，规则的右侧和左侧以及初始图被改变，添加新的顶点。每个添加的顶点必须是新的（它必须来自一个还不存在的类型），因为它不能引起边效应，也就是说，它不能创建除了预期的依赖或连接之外的其他依赖或连接。所有新的顶点也必须添加到新文法的类型图中。由于一个规则可以在RE中出现多次，并且具有不同的顺序限制，因此可以存在同一规则的多个实例，其中每个实例都将具有不同的添加依赖项和连接项。定义3.3给定一个控制图文法CGG=（（TC，IC，PC，πC），exp）和一个正则表达式e=ei∈expei，得到一个等价的图文法GG=（T，I，P，π）如下：A. Bertei等人/理论计算机科学电子笔记324（2016）1523(1)（e1，P1，π1，T1）=depRules（e，PC，πC，TC）;(2)（e2，P2，π2，T，I）=depState（e1，P1，π1，T1，IC）;(3)int n=nums（nums）;π=rules（e2）a π24;语法GG的构造分为三个步骤。 在第一步 (1)第二步，引入规则之间的依赖关系和冲突关系(2)通过在初始图中添加元素来定义初始规则之间的冲突，并且最后，（3）利用新创建的规则来获得规则集。在接下来的小节中，将详细介绍这些步骤对于RE e，在一组规则名称上，e的初始规则集定义为initial（e）={v|w∈ L（e）<$v∈prefix（w）<$|v| = 1}。以类似的方式，e的最终规则集定义为final（e）={v|w∈ L（e）<$v∈suffix（w）<$|v| = 1} 5。3.2在规则之间添加依赖关系和冲突在第一步中，更新规则和类型图，包括新的顶点来定义依赖关系和连接，以反映由e定义的应用程序序列。结果规则集包含所有原始规则和每个更改规则的一个新版本更改后的规则将接收新的名称，然后正则表达式e也会函数depRules（e，PC，πC，TC）定义了这些新元素的构造定义3.4函数depRules：EXP×P2×（P→Rule（T））×Graphs→EXP×P2×（P→Rule（T））×Graphs在规则之间添加依赖关系/连接关系由下式定义：depRules（e，P，π，T）=4域的限制：S a r ={x ›→ y|x <$→ y ∈ r<$x ∈ S}，其中S是一个集合，r是一个关系。5给定一个词w，前缀（w）和后缀（w）分别表示w的所有前缀和后缀的集合; |W|表示w的长度24A. Bertei等人/理论计算机科学电子笔记324（2016）15⎧⎪⎪⎪⎪⎪⎪⎪不S（e，P，π，T），如果e=r，r∈P（e，PJ，πJ，T），若e=ε，PJ= Pε，πJ= π<${ε <$→ <$→ <$}⎪（sJ，Ps，πs，Ts）=depRules（s，P，π，T）（tJ，Pt，πt，Tt）=depRules（t，Ps，πs，Ts）⎪⎪⎪⎨（sJ，Ps，πs，Ts）=depRules（s，P，π，T）（tJ，Pt，πt，Tt）=depRules（t，Ps，πs，Ts）x/∈VTt，TJ=（VTt⎪{x}，ET，oTt，dTt）（sJJ，PsJ，πsJ）=right（sJ，Pt，πt，x）（tJ，PtJ，πtJ）=左（tJ，Pt，πt，x）PJ=Pt<$PtJ<$PsJ，πJ=πt<$πtJ<$πsJ⎪（es，Ps，πs，Ts）=depRules（s，P，π，T）⎪JJJSSSx/∈VTs，TJ={VTs⎪{x}，ET，oTs，dTs}（es，Ps，πs）=right（e，P，π，x）（sJ，PsJJ，πsJJ）=left（eJs，PsJ，πsJ，x）⎪⎩PJ=Ps∪PsJ∪PsJJ,πJ=πs∪πsJ∪πsJJ为了添加依赖项，正则表达式被分解为子表达式和每一个中的变化在必要时进行，因为不是RE的所有操作都需要添加依赖性和连接性。 REe可以是以下类型之一：ε（空），规则（原子），连接，选择或闭包。需要添加依赖项/连接项的类型是连接和闭包。所以对于原子REr来说，什么都不应该改变。对于空REε，空规则（不删除、保留或创建任何内容的规则对于一个选择，只有它的子表达式的变化应该被反映。对于连接，除了反映每个子表达式的变化之外，还需要添加由该操作创建的依赖关系此外，对于第二子表达式的每个初始规则，相同的顶点被添加到左手侧。最后，对于闭包s，必须反映s的变化这个操作引入了一个循环依赖，它是通过分别在s的每个初始和最终规则的左侧和右侧添加一个新顶点来定义的。此外，初始和最终规则必须保持，以便允许中断循环。右（左）函数在给定正则表达式的最终（初始）规则的右（左）侧添加给定顶点，定义新规则。正则表达式必须使用新规则的名称进行更新，以反映子表达式的依赖关系。此外，此表达式还显示了哪些规则（SJ+TJ，Pt，πt，Tt）， 如果e=s+t，其中（sJJ;tJJ，PJ，πJ，TJ）如果e=s;t，其中（sJ;PJ，πJ，TJ），如果e=s，其中A. Bertei等人/理论计算机科学电子笔记324（2016）1525应该保存在最终的图形语法中。这个信息是必要的，因为在创建依赖关系的过程中，原始规则被保留（因为它们可以在表达式中出现不止一次），并且在过程结束时，未使用的规则应该被丢弃（第三步）。考虑一个类型图GT和一个新的顶点x：• addV（GT，x）=（（VG<${x}，EG，oG，dG），（tV• extType（GT，x）=（G，tG，T<${x}）.n {xn →x}，tEG），T∈ {x}）;定义3.5函数右、左：EXP×P2×（P→规则（T））×集合→EXP×P2×（P→规则（TJ））定义为：right（e，P，π，x）=（eJ，PJ，πJ），其中：PJ=π;πJ=π;eJ=e;<$p∈final（e），其中i∈N<$isnew（P<$PJ，pi）PJ=PJ<${pi}Rpi=addV（Rp，x）;Kpi=extType（Kp，x）;Lpi=extType（Lp，x）πJ=π{pi（Lpi←Kpi→Rpi）}eJ=upFinalNames（eJ，pi）left（e，P，π，x）=（eJ，PJ，πJ），其中：PJ=π;πJ=π;eJ=e;<$p∈initial（e），其中i∈N<$isnew（P<$PJ，pi）PJ=PJ<${pi}Lpi=addV（Lp，x）;Kpi=extType（Kp，x）;Rpi=extType（Rp，x）πJ=π<${pi<$→（Lpi<$Kpi→Rpi）}eJ=upInitialNames（eJ，pi）upFinalNames和upInitialNames函数用于修改正则表达式，以便更新新规则的名称G26A. Bertei等人/理论计算机科学电子笔记324（2016）15定义3.6函数upInitialNames，upFinalNames：EXP×P→EXP定义如下：upInitialNames（e，pi）=A. Bertei等人/理论计算机科学电子笔记324（2016）1527⎩⎧⎪⎨⎧⎪⎨⎧⎪⎨⎧⎪⎨⎪（p+pi）如果e=pupInitialNames（s，pi）;tife =s;tiupFinalNames（e，pi）=（p+pi）如果e=ps;upFinalNames（t，pi）ife =s;t如果e=s+t，则upF inalNames（s，p i）+ upFinalNames（t，p i）通过使用upFinalNames和upInitialNames函数而不是原来的函数，函数right和left分别从右和左进行了区分。这些新函数通过在旧规则名称和新规则名称之间进行非确定性选择来更改旧规则的名称这种修改也可以保持原始规则（需要开始和完成迭代周期）。定义3.7函数upInitialNames，upFinalNames：EXP×P→EXP定义如下：upInitialNames（e，pi）=（p+pi）如果e=pupInitialNames（s，pi）;tife =s;tupInitialNames（s，pi）+upInitialNames（t，pi）ife=s+tNames（s，pi）如果e=supFinalNames（e，pi）=（p+pi）如果e=ps;upFinalNames（t，pi）ife =s;t upFinalNames（s，pi）+upFinalNames（t，pi）ife =s+t如果e=s，则返回finalNames（s，p i）3.3在初始规则之间添加冲突在创建规则之间的依赖性之后，进行新的改变以在RE的初始规则之间添加冲突在这个中间阶段（2）中，函数depState应用于前一步结果以添加冲突。添加此配置修改：规则集，包括添加了冲突的规则;类型图，包括用于创建冲突的新顶点;正则表达式，用新的规则名称替换旧的规则名称;以及初始图，添加第一个规则要使用的元素，从而定义28A. Bertei等人/理论计算机科学电子笔记324（2016）15.他们3.8函数depState：EXP×P2×（P→Rule（T））×Graphs×Graphs→EXP×P2×（P→Rule（T））×Graphs×T-Graphs在初始规则之间添加连接，定义如下：depState（e，P，π，T，I）=（eJ，PJ，πJ，TJ，IJ），其中：PJ= 0;πJ= π;eJ=e;x/∈VT;TJ=（VT<${x}，ET，oT，dT）;IJ=addV（I，x）;<$p∈initial（e），其中i∈N<$isnew（P<$PJ，pi）PJ=PJ<${pi}Lpi=addV（Lp，x）;Kpi=extType（Kp，x）;Rpi=extType（Rp，x）πJ=πJ<${pi→<$（Lpi<$Kpi→Rpi）}eJ=upInitialNames（eJ，pi）3.4选择使用的规则在最后的步骤（3）中，函数规则计算新的图形语法GG的所有规则的集合，仅维护实际出现在REe2中的规则的实例（从第二步骤产生）。这一步是必要的，因为规则集总是随着新实例的增加而增加定义3.9函数规则：exp→ P（P）定义为：rules（e）={r}，如果e=r<$r∈Prules（t）如果e=t;s=t+s，则rules（s）;规则应用的顺序现在由规则之间的依赖性提供，其中一个规则的应用允许下一个规则的应用。通过这些条件，规则中的冲突和依赖可以表示RE的相同行为例3.10图4、图5和图6示出了从例3.2中给出的受控图语法翻译得到的图语法GG。观察到新顶点被添加到类型和初始图中，以及规则的左侧和右侧。在类型图中添加了用于创建依赖项和连接项的所有新顶点：，和。在初始图中，仅添加一个顶点，因为RE的初始规则中仅存在开始规则。同样的顶点也被添加到左侧的开始。1规则。假设新顶点仅位于Start的左侧。1规则，这条规则与任何其他规则都不冲突。注意，有两个版本的Start规则，这是由于闭包操作而发生的。一个版本（开始。（1）应用A. Bertei等人/理论计算机科学电子笔记324（2016）1529见图4。 GG图文法的类型图图五. GG图文法的初始图在闭包迭代的第一次，因为在状态图中仍然没有启用另一个版本的顶点（开始。2）。第二个版本将在以下迭代中启用。同样，有两个版本的完成规则，这是在冲突。为了停止交互，第二个版本的完成规则（完成。（1）必须应用。通过在中间规则的左侧和右侧包含新的顶点，引入了其他的冲突和依赖在这个新语法中，输入1。1，输入1。2，支付1。1是冲突的，并且它们都依赖于开始规则。这意味着只能应用这些规则中的一个，并且只能在应用了其中一个开始规则之后才能应用。请注意，在添加新顶点的过程中，规则名称都发生了更改4结论图语法是一种可视化和直观的语言，允许对具有复杂特征的系统进行规范和形式验证。之所以选择这种语言，是因为有不同的技术和工具允许使用模型检查和定理证明器来验证该语言中描述的系统属性。 受控图语法允许设置顺序 在规则应用程序中，不考虑状态，而是考虑辅助控制结构，如正则表达式。然而，没有工具允许正式验证这种语法的属性在目前的工作中，定义了受控图文法的翻译，这导致了普通的图文法，其中控制由 当前数据和状态。因此，所提出的翻译使得能够使用Event-B语言描述受控图语法，允许使用定理证明技术来验证CGG规范。因此，软件30A. Bertei等人/理论计算机科学电子笔记324（2016）15见图6。 GG图文法规则。设计人员将有机会使用一种形式化的和直观的语言来指定系统，并对这些系统进行属性验证作为未来的工作，我们打算研究使用变量来简化翻译的图形语法的定义，它可以包含大量的规则，这取决于用于控制规则应用程序的RE。为了做到这一点，有必要引入具有属性的CGGA. Bertei等人/理论计算机科学电子笔记324（2016）1531引用[1] Dwyer，M. B、Hatterygal，J.，罗比河普阿苏雷亚努角美国，维瑟，W.：形式软件分析软件模型检测的新兴趋势。软件工程的未来120-136. 03 The Dog（2007）[2] Craigen ，D.，Gerhart，S.，Ralston ，T.：形式方法工业应用的国际调查。Z用户讲习班，伦敦（1993年）[3] Dehar be，D.， 莫雷拉A.M.， Rib，L.， R odrigues，V. M.，： I ntr oducaeo dosFormais：Especific a cao，Se ma nticae VerificacaodeSistemasConcorre ntes. 《美洲和应用信息杂志》。7、7-48（2010年）[4] Behm，P.，Benoit P.，Faivre，A.，Meynadier，J.：METEOR：B在大型项目中的成功应用。计算系统开发中的形式方法世界大会，法国图卢兹（1999年）[5] Abrial，J.R.：B书：将程序转化为意义。剑桥大学出版社，纽约，美国（1996年）[6] Ehring，H.，Pfender，M.，Schneider，H. J.：Graph-grammars：An Algebraic Approach In：AnnualSymposium on Switching and Automata Theory.pp.167-180. IEEE计算机协会。03 The Dog（1973）[7] Rensink，A.：图文法的显式状态模型检查。在Concurrency，Graphs and Models，Pierpaolo Degano，Rocco Nicola ， and Jose; Meseguer （ Eds. ） . 计 算 机 科 学 讲 义 ， 第 5065 卷 。 05 The Dog of the Dog（2008）[8] Ferreira，A.公共图书馆，福斯湖，Ribeiro，L：面向对象的图形语法规范的形式验证。理论计算机科学电子笔记175，101-114（2007）[9] 巴雷西湖Rafe，V.，Rahmani，A. T.，Spoletini，P.：图变换系统模型检验的一种有效解决方案。理论计算机科学电子笔记213，3-21（2008）[10] Kastenberg，H.，Kleppe，A. G.，Rensink，A.：使用图形转换定义面向对象的执行语义。在：Gorrieri，R.，Wehrheim，H.（编辑）FMOODS 2006年。LNCS，vol. 4037，pp. 186-201. 05 The Dog（2006）[11] 卡瓦列罗，S.A. D. C.：图文法的关系方法2010年。计算机科学博士论文- 南里奥格兰德联邦大学- UFRGS（2010年）[12] 里贝罗湖Dotti，F. L.，卡瓦列罗，S. A. D. C.的方法，Cristine，F.：用Event-B.ECEASST.实现定理证明文法.30岁。（二零一零年）[13] 卡瓦列罗，S. A. D. C.的方法，里贝罗，L.：使用逻辑方法验证图语法。科学计算机程序设计。77，480-504（2012）[14] 部署. 事件B和罗丹平台。http://www.event-b.org/（最后一次访问是2015年7月罗丹发展得到了欧盟ICT项目DEPLOY（2008 - 2012）和RODIN（2004-2007）的[15] 罗森伯格，G.：图文法与图变换计算手册：第一卷。层. 世界科学出版社，River Edge，美国（1997年）