基于对象的图形语法及其在分布式系统规范中的应用

理论计算机科学电子笔记109（2004）125-136www.elsevier.com/locate/entcs基于对象的图形语法1Osmar Marchi dos Santos2，Fernando Lu 'ıs Dotti3FaculdadedeInforma'ticaPontif<$ıciaUniversidadeCatoo<$licadoRioGrandedoSulPorto Alegre，Brazil莱拉·里贝罗4InstitutodeInforma'ticaUniversidade Federal do Rio Grande do Sul巴西阿雷格里港摘要基于对象的图文法（OBGG）是一种适合于分布式系统规范的形式语言。在以前的工作中，定义了从OBGG模型到PROMELA（SPIN模型检查器的输入语言）的翻译，从而能够使用SPIN验证OBGG模型。本文建立在这些结果的基础上，我们扩展了属性指定的方法，并定义了一种将PROMELA迹解释为OBGG推导的方法，为OBGG模型不正确的属性关键词：图文法，模型检测，可视化的痕迹。1介绍在[7]中，定义了一种适用于指定分布式系统的可视化形式规范语言该语言是对图语法的限制，称为基于对象的图语法（OBGG）。目前，OBGG中的模型可以1这项工作得到了HP Brasil-PUCRS协议CASCO（第32 TA）、PLONIC（CNPq）、IQ-Mobile II（CNPq/CNR）和DACHIA（FAPERGS/IB-BMBF）研究项目的部分支持2电子邮件地址：osantos@inf.pucrs.br3电子邮件地址：fldotti@inf.pucrs.br4 电子邮件地址：leila@inf.ufrgs.br1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.061126O.M. dos Santos等人理论计算机科学电子笔记109（2004）125通过模拟[5]和验证[6]进行分析。此外，从OBGG模型开始，我们可以生成在真实环境中执行的代码，然后直接映射到Java [5]。我们还研究了一种方法来考虑分布式系统的经典故障模型，允许在存在选定故障的情况下对给定模型进行推理[8]。通过使用上面提到的方法和工具，我们定义了一个框架来帮助分布式系统的开发。该框架的创新之处在于使用了与底层统一形式主义相同的形式规范语言（OBGG）。在 [6] 中 定 义 了 一 种 验 证 OBGG 的 方 法 ， 其 中 OBGG 模 型 被 翻 译 为PROMELA，SPIN模型检查器的输入语言。这种方法的一个重要方面是属性（待验证）在OBGG模型上指定，而不是在转换的PROMELA模型上指定。所提出的方法只考虑事件上的属性（在OBGG的情况然而，系统的互补方面可以通过使用状态上的属性来指定。此外，SPIN中的反例是在PROMELA模型翻译后自动生成的，因此对OBGG模型没有相应的意义。本文的主要贡献是：（i）扩展了属性指定方法以考虑对象的状态;（ii）定义了一种方法来为OBGG模型不正确的属性生成图形反例。本文的结构如下：第2节介绍了OBGG和SPIN的概述;第3节简要解释了[6]中定义的OBGG模型的翻译，并介绍了本文的贡献（i）和（ii）;第4节给出了结论，相关工作和未来的工作。2背景在本节中，我们简要介绍OBGG和SPIN模型检查器。2.1基于对象的图文法图表是一种非常自然的手段，可以直观地解释复杂的情况。图形规则可以补充用于捕获系统的动态方面。由此产生的图文法概念将Chom- sky文法从字符串推广到图[14].图文法的基本概念是，系统的状态可以用图（系统状态图）表示，并且从系统的初始状态（初始图）开始，规则的应用连续地改变系统状态。在这里，我们将使用图语法作为分布式O.M. dos Santos等人理论计算机科学电子笔记109（2004）125127系统.这种系统的构造将按组件进行：每个组件（称为实体）被指定为一个图语法;然后，整个系统的模型通过组合指定组件的实例来构造（该模型本身就是一个图语法）。我们将使用基于对象的图语法（OBGG）[7]，而不是使用一般的图语法来指定组件。 这种选择有两个优点：在实践方面，规范是以大多数用户非常熟悉的基于对象的风格完成的，因此易于构造，理解并因此用作实现的基础;在理论方面，限制保证语义是组合的，降低匹配的复杂性，以及简化语法分析OBGG是图文法的一种限制形式，顶点，以及表示基于对象的概念的规则的配置。一个OBGG由一个类型图、一个初始图和一组规则组成（见图1）。类型图实际上是将在此语法中使用的（图形）类型的描述（它指定了类型可能的实体、消息、属性和参数一个实体在对一条消息作出反应时的行为是由一个（一组）规则定义的。因此，规则的左侧总是指定由特定实体接收消息。在右侧，该消息被消费，应用规则的效果被定义。该结果可以是：属性值的改变;对象（实体的实例）的创建;和/或新消息的生成。初始图指定系统的起始状态。2.1.1例如在本节中，我们使用OBGG对读者和作者问题进行建模。组成规范的对象的类型图、初始图和规则如图1所示。读者和作者问题由一个资源和两种过程（读者和作者）组成。读取器和写入器进程可以在资源中执行、读取和写入操作，重新启动。为了在资源中保持一致的状态，每个写操作必须对资源具有独占访问权。读取器进程可以在资源中并发执行读取操作，前提是没有写入器进程正在访问该资源。5图形符号：在图1（a）中，矩形是顶点，圆圈内的数字是这些顶点的名称（这些符号用于指示图1（b），（c）和（d）中每个顶点的类型顶点内的列表是顶点属性。图1中出现的消息符号是超弧。128O.M. dos Santos等人理论计算机科学电子笔记109（2004）125在我们对问题的建模中，定义了两个实体（图1（a））：资源和过程。Resource实体表示资源，它有两个属性来跟踪访问资源的读取器（nr）和写入器（nw）的数量。Proc实体代表读者和作者，拥有一个id（标识）和一个对资源的引用（res）。Resource对象的规则如图1（c）所示，Proc对象的规则如图1（d）所示。资源对象可以接受读操作（规则ReqRead）和写操作（规则ReqWrite）的请求。如果一个读操作被接受，它最终会完成（规则FinRead），向发送请求的Proc写操作也是如此（规则FinWrite）。Proc对象具 有循 环行 为 ，即 在从 Resource 接 收到 操作 的 确认 （规 则EndRead 和EndWrite）之后，Proc对象开始新的操作（规则StartRead和StartWrite）。在图1（b）中，给出了一个由一个Resource对象、两个Proc2.2自旋SPIN模型检查器[10]是一个验证并发软件系统的工具 SPIN的输入语言是PROMELA。SPIN中的属性规范使用线性时序逻辑（LTL）定义。除了作为模型检查器，SPIN还可以用作模拟器。SPIN的模拟特性，除其他外，用于模拟对于给定模型为假的属性的反例（跟踪）。由SPIN生成的反例由PROMELA模型的语句组成，这些语句的变量由模型的当前状态的值PROMELA具有类似C的语法和结构，用于接收/发送类似于通信顺序进程（CSP）的消息。该语言是基于进程的，进程可以通过同步和异步消息通道以及全局变量交换信息非确定性是使用条件和重复结构建模当在SPIN中指定属性时，用户需要在PROMELA模型上定义原子命题。定义原子命题的一种可能性是使用全局变量。这导致需要将属性插入到将用于验证的全局变量中3使用SPIN在本节中，我们介绍了OBGG模型翻译的主要特点。我们描述了属性是如何建模的，并提出了一个扩展的属性指定方法来考虑对象的内部状态O.M. dos Santos等人理论计算机科学电子笔记109（2004）125129(a)（b）第（1）款（c）第（1）款（d）其他事项图1.类型图（a）、初始图（b）和规则（c）和（d）。（第3.2节）。最后，在第3.3节中，我们介绍了一种方法，用于生成图形反例，PROMELA跟踪，这是有意义的OBGG用户。3.1翻译概述在[6]中定义的转换中，OBGG对象被映射到PROMELA过程（我们称之为对象过程）。组成对象过程的变量是相应对象的属性。出于验证目的，OBGG对象的属性仅限于PROMELA支持的类型。OBGG消息被转换为PROMELA消息。消息的接收是通过异步通道完成的，称为对象进程通道，也用作对象进程的引用。OBGG对象的规则是130O.M. dos Santos等人理论计算机科学电子笔记109（2004）125映射到对象进程内部的条件结构。此结构在其条目中具有触发对象规则的必要条件对象之间的并发性自然由对象进程之间的并发性来保持。PROMELA通道的使用有两个方面需要考虑：（i）在OBGG中，对象处理的消息不保持顺序-而PROMELA通道保持顺序;（ii）在OBGG中，对象在每个时刻可以接收无限数量的消息- 在PROMELA中，通道具有最大数量的消息，并且如果通道已满，则对通道的后续写入将与同一通道上的实际读取同步。为了处理（i），每个对象都有一个内部通道，用于以非确定性的方式处理存储的消息。为了处理（ii），我们插入了断言，在发送消息之前，评估表达式以确定目的地通道是否未满。因此，当验证模型时，当对象处理通道满时可能产生错误，从而要求用户增加缓冲器大小。对象进程的一般行为如下：（i）在对象进程通道中等待新消息;（ii）一旦接收到新消息，就将它们发送到对象进程的内部缓冲器;（iii）从内部缓冲器非确定性地选择消息，并尝试应用规则来处理该消息;（iv）在对象进程通道中等待新消息。a）如果消息被处理并且对象处理通道为空，则返回到（iii）;（iv.b）如果没有消息被处理或对象处理通道不为空，则返回（i）。OBGG初始图由模型的对象实例和消息组成。 初始图在PROMELA中成为一个init进程。这初始化过程具有三个阶段：（i）为出现在初始图中的对象创建对象处理通道;（ii）执行在初始图中定义的对象处理;（iii）使用对象处理通道发送初始消息。关于这种翻译的更多细节可以在[6]中找到，包括对生成的PROMELA模型和原始OBGG模型的语义兼容性的讨论。3.2物业规格基本上，在文献中，我们可以确定两种互补的方法，用于指定有关模型执行的属性，一个基于事件，另一个基于状态。为了将这些方法与OBGG一起使用，我们可以将规则的应用视为事件，并将从规则的应用中获得的图形视为状态。在[6]中，我们提供了一种基于OBGG事件这将在第2.1节中更详细地介绍第3.2.1条。在第3.2.2节中，我们提出了一种考虑对象内部状态的属性验证方法。O.M. dos Santos等人理论计算机科学电子笔记109（2004）125131→||3.2.1关于事件当在SPIN中指定转换后的OBGG模型的属性时，我们必须考虑SPIN是一个基于LTL状态的模型检查器。为了指定基于事件的属性，我们必须通过全局变量提供属性指定中使用的事件的名称。在我们使用事件的方法中，从transla-tion生成的每个PROMELA模型都有一个称为事件RuleName的全局变量。此变量的类型是符号名称的枚举，其中包含组成模型的OBGG规则的名称。因此，当应用规则时，规则的名称被原子地写入事件RuleName全局变量，即，所应用的规则的名称在模型的当前状态中可见使用这种方法，可以编写关于规则（事件）发生的LTL公式，其中，对于翻译的PROMELA模型，事件是事件RuleName全局变量的值的变化。使用SPIN指定事件属性的想法已经在[1]中进行了探索。例如，我们可以将事件ReqRead（参见图1（c））定义为变量事件RuleName的值从not ReqRead更改为ReqRead（其中ReqRead是应用的规则）。我们使用下一个时态运算符（X）来标记值的变化，生成公式（！ReqReadX ReqRead）。作为该方法的一个例子，我们可以定义一个LTL公式来指定用OBGG建模的读者和作家问题的互斥属性。为了使用规则的应用指定属性，作为事件，我们需要推理用于表示被指定的属性的规则应用的顺序（次序）。为了表示互斥属性，我们必须确保在执行写操作时从不执行读或写操作请求（规则ReqRead和ReqWrite）。写操作的特征在于请求（规则ReqWrite）和确认（规则FinWrite ）。此外，互斥属性被定义为EndWrite3））。 我们能够验证此公式，从而从SPIN中获得假值。由此证明了模型中特定Proc对象饥饿从SPIN中获得的反例对应于一个文件，其中PROMELA模型（转换的OBGG模型）的行具有由模型当前状态值在下一节中，我们使用获得的O.M. dos Santos等人理论计算机科学电子笔记109（2004）125133反例，为这个公式，以说明的方法，产生图形反例是有意义的OBGG用户。3.3反例的生成在分布式系统的文献中，一种被广泛接受的用于查看分布式系统执行的图形形式基于进程之间的消息交换。这种方法包括为组成系统的每个过程定义一个时间线。通过显示进程发送/接收的消息（通过标记的弧线），时间向下增加。由于OBGG专注于分布式系统的规范，因此使用与所描述的图形表示类似的图形表示对于使用消息传递抽象的用户来说具有直观的然而，只显示消息的交换并不能捕捉OBGG的另一个重要抽象，即规则的应用。为了在OBGG模型的图形执行视图中考虑规则的应用，我们可以将关于规则应用的信息添加到组成系统的每个对象的时间线。此信息包含应用的规则的名称，每当对象执行规则时都会添加此信息作为这种方法的一个例子，从SPIN中得到的关于3.2.2节中验证的性质的反例如图2所示。对于模型的每个对象，定义一个由对象名称标识的时间线。时间向下增加，消息通过标记的弧线显示。对象执行的规则显示在对象时间线的右侧。此执行显示了对象Proc3在资源（规则StartWrite）中发出从未执行的写操作的情况，因为Proc4写操作在模型中经常被执行。当在执行中检测到无限循环时，图形中会显示短语START OF CYCLE。图2中的图形是通过过滤从SPIN获得的反例由于从OBGG到PROME-LA的转换的固有特性，在PROMELA模型中，消息没有唯一的ID（标识符），这是OBGG中可用的信息。因此，当多个具有相同类型和相同属性的消息被发送到同一对象时，无法识别哪些相同的消息触发了对象中的虽然可以用这些反例进行所需的分析，但在某些情况下，可能无法分析事件之间的因果关系。134O.M. dos Santos等人理论计算机科学电子笔记109（2004）125图2.从SPIN获得的反例的图形视图4最后发言在本文中，我们解释了如何使用事件（规则的应用）来指定OBGG模型验证的属性。在此基础上，我们定义了该方法的扩展，以考虑使用对象的内部状态来指 定 本 文 的 第 二 个 贡 献 是 定 义 了 一 个 图 形 布 局 ， 它 对 OBGG 用 户 查 看PROMELA反例有意义。O.M. dos Santos等人理论计算机科学电子笔记109（2004）125135为了使用模型检查工具，在形式语言之间进行转换和集成正在成为一种常见的做法，因为很多时候，重用比构建特定的验证工具更容易（也更有效）我们可以在文献中找到各种各样的作品，使用视觉和非视觉语言，专注于基于对象/面向对象系统的验证在文献中，当我们关注非视觉语言的验证时，我们发现了像[4，3，13，9，16]这样的作品。更具体地说，[4，3，9]中提出的工作旨在验证受限Java程序，其中Java程序被翻译为SPIN模型检查器的输入语言。尽管这些工作处理Java程序的验证，[13]通过考虑Actor并发模型扩展了PROMELA（SPIN的输入语言），为了模型检查基于对象的分布式系统。在[16]中，引入了形式规范语言Object-Z与ASM（抽象状态机）的集成，创建了OZ-ASM符号。经过一系列翻译后，可以使用SMV工具验证OZ-ASM规格。对于视觉语言的验证，我们在文献中发现了以下作品[11，12，15]。[11]中提出的工作定义了一种可视化和面向对象的语言（称为v-Promela），可以映射到SPIN模型检查器。属性规范可以在v-Promela模型上定义，而不是在翻译的PROMELA模型上定义，但是没有方法可以在v-Promela中使用SPIN可视化验证结果[12]提出了一种称为vUML的工具，它试图提供UML模型的自动验证。这种方法包括UML模型到PROMELA的映射使用该工具，可以验证UML模型的死锁、活锁、无效状态等[12]。此外，使用SPIN验证的反例与UML序列图。在[15]中，提出了一个模型检查可视化语言的框架。该方法背后的主要思想是，视觉语言可以建模为图转换系统。因此，有一种方法来验证一般的图形转换系统，它是可能的验证可视化语言。 的方式 来指定验证的属性，但我们无法找到如何使用该框架生成与考虑用于模型检查的语言之间的翻译的大多数类似方法使用主要的OBGG抽象。此外，我们有一个正式的证明我们的翻译的正确性，这是在文献中发现的大多数作品中找不到的。136O.M. dos Santos等人理论计算机科学电子笔记109（2004）125未来的工作包括定义语法的属性和实现的工具，用于验证OBGG使用的方法定义到目前为止。引用[1] Che chik，M. 和D. O. P.A.，Eventsin p ro p.A.，in：5thand6thInternationalSPIN Workshops，LNCS1680（1999），pp. 154-167。[2] 科普斯坦湾和L. Ribeiro，使用图文法的仿真模型，在：第10届欧洲仿真研讨会（1998年），pp.60比64[3] Corbett，J. C.例如，Bandera：Extracting Finite-State Models from Java Source Code，in：22nd International Conference on Software Engineering（2000），pp. 439-448[4] Demartini，C.，R. Iosif和R.陈晓，基于SPIN的Java多线程应用程序的建模与验证，第四届国际SPIN研讨会，北京，1998。[5] Dotti，F. L.，L. M.杜阿尔特湾Copstein和L. Ribeiro，移动应用的仿真，在：2002年通信网络和分布式系统建模与仿真会议（2002年），pp. 261-267.[6] Dotti，F. L.，L.福斯湖Ribeiro和O. M. Santos，基于对象的分布式系统的验证，第六届开放式基于对象的分布式系统形式化方法国际会议，LNCS2884（2003），pp. 261-275。[7] Dotti，F. L.和L. Ribeiro，Specification of mobile code systems using graph grammars，in：4th International Conference on Formal Methods for Open Object-Based DistributedSystems，IFIP Conference Proceedings177（2000），pp. 45比63[8] Dotti ，F. L. ，L. Ribeiro 和O. M. Santos， Specification and analysis of fault behavioursusing graph grammars ， in ： 2nd International Workshop on Applications of GraphTransformations with Industrial Relevance ， Lecture Notes in Computer Science3062（2003），pp.120-133[9] Havelund，K.和T.Pressburger，Model checking java programs using java path finder，Software Tools for Technology Transfer2（2000），pp.366-381.[10]Holzmann，G. J.，模型检查器SPIN，IEEE软件工程学报23（1997），pp. 279-295.[11] Leue，S.和G. Holzmann，v-Promela：一种面向对象的SPIN语言，第二届面向对象的实时分布式计算国际研讨会（1999年），pp. 14-23.[12] Lilius，J.和I。P. Paltor，vUML：a tool for verifying UML models，in：14th InternationalConference on Automated Software Engineering（1999），pp. 255-258[13] Mo Cho，S.例如，将模型检查应用于并发面向对象软件，在：第四届自治分散系统国际研讨会（1999年），pp。380-383[14] 罗森伯格，G.，编辑，[15] Vo，D.，陈文生，计算机科学与工程，2003年第2[16] 温 特 ， K 。 和 R.Duke ， Model checking Object-Z using ASM ， in ： 3rd InternationalConference on Integrated Formal Methods，LNCS2335（2002），pp.165-184。