面向对象图文法规范的形式化验证方法

理论计算机科学电子笔记175（2007）101-114www.elsevier.com/locate/entcs面向对象图文法规范的形式化验证AnaPaulaLüdtkeFerreira1巴西里约热内卢淡水河谷大学Luciana Foss，Leila Ribeiro2巴西阿雷格里港南里奥格兰德联邦大学摘要由于网络的重要性和当前对模块化、可重用和易于开发的软件的需求，并发面向对象系统无处不在。然而，检查这样的系统的正确性是一项艰巨的任务，主要是由于并发和继承方面。在本文中，我们提出了一种方法来验证并发面向对象系统。我们使用配备了面向对象功能（包括继承和多态性）的图语法作为规范形式主义，并定义了从这些规范到SPIN模型检查器的输入语言Promela的翻译。保留字：图形文法、面向对象程序设计、模型检验。1引言软件开发技术经过多年的发展，以处理当前的开发需求。这些技术所基于的范例（特别是对象、事件和并发）使建模和编码过程变得更容易。然而，这些系统的测试和验证变得更加复杂，主要是由于多个进程竞争相同资源的不确定性行为。面向对象系统的特性--继承、多态和方法调用的动态绑定--也使得静态分析在验证过程中的使用有限。因此，并发面向对象系统的正确性保证是一项艰巨的任务。1电子邮件：anap@unisinos.br2电子邮件：{lfoss，leila}@ inf.ufrgs.br1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.04.020102A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101实现系统正确性证明的第一步是提供系统的形式化规范。可以分析语义模型以检查所需属性是否成立。选择使用哪种规范语言取决于应用程序的特性，但也取决于所选择的开发范式。我们建议，如果遵循面向对象的开发过程，一个适当的正式规格化形式主义应该是兼容的结构。面向对象的图形语法首先在[8]中提出，作为代数单推出方法[13]的扩展，以包含面向对象的特性，如继承，多态性和动态绑定。本文的主要贡献是提出了一个验证方法，规格书写为面向对象的图形文法。这种方法是基于这种规格到Promela程序的翻译。Promela是SPIN模型检查器的输入语言[10]。特别是，继承、多态和动态绑定等特性也将忠实地编码在Promela中。我们的面向对象验证方法是一种直接的、基于翻译的方法，与依赖于对规范语言本身的分析的方法不同，例如[2]，[12]，[1]，[15]，[16]。我们遵循一条工作路线，[5]对于没有面向对象特性的图语法然而，除了为继承、多态和动态绑定特性构建翻译之外，我们还基于定义良好的观察语义[7]进行翻译，该语义从面向对象的范式视图解释面向对象的图形语法计算。本文的结构如下：Sec. 2给出了面向对象图和面向对象文法的主要组成部分。秒3给出了从面向对象的图语法规范到Promela程序的形式化翻译的定义所遵循的指导原则，然后是第2节中显示的示例四、运行的例子是并发理论中的一个经典问题，称为哲学家用餐问题。最后评论见第二节。五、2面向对象的图文法面向对象系统由先前定义的类的实例组成，这些类具有由属性定义的内部结构，并通过消息传递在它们之间进行通信。面向对象的系统状态由对象和一组尚未被使用的消息组成。 信息是触发器 方法的执行，它们的实现可以在派生类中重新定义。类和消息在类模型图中一起建模。在形式上，类标识符是图节点，属性被建模为超弧（也就是说，每个类可以通过属性超弧连接到许多其他类），消息也被建模为超弧（其中目标是消息的目的地，源是其参数）。继承层次结构通过在图节点之间施加严格的关系来定义。严格关系是一种非自相关的、非循环的函数关系，它具有一个额外的性质，即没有通过它连接的元素的无限链（严格关系的自相关和传递闭包是一个偏序[7]）。消息超弧也具有顺序A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101103V±VVV结构，它反映了派生对象重写其超类的继承方法的可能性。带有严格关系的自反传递闭包的集合称为严格有序集。定义2.1[类模型图]类模型图是一个元组V±，E±，L，src，tar，lab，其中V±=V±，±是严格有序的顶点集，E±=E ±，±V E是一个严格有序的（超）边集，L={ attr， msg}是一个无序的两个边缘标签src，tar：E→V是单调保序函数，分别称为源函数和目标函数，lab：E→L是边缘标签函数，使得以下约束成立：• 结构约束：对于所有e∈E，以下成立：(i) 如果lab（e）= attr，则src（e）∈V且tar（e）∈V，且(ii) 如果lab（e）= msg，则src（e）∈V，且tar（e）∈V。• 序关系约束：对于所有e∈E，以下成立：(i) 如果（e，EJ）∈±E，则lab（e）=lab（EJ）= msg，(ii) 如果（e，EJ）∈±E，则src（e）=src（EJ），(iii) 如果（e，eJ）∈±E，则（tar（e），tar（eJ））∈±+，且(iv) if（eJ，e）∈ ±Eand（eJJ，e）∈ ±E，其中itheJ=/eJJ，then（ta r（eJ），tar（eJJ））∈/εannd（ta r（eJJ），tar（eJ））∈/±n.集合{e∈E|lab（e）= attr}和{e∈E|lab（e）= msg}由E表示|属性和E|msg，分别。结构约束确保超弧建模属性和消息具有正确的源和目标。继承和覆盖层次结构通过强加图形节点（即，类）和消息边（即，方法）是严格有序集。只允许单继承，因为±V必须是一个函数。消息弧之间的关系±E通过映射它们来确定在派生对象中覆盖哪些方法。应用于±E的限制确保方法被一致地重新定义，即，只有消息弧可以被映射（i），它们的参数是相同的（ii），被重新定义的方法（严格地）位于类模型图的上方（±+下）（iii），并且只有关于关系±V和±E的最接近的消息可以被重新定义（iv）。例2.2图1中的类模型图描述了哲学家就餐问题的面向对象系统结构。图节点表示类：Philosopher，派生为两种不同的类型：Left-HandedPhilosopher和Right-HandedPhilosopher（继承关系如虚线箭头所示）;Fork，表示哲学家竞争的共享资源;Table，模拟哲学家坐的地方和可以拿起叉子的地方;ForkHolder，可以是Philosopher或Table。属性是元素必须拥有的信息，以便正确计算：哲学家坐在桌子旁，为了吃饭，有一个左叉和一个右叉;叉有一个所有者，这是ForkHolder。消息代表程序中参与者执行的操作。一个叉子可以被哲学家获得，104A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101吃思考吃吃吃右撇子哲学家哲学家左撇子哲学家CC所有者释放ISAT获取修得右叉左叉叉表叉架图1.哲学家用餐问题的类模型图一个哲学家坐在桌子上。哲学家可以思考，吃，或接受一个消息Eat，它将他发送到获取他的叉子的过程，以及一个消息Got，通知已经获取了叉子。左撇子和右撇子的哲学家会忽略“吃”这个信息，这个信息由连接两个超弧的线表示。类模型图可以用作面向对象系统状态的类型结构在定义这些状态（它们将是面向对象的图）之前，我们将定义如何将图映射到类模型图，然后施加限制以使这种映射与继承兼容基于继承和覆盖关系，我们定义了辅助函数，给定类标识符（节点），返回该类的属性集（继承或未继承），以及该类可能接收的消息集定义2.3[C型图]C型图GC是一个元组G，t，C，其中C=<$VC±，EC±，L，srcC，tarC，labC是一个类模型图，G=<$VG，EG，srcG，tarG是一个超图，t是一对全函数<$tV：VG→VC，tE：EG→EC使得（tsrcG）±V（srcCtE）和（ttarG）±V（tarCtE）。 而且我们VCVC定义：• 属性集函数attrG：VG→2EG对每个顶点v∈VG返回具有源v的属性边的集合;• 消息集函数msgG：VG→2EG为每个顶点v∈VG返回具有目标v的消息边的集合。• 扩展属性集函数，attr：V→ 2 E，其中attr（v）={e∈E|C Clab（e）= attr<$src（e）∈ ↑v}，↑v是v的所有超类的集合。• 扩展消息集函数msg：V→2E，其中msg（v）={e∈E|MSG|tar（e）∈ ↑veJ∈E|msg：tar（eJ）∈↑v<$eJ±Ee}。C类型图反映了面向对象范式中属性和方法的继承它们是在类模型图上类型化的普通超图。然而，类型态射比传统态射更灵活[3]：一个C-A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101105VCVEEEEEE2ECE类型图边e可以关联到任何C-类型图节点v，只要它的类型边tE（e）（在C中）关联到节点类型vJ（也在C中），使得tV（v）和VJ在继承顺序关系下连接（即，tV（v）±ΔvJ）。 这定义反映了这样一个事实，即一个对象可以使用属于以下之一的任何属性：它的原始类，因为它是在类被特殊化时继承的。扩展属性集函数返回所有属性弧的集合，其源是v或v通过继承关系连接到的任何其他顶点±0.001。扩展的消息集函数将所有消息返回到指定的类型可以接收。请注意，对象内的消息重新定义（由优先关系在类模型图上，考虑，因为只有重新定义的方法可以在专门化类的作用域中看到。对C-型图G，t，C ∈ G，设全函数t∈：2 EG →2 EC 是将类型化功能扩展到边（或节点）集。 符号t|msg和t|attrE E将被用来表示应用的t到只包含消息的和属性（分别）超弧。 现在我们可以给出一个定义图表示一个面向对象的系统。定义2.4[面向对象图]设C是类模型图。一个C型图<$G，t，C <$是一个面向对象图当且仅当图下面（在设置）通勤。如果对每个v∈VG，函数t∈ G，|attr（attrG（v））是注入图，GC是严格面向对象图. 如果t|attr（attrG（v））也是满射的，GC被称为完全面向对象图。EG，，msgG_t*|MSG.V_GtV.属性GEG_t*|attrJ消息J属性J2EC，，.VC.2ECC在定义2.4的图中，左边的方块确保了消息边只能指向一个对象，如果它是在应用于对象类型的扩展消息集函数返回的一个边上键入的这意味着只允许输入消息所属的重定义链中最少的消息。这与动态绑定的概念是兼容的，因为任何对象实际调用的方法都是由特定计算中出现的实际对象确定的状态 所有t的内射性|attr（attrG（v）），v∈ VG，表示所有属性弧都是不同地键入（即，对象没有超出属性）。满射性意味着类模型图中所有层次上定义的所有属性（通过节点上的继承关系）都存在。一个完整的面向对象图的定义与面向对象框架中的继承概念是一致的，因为一个对象从它的原语类继承了所有的属性例2.5图2显示了一个完整的面向对象的图，它是在图1中描述的类模型图上键入的。让康德、黑格尔和尼采这三个要素成为右撇子哲学家，而其他要素就像它们的名字所表明的那样被类型化。根据类型类模型图，右撇子哲学家根本没有属性，也不会收到消息。2106A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101左叉右叉所有者所有者表ISAT左叉右叉ISAT左叉右叉黑格尔叉3叉1叉2VC121212，，E？REGV思维康德思维尼采ISAT图2.哲学家用餐问题的初始图sage键入的是Thinking。然而，由于它的父类Philosopher有那些弧连接到它，它们可以连接到任何派生对象，从而允许元素的继承。要明白这一点，考虑一下右撇子哲学家康德的属性isAt它被键入变形映射到的边ism有一个Philosopher类的元素作为源，所以（tsrcG）（isAt）=右撇子Philosopher±VPhilosopher=（srcCtE）（isAt），态射是允许的。C型图之间的关系可以用态射来描述.定义2.6[C-型图态射]设GC= G1，t1，C GC=设G2，t2，C n是在同一类模型图C=NV±上型化的两个C-型图，E±，L，src，tar，lab. 一个C型图态射h：GC→GCGC之间和GC，是一对偏函数h=HV：VG→VG2，hE：EG1→EG2，使得下图（在类别SetP中）对所有元素v∈dom（hV）进行了交换，（ t2V<$hV）（v）±VCt1V（v），以及所有的线性项tse∈dom（ hE），（ t2E<$hE）（e）±ECt1E（e）. 如果对所有元素e ∈ dom（h E），（t2 E<$h E）（e）= t1 E（e），则称态射是严格的。E_G1srcG、tarGH zdom（hE）H.艾薇！_2srcG、tarG1 1 2 2JhJVG1G2图态射是一种保持超弧源和目标的映射类型化图态射也保留（节点和边）类型。然而，普通的类型图态射[3]不能正确地描述面向对象系统上的态射，因为对象之间存在的继承关系使得某种类型的对象的动作对从它派生的所有对象都有效，因此，一个对象可以被看作不是唯一类型的，而是有一个类型集（即通过继承关系连接的所有类型的集合）。定义一个与底层顺序关系兼容的图态射确保了多态性可以一致地应用。面向对象系统的行为（方法的实现）将是思维V1A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101107获取获取叉修得所有者释放分离叉所有者哲学家叉哲学家哲学家叉叉表表哲学家表表叉所有者图3. 用餐哲学家问题的叉子通过规则建模，其中左侧和右侧是面向对象的图形。除了结构限制（由于规则是C型图态射的事实而强加的）之外，其他一些限制是必要的，以确保与对象范式的概念的兼容性特别地，规则左侧包含消息类型的恰好一个每个规则表示对在该过程中消费的消息的对象反应。这种需求不会造成不合理的限制，因为系统可能有许多规则指定对同一类型消息的反应（非确定性），并且如果它们的触发器存在于实际状态并且引用的规则不冲突，则许多规则可以并行应用[6]。在规则的左侧将允许最多一个具有属性的对象，以及该相同对象必须是上述消息的目标的要求。这种限制实现了信息隐藏的原则，即对象的内部配置（实现）只能是可见的，因此只能由其自身访问。规则态射必须是可逆的，以确保对象的类型不会随着计算而改变。最后，两边的边之间必须有一个双射，因此对象不会随着计算的发展而获得或失去属性。面向对象图文法由类模型图、初始状态（一个完整的面向对象图）和一组面向对象规则组成例2.7哲学家就餐问题的面向对象的图文法如图3、4和5所示。所有面向对象的规则（左侧和右侧）都是在图1所示的类模型图上类型化的面向对象图。然而，为了使表示更清晰，所有节点和边都以其类型命名，从而使类型态射显式。面向对象的图文法的语义是基于规则应用的。匹配和直接派生的定义方式与单推出方法相同：匹配是完全C型图态射，直接派生是面向对象图及其态射范畴中的匹配和规则箭头的推出[9]。我们没有使用通常的转换系统，而是使用从系统的初始图开始应用规则（状态是图，转换是图态射），我们定义了一个基于以下的抽象语义：108A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101吃RHP第一岔路获取修得RHP第二岔路右叉左叉右叉左叉获取修得吃左叉RHP开始进食右撇子哲学家叉叉叉叉叉叉右撇子哲学家右撇子哲学家叉叉t（o）Gt（o）G右撇子哲学家右叉右撇子哲学家右叉左叉释放吃右叉停止进食思维左叉右叉ISATISAT释放思维停止思考吃哲学家哲学家表哲学家哲学家表叉叉叉叉图4. 哲学家用餐问题的哲学家右撇子哲学家左叉图5. 右撇子哲学家规则的哲学家吃饭的问题。意见。这种语义保存了系统中发生的事件的信息因此，尽管我们不能基于对象状态来表达属性，但我们仍然可以基于对象如何响应应用于它们的规则来研究对象的属性。抽象语义是由一个标记的转换系统，它的状态是由语法中的规则应用程序生成的图形，两个状态之间的转换被标记的规则的名称一起应用的对象标识规则被应用。定义2.8[面向对象的图语法转换语义]设G=C，P C，C是一种面向对象的图文法。G 的变迁语义由标号变迁系统TG=<$S，s0，L，→ G给出，其中S ={GC|IC<$$>GC}是状态集，s0 = IC是初始状态，L={<$p，o <$∈PC×VG|G∈STp∈E}，是标签的集合，其中，是语法集，可以应用于类型tG（o）的对象的产生式，→是转移关系，并且面向对象图GC和HC在→下相关，如果存在面向对象图产生式r：LC→RC∈PC，则面向对象匹配C C Cr，mCm：L→G使得G你好A.P. L Ferreira等人理论计算机科学电子笔记175（2007）1011093翻译SPIN [10]的输入语言是Promela（PROtocol/PROcess Meta LANGUage），这是一种用于建模状态转换系统的专用语言。在面向对象的图形语法中，继承、多态和动态绑定将被编码在Promela中，而Promela最初并没有任何面向对象的特性。完整的翻译算法[7]相当长，将在这里非正式地介绍。对象被建模为Promela进程，对象之间通过异步通信通道进行消息交换。为了克服Promela中缓冲通道的FIFO策略，使用了与[5]相同的解决方案：使用本地缓冲器来继承关系显示为对任何程序元素可见的全局数组。子类多态性是通过这个数组中的一个约束来编码的，以确保只有当匹配的元素正确相关时才发生规则匹配动态绑定是作为每个对象进程定义中的消息调度过程来实现的与经典的面向对象编程语言实现[14]不同，其中虚拟表确定在执行时应该调用哪个方法，我们的方法使用了一点计算反射[17]，在这个意义上，每个对象（进程）都知道自己的类型，并且当其他实体访问对象时，这些信息可以被其他实体使用（作为属性或消息参数）。因此，对象可以在运行时根据消息接收者的实际类型决定要发送的适当消息。每个初始图节点被转换成一个过程，其属性的所有目标作为参数（使用施加在每个对象属性上的任意总顺序）。每个初始消息连同其参数（每个消息的源在初始图中）被放入适当的对象通道中因此，属性边的目标成为过程参数，消息参数成为过程局部变量。一个进程代码（对象行为）由一个无限循环组成，它不断地（非确定性地）测试一个新的消息是否已经到达对象主通道（在这种情况下，该消息被检索并放置在本地消息缓冲器的某个空槽中），或者是否有是本地缓冲器中等待使用的消息。在后一种情况下，消息从缓冲器中原子地检索，并应用它所引用的产品。如果对象通道和本地消息缓冲器都不包含任何要消费的消息，则进程将跳转到主循环的开始，并保持阻塞状态，直到新消息到达。匹配过程测试（i）是否所有属性都被正确地键入，以及（ii）是否所有属性值都是正确的。例如，考虑图3中的第一条规则。只有当属性顶点（Fork类型）的持有者是一个类型为Table的对象时，此匹配才可能。如果它是一个哲学家，则不会发生匹配，因为这两个元素没有继承关系（尽管它们都派生自ForkHolder）。类型测试是通过检查上述全局继承数组来执行的现在，考虑来自同一图的第二条规则。只有当作为消息Release的参数传递的Philosopher是110A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101拿着叉子的那个因此，在作为不同弧的源或目标的对象之间进行相等性测试。选择应用哪种生产是通过对所有存在匹配（对于接收到的消息）的规则进行条件测试来执行的。由于Promela中的条件测试在多个条件为真时具有不确定性结果，因此应用哪个产生式的选择也是不确定性的，正如语法语义所要求的那样。规则应用可以被描述为：（i）对象属性根据规则态射被修改;（ii）全局变量事件RuleName被设置为所应用的产品名称;（iii）对于产品属性顶点的类型通过继承而与之相关的所有类，变量事件x的集合被设置为对象标识;（iv）最后，创建出现在应用产生式的右侧的所有消息，并且这是特别相关的，因为正是该过程执行动态绑定。执行步骤（i）至（iii）而不生成中间状态，以确保属性验证的正确性。如果没有应用任何规则（因为对于实现接收到的消息的任何生产都不可能有匹配），则消息被放回本地缓冲器中，并标记为已检查。在新消息到达之前，不会检索已检查的消息以供应用。由于只有对象可以更改自己的状态，因此只有在实际应用另一个产品之后，才能匹配此消息。这一过程还有助于减少验证过程的程序状态空间。要发送的正确消息取决于接收消息的实际对象的类型。由于任何节点的低层集合（根据继承层次）是有限的，并且不会随着程序的执行而改变，因此条件结构会照顾它。例如，考虑图4中的第二条规则。一个信息吃被发送到一个哲学家。然而，这个消息被所有Philosopher子类重新定义，所以必须知道元素类型才能发送正确的消息。生成的代码由以下伪代码说明：if（接收对象消息通道未满）if. 接收对象类型是哲学家->发送消息为哲学家. 接收对象类型是Left-HandedPhilosopher -> send消息Eat for the Left-HandedPhilosopher. 接收对象类型是Right-HandedPhilosopher -> send消息Eat for the Right-HandedPhilosopher整个规则应用过程是原子地执行的。因此，从消息从本地缓冲器取出到规则应用完成（通过应用规则或将消息放回本地缓冲器，如果不存在与该规则匹配的话），由于原子关键字，没有其他进程可以与该执行交错。 规则应用程序过程是必要的，以模仿规则在图形语法中的应用方式其中整个匹配和应用过程在单个步骤中执行。此外，如果允许交错，则可能出现错误：如果在为产生式查找匹配和应用该产生式之间停止了进程，则同时状态图可能以改变规则应用的方式被改变。A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101111不可能;因此匹配/应用程序被认为是任何对象行为的关键区域。4验证SPIN中的属性验证可以使用多种方法来完成，其中有LTL [11]属性验证。验证哲学家用餐问题的有意义的事件可以被描述为，例如，我们将使用已经提出的面向对象的图形语法的哲学家用餐的问题作为运行的例子。由于篇幅的原因，我们将只验证活性属性，即“任何时候哲学家决定吃，他最终都会这样做”。我们将证明这个属性在所提供的模型中是假的。SPIN执行基于模型的验证，这意味着属性只能在状态上定义，而不能在转换上定义。我们提出的翻译定义了一组全局变量，以允许对事件进行验证：（i）属于类模型图的每个类的一个全局变量，语法在该类模型图上被类型化，以标识该类型的最后一个对象，该对象具有应用于它的产生式（如果消息被对象接收，并被某个规则应用程序使用，则对象标识被分配给相应的变量），以及（ii）一个全局变量，用于标识应用了哪个规则，并且它在每次发生这样的动作时被更新。请注意，规则应用并不等同于消息使用。虽然每个规则应用程序都精确地对应于对接收到的消息的响应，但是可以有多个（不同的）规则实现针对相同类型的消息的操作如果有兴趣验证规则可以应用的可能顺序，则此变量是必需的XSpin工具允许使用预处理器宏#define以类似C的方式定义命题。这些属性可以根据属于系统初始图的实际对象 因为我们只对哲学家的行为感兴趣，所以一个用来识别每个哲学家的命题被定义为#define isKant（事件哲学家==康德）。感兴趣事件的命题#define aPhilWantsToEat（事件RuleName ==规则Philosopher StopThinking）或#defineaPhilStartsToEat（事件RuleName==规则PhilosopherStartsEating）。为了发现一个已知的事件是否发生在一个特定的对象上，可以定义诸 如 #define philKantWantsToEat （isKant aPhilWantsToEat ） 和#definephilKantStartsToEat（isKant aPhilStartsToEat）使用上面定义的命题，可以写出关于系统行为的LTL性质“<<哲学家在任何时候决定吃东西，他最终都会这么做”的性质可以表述为[]（philKantWantsToEat− > > philKantStartsToEat），其中符号>和[]代表通常的线性时间逻辑量化器Q（ 最 终 ） 和 Q （ 总 是 ） 。 对 于 所 有 哲 学 家 来 说 ， 它 可 以 表 述 为 []（ （ philKantWantsToEat−><>philKantStartsToEat ） && （ philHegel-WantsToEat−><> philHegelStartsToEat）&&（philNietzscheWantsToEat−>112A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101图6. 没有死锁属性<>philNietzscheStartsToEat））.最后一个属性在所提供的模型中不为真。图6显示了一个图形化的反例（取自模型检查器的输出，并由[4]中开发的系统生成）。反例显示了三位哲学家（尼采，黑格尔和康德）及其各自的分支。进程由水平线表示，箭头表示到达和离开每个进程的消息请注意，设置了一个死锁情况：每个哲学家都抓住了一个fork，并向另一个fork发送了一条消息试图获取它。不能再被应用，所有的哲学家都将永远等待。5结论面向对象的图文法为面向对象的系统提供了一个基于图的规范框架，其中特殊的偏序表示继承和覆盖层次结构，使多态性和动态绑定成为形式主义的内置我们已经提出了一个（草图）从面向对象的图形语法规范到Promela程序的翻译。所有面向对象的特性都被转化为Promela：继承表现为一个全局数组;多态性通过对该数组的检查在匹配过程中实现;动态绑定通过消息调度机制实现，该机制检查消息接收者类型以确定要发送的正确消息;信息隐藏和A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101113封装在转换时自然出现，因为单个进程实现每个系统对象。图规则应用程序的转换在规则可以被应用之前建立匹配的存在，并且消费哪个消息和应用哪个产生的选择是不确定的，如所定义的语法语义所要求的。我们目前没有处理对象的创建和删除，但它是对这种翻译的直接扩展，目前正在自动化（使用基于XML的语言GXL和GTXL的扩展[18]）。可以进行扩展以定制到应用特性的转换，以便减少所产生的状态空间。建议的翻译可以说是语义上的声音，在这个意义上，没有图形系统的行为是删除或介绍的翻译。即使在Promela程序中存在不对应于属于语法语言的任何图的状态，如果这些状态不是规则应用程序的一部分，则始终可以翻译这些状态。如果它们是，它们不能与任何其他进程执行交错，因为规则应用是原子地执行的，因此它可以将Promela状态的原子块转换为图形状态。这一翻译正确性的正式证明正在准备出版。最后，我们使用了一个哲学家用餐问题的模型来说明如何进行验证，以及如何使用我们的方法发现错误。引用[1] Baldan ， P. ， A. CradiniandB. Kéonig ， Verifyingfinite-stattegraphgramma r s ： A n unfold i ng-basedapproach，in：CONCUR，2004，pp. 83比98[2] 伯 卡 特 岛 和 Y.- M. Quemener ， Model-checking of infinitite graphs defined by graph grammars ，TechnicalReport995 ， IRISA-InstitutdeRecherchenInformiquetSyst`emesAl′eatoires ， Rennes（1996）。[3] Corradini ， A. ， 联 合 Montanari 和 F. Rossi ， Graph processes ， Fundamentae Informatica26（1996），pp. 241-265[4] 我的天啊！M.，“V e ri fic aerodeca o Foro r m al d e S i s t e m as D i s t r i b o s M o d e l a d o s n a G r a m'at i c d e G r a f o s B a s e a d a e m O b j e t o s，”M a s t e r s t h e sis，P o n t i f's a c ia U n i v e r s i d e C a to li c o R i o G r and e d o Su l，P o r to Alegre（2004），89 p.[5] Dotti，F. L.，L.福斯湖Ribeiro和O. M. Santos，基于对象的分布式系统，在：E. Najm ， U.Nestmann 和 P.Stevens ， editors ， Proceedings of the 6th IFIP TC6/WG6.1InternationalConferenceonFormalMethodsforOpenObject-BasedDistributedSystems（FMOODS 2003），LectureNotes in Computer Science2884（2003），pp.261-275。[6] H.，R.H eckel，M. Koro，M. 卢韦湖 Ribeiro，A. 我是一个人。在此基础上，提出了图变换的一般方法. 第二部分：单推出方法和与双推出方法的比较，，1（基础），世界科学，新加坡，1996年，页。247-312[7] 费雷拉A.P. L.，[8] 费雷拉A. P. L. 和L. 面向对象的图形和语法，E。Najm，联合Nestmann和P. Stevens，编辑，第6届IFIP TC 6/WG6.1开放式基于对象的分布式系统的形式化方法国际会议论文集（FMOODS 2003），计算机科学讲义2884（2003），pp. 16比31[9] 费雷拉A.P. L. 和L.面向对象图文法中的推导，H.Ehrig，G.恩格斯，F. Parisi-Presicce 和 G.Rozenberg ， editors ， Proceedings of the 2nd International Conference onGraph Transformations（ICGT 2004），Lecture Notes in Computer Science3256（2004），pp.416-430114A.P. L Ferreira等人理论计算机科学电子笔记175（2007）101[10] Holzmann，G. J.，SPIN，IEEE Transactions on Software Engineering23（1997），pp. 1比17[11]Huth，M.R. A. 和M.D. Ryan，[12] Koch，M.，“Integration of Graph Transformation and Temporal Logic for the Specificationof Distributed Sys t em s“，P h D The sis，T e chn i sch e Universit？t Berlin，Berlin（1999）。[13] L？we，M.，“Extende d A l gebr a i c G r ap h T r an s for m at i on，“P h. D. Thes is，Techni schennUniversitéattBerlin，Berlin（1991）.[14] Pratt，T. W.和M. V. Zelkowitz，[15] Rensink，A.，关于模型检验图文法，M. Leuschel，S. Gruner和S. L. Presti，editors，Workshop onAutomated Verification of Critical Systems（AVoCS）（2003），pp. 150-160.[16] Rensink，A.， GROOVE模拟器：状态空间生成工具，见：J. Pfalz，M. 纳格尔和B. Büohlen，editors，ApplicationsofGraphTransforrmartionswithithIndustrialRelevance（AGTIVE），Lecture Notes in Computer Science 3062（2004），pp. 479-485[17] 史密斯湾，澳-地C.的方法，“Reflection and Semantics in a Procedural Language,” PhD Thesis,Massachusetts Institute of Technology, Cambridge, MA[18] Winter，A.，B. Kullbach和V.GXL图形交换语言的概述，在：S。Diehl，编辑，软件可视化国际研讨会，计算机科学讲义2269（2001），pp. 324-336