基于对象的并发系统建模与分析工具的开发与集成研究

理论计算机科学电子笔记127（2005）3-13www.elsevier.com/locate/entcs基于并发对象的应用程序开发环境1，2费尔南多湖Dottia，3，Lucio M. Duartea，4，LucianaFossb，5，Leila Ribeirob，5，Daniela Russib，5，Osmar M.dos Santosa，3aFaculdadedeInforma'ticaPontif<$ıciaUniversidadeCatoo<$licadoRioGrandedoSulPorto Alegre，BrazilbInstitutodeInforma'ticaUniversidade Federal do Rio Grande do Sul巴西阿雷格里港摘要OBGG（Object-Based Graph Grammars）是一种形式化的规范语言，适用于对并发的基于对象的系统进行建模。在以前的工作中，我们主要讨论了语言以及OBGG中描述的系统的案例研究和分析技术（模型检查和仿真）。在本文中，我们提出了一套工具，我们已经开发和/或集成，以建立一个环境的并发基于对象的系统的开发。有了这个环境，我们支持使用OBGG指定的并发基于对象的系统的规范和分析保留字：编辑、验证、模拟、代码生成。1这项工作是与HP Brasil-PUCRS（CASCO 项目第32 TA）合作开发的，并得到了ForMOS（FAPERGS/CNPq）、PLONIC（CNPq）、IQ-Mobile II（CNPq/CNR）和DACHIA（FAPERGS/IB-BMBF）研究项目的部分支持。2姓名按字母顺序排列3电子邮件：fldotti@inf.pucrs.br，osantos@inf.pucrs.br4电子邮件：lucio. imperial.ac.uk，在伦敦帝国理工学院攻读博士5 电子邮件：lfoss@inf.ufrgs.br，leila@inf.ufrgs.br，russi@inf.ufrgs.br1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.12.0264F.L. Dotti等人理论计算机科学电子笔记127（2005）31介绍在[9]中，定义了一种适用于指定并发基于对象的系统的可视化形式规范语言。该语言本身是一个图形语法的限制，称为基于对象的图形语法（OBGG）。目前，OBGG中的模型可以通过验证[7]和模拟[6]进行分析。此外，从OBGG模型开始，我们可以生成在真实环境中执行的代码，然后直接映射到Java代码[6]。由于OBGG基于消息传递机制进行通信，并遵循异步计算模型，因此该语言也适用于分布式系统的规范。因此，为了处理分布式环境中常见的方面，例如容错，在[8]中，我们研究了一种方法来考虑分布式系统的经典故障描述（例如崩溃故障），允许在存在选定故障的情况下推理给定的OBGG模型通过使用上面提到的方法和工具，我们定义了一个框架来帮助开发并发（和分布式）基于对象的系统。该框架的创新之处在于通过一系列的方法和工具来支持相同的形式化规范语言（OBGG）。在本文中，我们提出了一套工具，我们已经开发和/或集成，建立一个环境的并发基于对象的系统的发展。该环境的主要模块是：（i）OBGG规范的编辑器;（ii）用于存储规范的数据库;（iii）从数据库读取规范的翻译器，生成用于验证和模拟的模型，以及用于在真实环境中执行的Java代码;（iv）使用SPIN模型检查器的接口[11];（v）从头开始构建的模拟工具。使用这个环境，我们支持使用图形语法指定的并发基于对象的系统的本文的组织如下：第2节显示了环境的体系结构;第3节介绍了形式化规范语言OBGG，以及OBGG编辑器工具的解释;第4节简要讨论了OBGG可用的分析方法（模型检查和仿真）以及在真实环境中执行的代码生成;最后，第6节为我们带来了结论和未来的工作。2环境建筑在本节中，我们将介绍用于开发使用OBGG建模的并发基于对象的系统的环境的体系结构。该环境由一组集成工具组成，其中每个工具添加一个F.L. Dotti等人理论计算机科学电子笔记127（2005）35规范验证模拟选项，结果选项，结果数据库型号：PZPLZYSPIN模拟器分析工具OBGG模型翻译验证模型翻译仿真模型验证翻译仿真翻译执行翻译翻译工具翻译Java程序、信息流未执行的职能支撑平台人机界面工具仿真验证编辑器环境的不同特征。该架构如图1所示，其中具有类似功能的工具被分组为特定模块。图1. 环境的建筑使用图1所示环境的第一步是使用编辑器指定系统，该编辑器负责将OBGG规范存储到数据库/从数据库恢复OBGG规范。编辑器是人机界面工具的一部分，人机界面工具也由验证和模拟界面组成。Verification接口允许在翻译的验证模型中验证属性的指定，并向用户展示验证结果[18]，目前已实现OBGG方面的反例生成，但尚未集成到环境中。仿真界面以图形方式向用户呈现仿真结果，目前尚未实现该工具。数据库的结构基于[17]中提出的结构。根据数据库中的定义，用户可以创建/编辑两种规格类型的规格，分类为用于验证或模拟的规格。由于SPIN（用于验证OBGG模型的模型检查工具）施加的约束，验证规范使用特定（受限）的数据类型集。 另一方面，仿真规范可以使用Java语言中的特性（可用类），因为PLCNET仿真工具是用Java编写的，并且支持这种规范风格。我们不为代码生成定义规范。这是因为在我们为真实环境生成代码的方法中，我们使用了模拟规范（参见4.3节）。在数据库中有一个规范，用户可以使用翻译工具来生成输入代码：分析工具，允许执行转换的OBGG模型的验证和模拟;和支持平台。6F.L. Dotti等人理论计算机科学电子笔记127（2005）3用于在真实环境中执行已翻译的Java代码的表单第4节讨论了翻译工具实现的翻译方法，以及分析工具和支持平台中使用的翻译方法3并发基于对象系统在本节中，我们首先介绍OBGG规范语言的主要概念。然后我们描述了编辑器工具，它允许创建和编辑OBGG规范。3.1基于对象的图文法OBGG [9]是图文法[16]在顶点种类以及表示基于对象的概念的规则配置方面的受限形式。OBGG规范由类型图、规则集和初始图组成。类型图实际上是将在此语法中使用的（图形）类型的描述。它指定了类描述的结构部分，包括可能的消息、属性和参数的类型。OBGG对象（类的实例）在对消息做出反应时的行为由一个（一组）规则定义因此，规则的左侧总是指定特定对象接收消息在右侧，该消息被消费，应用规则的效果被定义。该效果可以是：属性值的改变;新对象的创建;和/或新消息的生成。初始图指定系统（模型）的起始状态OBGG系统的构造是按组件进行的：每个组件（称为类）都被指定为一个图语法;然后，通过组合指定组件的实例来构造整个系统的模型（该模型本身就是一个图语法）。使用基于对象的风格的优点有两个方面：在实践方面，基于对象的风格对大多数用户来说都很熟悉，因此便于构建，理解并因此用作实现的基础;在理论方面，限制保证语义是组合的，降低匹配的复杂性，以及简化语法分析。3.2编辑器编辑器允许通过图形交互界面创建和编辑OBGG规范每个规范由类和初始图组成。一个类定义有一个特定的类型图和一组规则F.L. Dotti等人理论计算机科学电子笔记127（2005）37定义为该类的对象。在初始图形定义中，用户指定其指定的初始配置（将被转换用于验证或模拟的模型）。编辑器允许用户通过访问菜单栏（文件栏）从数据库创建、打开和保存新规范。通过菜单栏，用户还可以：创建新的类型图（自动创建新的类定义），规则和初始图（Specification图）;生成验证，模拟或执行的代码（Option图）;访问帮助部分（Help图）在编辑器中实现的规范的图形版本由选项卡组成，其中主选项卡表示类和初始图。在类选项卡中，有一个选项卡用于表示类的类型图，其他选项卡用于表示该类类型的规则。编辑界面由两个主要部分组成：绘图区（规则6为两个）和工具栏。绘图区负责显示图形规格并允许编辑组件。工具栏用于选择绘图区域的编辑方式，基本上分为选择、插入、删除三类。为了实现编辑器的接口，我们首先定义了一些基本的构建块，这些构建块被进一步专门化以满足所涉及的组件（类型图、规则和初始图）的编辑要求。同样，绘图区域中显示的图形元件是从定义图形节点和弧元件的基本类派生的类。虽然用户可以自由编辑规范，但完整性检查是必要的，以保证规范的一致性。基本上，这些约束分为四类：A型图约束：1 创建：由类型图描述的类必须存在于其定义中，并且永远不会被删除;2 消息修改：修改消息导致改变旧消息沿规则和初始图的所有出现;3 属性和参数修改：这些修改导致检查属性或参数是否用于规范的任何规则或初始图中。如果存在，则警告用户;4 消息、参数和属性删除：如果删除的元素出现在任何规则或初始图中，则必须警告用户B规则约束：1 创建：指向对象的一条消息必须存在于6规则还有一个输入框（在绘图区域上方），用于定义规则条件。8F.L. Dotti等人理论计算机科学电子笔记127（2005）3左手边的规则。同样的物体必须出现在右手边。必须删除右侧的消息。所有其他修改必须在接收消息的对象内部进行。这些修改可以仅考虑对象的属性和接收到的消息的参数2 对象的动态创建：根据OBGG，在规则中创建的对象（添加在右侧）必须具有指向它的Init消息。类的类型图（对象是实例）必须具有Init消息。此外，还必须定义用于处理Init消息的Init规则。初始化消息/规则都由用户定义。C初始图形约束：1版本：初始图中使用的所有属性和参数必须具有定义的值或引用。D.一般限制：1.消息和规则之间的一致性：编辑器必须检查为类定义的所有消息是否都被规则正确处理目前，在我们的编辑器中，我们已经实现了约束A.1，A.2，A.3，A.4，B.1，C.1。尽管如此，限制B.2和D.1的执行是今后工作的一个重要方面。4分析和代码生成在本节中，我们将回顾我们用于验证、模拟和生成执行代码的方法4.1验证当使用验证时，我们能够分析模型可以生成的所有可能的执行。 为了使用验证分析OBGG模型，[7]我们定义了从OBGG到PROMELA（SPIN模型检查器的输入语言）的翻译。基本上，在转换中，OBGG对象被映射到PROMELA进程。出于验证目的，OBGG对象的属性仅限于PROMELA支持的类型。此外，OBGG消息被转换为PROMELA消息，并且消息的接收通过异步通道（为每个转换对象定义）完成，该通道也用作对转换对象的引用。OBGG对象的规则被映射到翻译对象内部的条件结构，OBGG初始图成为PROMELA中的初始过程。对象之间的并发性自然由并发性F.L. Dotti等人理论计算机科学电子笔记127（2005）39转换对象（过程）之间的关系。然而，在使用PROMELA通道时需要考虑 两 个方 面 ： （ i ） 在 OBGG 中 ， 对 象 处理 的 消 息 不保 持 顺 序 - 而PROMELA通道保持顺序;（ii）在OBGG中，对象在每个时刻可以接收无限数量的消息-在PROMELA中，通道具有最大数量的消息，如果通道已满，则随后对通道的写入将与同一通道上的最终读取为了处理（i），每个对象都有一个内部通道，用于以非确定性的方式处理存储的消息为了处理（ii），我们插入断言，就在发送消息之前，评估表达式以确定目的地通道是否未满。因此，当验证模型时，当通道满时可能产生错误，从而要求用户增加缓冲器尺寸。关于翻译的更多细节可以在[7]中找到。在[7]中，我们还定义了一种使用线性时态逻辑（LTL）指定OBGG模型属性的方法-与SPIN中使用的时态逻辑相同。根据这种方法，属性是根据事件（规则的应用）来定义的。此外，在[18]中，我们扩展了我们以前的方法来处理对象的内部状态（仍然使用事件的概念），并且还提出了一种根据OBGG抽象而不是PROMELA生成反例的方法目前，如图1所示，属性指定方法没有实现，必须直接在SPIN中完成。我们打算实现此功能，并将其与用于根据OBGG自动生成图形反例的工具集成，以补充图1中提供的验证工具。4.2仿真使用模拟的主要优点是在概念阶段对系统进行定量和定性分析的可能性我们的环境为用Java语言编写的OBGG模型提供了一个模拟器[3]。它与通过称为内核的特殊模块交换消息来相互通信的实体一起工作。内核负责消息传递和全局时间控制。该算法采用保守的核算法，对仿真时间进行集中控制。考虑到内核的功能，OBGG模型直接映射到仿真环境。OBGG类及其属性一对一地映射到具有相应属性的仿真实体。每个规则指定的OBGG类的行为的一部分被映射到一个类（在实现语言级别）表示它。OBGG类处理的消息，与各自的属性，映射到仿真消息与其相应的属性。初始状态10F.L. Dotti等人理论计算机科学电子笔记127（2005）3通过创建适当的实体实例、消息和属性初始化，系统的初始状态被相应地映射到仿真环境的初始状态。模拟实体基本上由活动对象（具有内部线程的Java对象）建模。该对象的接收缓冲器用于存储内核传递的消息，这些消息对应于规范级别的消息。实体的内部线程选择由输入缓冲器中的消息启用的规则，并触发它们的执行，尊重图形语法给出的非确定性行为。模拟器允许表示消息的最小和最大时间戳，这意味着消息必须在（currenttime+minimum）和（currenttime+maximum）之间最小时间允许表示真实信道的延迟，对于分布式系统特别有用。最大时间支持的情况下，一个人想指定系统的时间限制，即，如果消息在特定时间间隔内没有被消费，则系统失败（实时系统）。4.3代码生成为了实现将正式规范转换为可执行代码的目标，我们进一步扩展了模拟器中使用的转换过程，这在前一节中进行了讨论。在模拟的情况下，时间以及因此系统中的所有事件由模拟算法控制。在这个过程中，内核在实体之间传递事件（消息）以及为这些事件提供时间一致性方面起着重要作用。 在实际情况下，时间是隐含的，即系统的事件在发生时自然地按时间排序。消息可以在生成时直接从实体传递到实体。因此，我们从OBGG规范中生成实际应用程序的第一步是将OBGG类映射到为模拟而建立的Java类，但不包括模拟时间控制方面和模拟内核的消息传递功能，使实体直接通信。为了在分布式场景中做到这一点，我们决定采用一个底层平台，以确保消息传递的分发透明性和FIFO（先进先出）语义，从而保持消息传递的内核语义。F.L. Dotti等人理论计算机科学电子笔记127（2005）3115相关工作我们可以将OBGG环境与各种相关工具进行比较由于该环境的主要目的是作为并发基于对象的系统的正确开发的基础特别是，我们将考虑用于并发基于对象的应用程序的规范、仿真、验证和代码生成的重写逻辑[14]非常适合作为分布式系统的形式化规范和分析的框架Maude [13]是一种基于重写逻辑的多范式可执行规范语言。它将等式逻辑子语言中的等式风格的函数规范与面向对象的对象系统规范风格集成在一起，这些对象系统可以是高度并发和不确定的。Maude规范是可执行的，使用Maude及其相关工具[5]，可以以各种方式分析这些可执行规范，包括符号模拟和调试，以及模型检查分析的灵活形式它已被用于允许软件设计的形式分析，并支持从相关的可执行规范生成代码。与我们的方法相反，Maude是一种文本语言，使用Maude的模拟和验证结果也以文本形式呈现给用户。在Petri网领域，有大量的工具（见[1]），但只有少数是针对对象范式的。CoopnTools是一个由一组工具组成的环境，支持基于CO-OPN语言的并发软件开发[4]。CO-OPN是一种基于同步代数Petri网的面向对象规范语言。这种语言允许使用Petri网布局定义并发对象，并包括子类型，子类化和泛型的设施。该环境包括编辑器、模拟器（令牌游戏）、测试工具和Java代码生成工具。然而，没有支持验证特定系统的属性。统一建模语言（UML）是一种标准化的可视化符号，用于对面向对象的软件进行建模，它在商业上被广泛使用因此，有许多支持UML图开发的工具可用。通常，这样的工具提供了以一种或多种商业编程语言生成代码的可能性。UML模型的模拟也已经被一些作者解决了，如[2]。由于UML语义是用自然语言给出的，因此它并不是没有歧义的。因此，许多作者致力于UML部分的形式化，以便可以将形式化验证应用于UML模型。例如，vUML工具[12]支持对UML子集的验证，12F.L. Dotti等人理论计算机科学电子笔记127（2005）3⟨⟩翻译成PROMELA。根据[12]，该工具不支持一般LTL公式的验证，但可以检查一组有价值的固定属性。提供了与UML模型兼容的抽象中的反例生成Fujaba项目旨在使用统一建模语言UML作为编程图形重写语言。 使用的规范语言在Fujaba工具[15]中，使用类图来指定系统的数据类型，并结合活动和协作图来指定其行为。Fujaba环境由一系列工具组成，其中包括编辑器，模拟器和（Java）代码生成器。尽管在Fujaba内部进行了有关验证的调查（见[10]），但这些调查仍未整合到环境中。6最后发言在本文中，我们提出了一种开发基于并发对象的系统的体系结构，其中系统是用一种基于图形语法的正式规范语言来规范的，称为基于对象的图形语法。如环境架构所示，我们正在定义图形界面，以使验证和模拟过程对用户透明。另一个未来研究方向是开发其他类型的完整性检查。此外，我们正在考虑使用XML（可扩展标记语言）代替目前使用的数据库，以提高环境的可扩展性引用[1] Petri网工具数据库，http://www.daimi.au.dk/PetriNets/tools/db.html（访问日期：2004年9月）。[2] 阿里夫湖和N. Speirs，A uml tool for an automatic generation of simulation programs，in：Proceedingsofthesecondinternationalworkshopon Softwareandperformance（2000），pp.71-76.[3] Arnold，K.和J. Gosling，[4] Biberstein，O.，D. Buchs和N. Guel fi，Object-oriented nets with algebraic specifications：CO-OPN/2 formalism。LNCS：并发面向对象编程和Petri网，Advances in Petri Nets 2001（2001），pp. 73比130[5] Cl av el，M. ，F. Dur'an ，S. E k er，P. Lincoln，N. Mar t's-Oliet ，J. Meseguer 和J. F.Quesada ， Maude ： Specification and Programming in Rewriting Logic ， TheoreticalComputer Science285（2002）. 187-243[6] Dotti，F.，L.杜阿尔特湾Copstein和L. Ribeiro，移动应用的仿真，在：2002年通信网络和分布式系统建模与仿真会议（2002年），pp. 261-267.F.L. Dotti等人理论计算机科学电子笔记127（2005）313[7] Dotti，F.，L. 福斯湖Ribeiro和O.Santos，基于对象的分布式系统的验证，第六届开放式基于对象的分布式系统形式化方法国际会议，LNCS2884（2003），pp.261-275。[8] Dotti ， F. ， L. Ribeiro 和 O.Santos ， Specification and analysis of fault behaviours usinggraphgrammars ， in ： 2ndInternationalWorkshoponApplicationsofGraphTransformations with Industrial Relevance，LNCS3062（2003），pp.120-133[9] 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，FMOODS 00177（2000），pp. 45比64[10] 赫希，M。和H. Giese，Towards the incremental model checking of complex realtime umlmodels，in：Proc. of the Fujaba Days 2003，Kassel，Germany，2003。[11] Holzmann，G. J.，模型检查器SPIN，IEEE软件工程学报23（1997），pp. 279-295.[12] Lilius，J.和I.Paltor，vuml：一个验证uml模型的工具，在：第14届IEEE自动化软件工程国际会议论文集（1999），第100页。255.[13] M. Clavel，P.L.，S. Eker和J.Meseguer，Maude原理，理论计算机科学中的电子注释4（1996），pp.65比89[14] Meseguer，J.，条件重写逻辑作为并发的统一模型，理论计算机科学96（1992），pp。73比155[15] Ni ck el，U.， J. Niere和A. Zündorf，Tooldemonstration：The fuja baenvi ronmen t，in：P roc.第22届国际软件工程会议（ICSE），利默里克，爱尔兰（2000年），页。742-745[16] 罗森伯格，G.，编辑，“图形语法和图形变换计算手册 1：《基础》，[17] Russi，D. T.一、“图形语法的表示和分析（葡萄牙语）”，硕士论文，UF R G S -Instituto de Inform 'atica，巴西（2003年）。[18] 桑托斯岛，澳-地F. Dotti和L.Ribeiro，《基于对象的图语法》（2004），第二代图变换和可视化建模技术，ENTCS，即将出版。