理论计算机科学电子笔记127（2005）101-111www.elsevier.com/locate/entcs基于图变换模型的行为精化ReikoHeckelaSebastianThoènebaComp. 科学，电气工程，数学，reiko@upb.deb国际研究生院动态智能系统，seb@upb.de德国帕德博恩大学摘要模型驱动的软件工程需要将抽象模型细化为更具体的、特定于平台的模型。为了创建和验证这些改进，捕获重构或通信场景的行为模型被呈现为动态元模型的实例，即，指定概念和基本操作场景的类型化图变换系统可以组成。现在可以基于相应的元模型来描述模型之间可能的细化关系。与以前的方法相比，图变换系统上的精化关系没有被定义为抽象变换规则之间的固定语法映射，例如，具体的规则表达式，但允许转换系统之间更松散的语义定义关系，从而产生更灵活的细化概念关键词：MDA和模型转换，一致性和协同进化，图转换系统的1介绍模型驱动的软件开发基于将抽象模型细化为更具体的模型的思想，最近的例子是OMG1提出的模型驱动架构（MDA）。在这里，平台特定的细节最初在模型级别被忽略，以允许最大的可移植性。然后，通过添加映射到给定目标平台所需的实现细节来细化平台无关模型。因此，在每一级，第1www.omg.org/mda/1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.08.037102R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）101在模型中加入了对所选平台的资源、限制和服务的假设符合建模语言的模型集通常定义为元模型，即，带有约束的类图，描述模型的各个元素及其组成。对于行为模型，该方法被扩展到动态元模型，形式化为类型化图转换系统[3]。非正式地，类型化图转换系统包括（1）定义允许的模型元素及其关系的词汇表的类型图，（2）进一步限制有效模型的一组约束，以及（3）一组图转换规则。类型图和约束可以看作是类似于经典的静态元模型。因此，符合给定（静态）元模型的模型被表示为类型图的实例图我们可以把类型图看作一个UML类图，把实例图看作一个符合类图的类型和约束的对应的UML对象图在动态系统在运行时演化的情况下，单个实例图仅在某个时间点对系统状态进行建模。为了对系统演化进行建模，动态元模型提供了图形转换规则。这些是可执行的规范，可用于定义图上的局部变换。由于图表示系统状态，因此转换规则指定，例如，可能的计算、通信或重构操作，其可以应用于产生到新状态的转换的各个状态。基于各个转换步骤，我们可以解释、模拟和分析动态模型的行为语义。特别地，我们可以生成一个状态转换系统，它反映了系统的所有可达状态，转换由可能的转换步骤定义我们为不同的抽象层次提供不同的元模型。因此，为了将抽象模型细化为更具体的模型，我们建立在所涉及的元模型之间的细化关系上。形式上，这种关系是通过抽象函数来定义的，如第2节所解释的。抽象是一种映射，通常通过某种投影将每个具体模型关联到相应的抽象模型。基于此，我们可以检查具体模型是否保留了抽象模型的结构在第3节中，我们提供了保留抽象模型行为的条件。我们要求抽象模型的行为可以在具体级别上进行模拟，并且我们讨论了如何在具体级别上通过模型检查来检查此为此，我们引入了一个翻译功能，逆变抽象，抽象模型属性映射到具体的水平。R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）1011032结构细化一个动态元模型被表示为一个类型化的图转换系统G=R_TG ，C ，R_TG，它由一个类型图T_G，一组结构约束C，和一组图转换规则R组成：L_R_TG.在TG上类型化的有效实例图的集合称为GraphTG。与之前的论文[1]一样，我们通过定义archi来描述这种技术作为软件架构元模型的架构风格：软件架构的基于图我们认为架构风格是系统实现平台的概念模型。指定风格动态的图转换规则捕获了重构和通信机制，这些机制允许架构在运行时发展，并由相应的平台支持。我们将在第3节中回到动态方面。现在，考虑一个模型驱动的开发过程，从一个抽象的、业务需求驱动的软件系统架构模型开始，该模型将被细化为一个具体的、特定于平台的在我们的简化示例中，我们假设平台无关级别的基于组件的架构风格，其中组件通过端口进行交互，只有在提供的接口和所需的接口匹配时才能连接。对于特定于平台的级别，我们假设一种表示面向服务的体系结构（SOA）的风格。在SOA中，组件的功能作为服务发布给服务请求者。特殊的第三方组件，称为发现代理，在运行时实现服务发现，即，服务提供者和请求者不需要预先知道彼此。为此目的，服务提供组件必须向发现代理发布所提供的接口的描述。然后，服务请求组件可以使用发现代理的查找机制来为自己的需求找到合适的服务描述。我们没有给出这两种架构风格的类型图;它们可以在[2]中找到。基本上，它们为上面总结的架构概念定义了节点和边类型。这些类型图的实例图用于表示平台无关或面向服务的体系结构。为了可读性，我们使用一个类似UML 2.0的具体语法，如图1所示。该示例描述了一个电子旅行社应用程序的体系结构。它要求航空公司系统为客户预订他们想要购买的机票。给定一个类似于平台无关体系结构风格的抽象转换系统G=TG，C，R，和一个具体的转换系统GJ=104R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）101∈与面向服务的架构风格类似，结构细化建立了抽象实例图G∈GraphTG和具体实例图GJGraphTGJ之间的关系：抽象G的有效精化，具体GJ必须保持抽象图的结构。由于将被比较的两个实例图在不同类型的图上表示，因此该条件以抽象函数为模来表示。图GJ是G的结构精化，如果G∈abs（GJ）。图1举例说明了应用于具体的、SOA特定的旅行社系统模型的抽象函数（底部），从而生成抽象的、平台无关的模型（顶部）。抽象删除了所有平台特定的元素，如发现组件和服务描述和需求文档。此外，平台特定的构造型服务适用于平台无关的词汇表成分抽象函数的定义有一系列的可能性，从两个类型图之间的简单映射，可以通过重命名图形元素的类型来提升到实例图（参见图1）。[2]）到由变换规则定义的复杂映射，例如，以检测逆向工程中的在本文中，我们将公理化这类映射的相关性质，而不是固定一种具体的定义方式3行为细化动态模型的行为部分由其元模型的图转换规则定义例如，对于抽象的、基于组件的体系结构风格，我们假设组件可以在运行时动态绑定到提供的接口。这可以通过如图2所示的接口绑定和解除绑定的适当重新配置操作来实现。在这种情况下，定义所需绑定和解除绑定操作的两个转换规则是对称的。形式上，转换规则由基础类型图上的实例图对表示然而，出于空间原因和更好的可读性，我们以类似UML的语法来表示它们，类似于前一节中的实例图。行为由实例图之间的转换表示。因此，可能的行为的空间是由一个过渡系统，其状态是可达图，其过渡由规则应用程序生成。给定模型的初始状态作为开始图，可以生成并且R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）101105ABS«组件»C1Int «component»C2«组件»C1Int«组件»C2书-书-旅程旅程书-书-班机班机«组件»航空公司«组件»旅行社«组件»客户端«描述»«满足»«满足»«满足»«知道»«需要»«知道»«知道»«需要»书-«需要»书-«组件»客户端旅程旅程书-书-班机班机«需要»«需要»«描述»«描述»«满足»«满足»«描述»«要求»«描述»«要求»«要求»«要求»«要求»«描述»«服务»航空公司«服务»旅行社«发现»查找图1.一、从面向服务的抽象到平台无关的风格印度报Int解绑图二、抽象建筑风格的重构规则106R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）101通过不断地将转换规则应用于先前生成的状态来探索转换系统。作为示例，图3以抽象架构风格显示了旅行社系统的转换系统。转换由应用的转换规则的名称标记。最近，GROOVE [7]或CheckVML [8]等工具支持从图转换系统自动生成转换系统。图三.抽象旅行社体系结构与平台无关风格类似，面向服务的架构风格中也有图转换规则。但是，它们必须考虑特定于平台的限制。例如，在SOA案例中，在可能访问服务之前，需要知道服务的描述。因此，图4所示的相应重新配置规则绑定在其左侧包括该附加前提条件。因此，只有当扮演服务请求者角色的组件知道服务描述时，才能应用绑定这是由UML依赖与sterotype知道。面向服务的风格包含更多的平台特定的转换规则publish和find，通过将服务描述发布到发现机构并通过查询满足某些要求的合适描述来实现动态服务发现。在执行绑定操作之前，由于篇幅所限，本规则«组件»«组件»客户端书-旅程客户端书-旅程«组件»客户端BookFlight书-旅程书-旅程BookFlightBookFlight书-旅程BookFlightBookFlight书-旅程BookFlight«组件»航空公司«组件»航空公司«组件»客户端«组件»航空公司«组件»旅行社«组件»旅行社«组件»旅行社«组件»旅行社«组件»航空公司R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）101107«要求«要求«描述»«描述»«组件»请求者«要求»«发现»D«描述»«需要»«要求»«描述»«满足»«描述»«需要»«要求»«描述»«满足»结合«服务»提供商«组件»请求者«服务»提供商«组件»请求者«知道»«知道»«发现»«知道»D中文（简体）«发现»D«描述»«描述»«服务»«服务»提供者提供者芬«满足»«描述»»«知道»«满足»«描述»»«知道»«知道»«需要»«组件»请求者«要求»«发现»D联合工业«组件»请求者«服务»提供商«组件»请求者«服务»提供商图四、面向服务架构风格的重构规则图4形成了[1，2]中提出的SOA风格的简化版本就像在平台独立的层面上一样，我们现在可以将SOA规则应用于旅行社架构的SOA特定变体（参见图2）。1），产生另一个表示平台特定行为的转换系统。108R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）101GG→为了检查两个模型（架构）的行为细化，我们现在必须考虑可以在底层动态元模型（架构风格）中生成的转换系统。形式上，我们再次考虑抽象系统=TG，C，R的实例图G以及具体系统J=TGJ，CJ，RJ的实例图Gj。我们假设GJ表示G的一个结构精化。为了成为行为精化，GJ的行为必须精化G的行为。是这种情况如 果每条路径GG1级 ... ⇒ Gn在抽象变迁系统中有acorres ponde ntpathGJ={\displaystyleG j}1 ={\displaystyle G j}} . . 在混凝土转变中=GJn系统，其中GJi定义G i（即，G i∈ abs（GJi）），对于所有i = 1. n.抽象系统中的每一步都可以与具体系统中的一系列步骤相匹配。抽象的单个变换步骤Gi<$Gi+1在具体层次上，用变换方程GJi=∑GJi+1来定义路径因为可能需要执行一系列连续的具体步骤为了实现抽象的（例如，额外的发布和查找），在SOA的情况下）。基于上面提到的图转换系统的模型检查方法，我们想将抽象路径的细化公式化然而，行为细化的条件包括Gi的结构细化，一般来说，它需要将具体的图形投影到抽象的图形上。水平，以验证所需的包含。为了只在具体系统的层次上表达同一性质，我们必须假定第二个映射transs：GraphTGGraphTGJ，逆变为抽象。它将抽象的实例图转换为具体的实例图，表示抽象状态在具体类型系统上的重构。请注意，具体图不一定表示具体模型的完整状态，而是为了满足抽象图的要求而必须存在的最小模式已经填好了因此，我们认为一个具体的实例图是一个抽象图的有效精化，如果它包含这个模式作为一个子图，形式上是transGGJ。例如，图5示出了如何将旅行系统的平台无关模型转换为具有服务而不是期望的组件的面向服务风格的模式根据上面的定义，包含此模式的有效的面向服务架构，例如，的SOA模型在图的底部第一，抽象模型的细化为了确保上述条件与结构加细的原始条件等价，我们必须确保两个逆变映射的相互一致性。这被正式表示为满足条件，R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）101109⊆书-书-旅程旅程书-书-班机班机«组件»航空公司«组件»旅行社«组件»客户端反式书-书-旅程旅程书-书-班机班机«服务»航空公司«服务»旅行社«组件»客户端图五、从独立于平台到面向服务的风格让人想起代数规范或逻辑中的类似条件，即，transs（G）<$GJi <$G <$abs（GJ）.在这种情况下，我们说这两个映射是兼容的。在这种假设下，细化可以表述如下。具体图GJ定义抽象图G，如果• 反式（G）→GJ• 对于抽象系统中的每一个变换步骤GH，存在一个transformations equen ceGJ=∑H JsuchthatH JrefinesH.从满足条件可以得出，上面的第一个子句等价于用抽象形式表示的原始条件G abs（GJ）。然而，新的条件只能在具体层面上得到验证。第二个子句实际上是对模拟关系的共归纳定义。用序列的形式来拼写，它说，对于每一条（可能是无限的）路径G <$G 1<$G2<$. 在抽象系统中存在一条路径GJ=GJ1 =GJ2 =... 在具有t rans（Gi）<$GJi的混凝土系统中，4相关工作使用元模型来定义图形语言在OMG编写的元对象工具（MOF）的上下文中变得非常流行他们还将元模型定义为具有附加约束的类型图，例如，基数如果模型符合类型图，则它是元模型的实例。在我们的工作中，我们通过图转换规则扩展了元模型的静态声明，这些规则允许将动态模型演化定义为系统演化的模拟。图变换技术110R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）101捕获模型的动态语义的方法受到Engels等人的启发。在[4]中。这种方法扩展了元模型，定义了一种建模语言，如UML，通过图形转换规则来描述表示模型状态的对象图的在[2]中，我们已经考虑了几个级别的平台抽象，这些抽象允许从平台无关的架构到更特定于平台的架构的类似MDA的细化。这就把我们带到了精化图和图变换行为的合适概念的问题：虽然结构精化意味着所涉及的类型图之间的关系，但行为精化的思想是将所涉及的图变换系统的变换规则联系起来。一般来说，我们可以将这些加细关系置于从句法到语义定义的关系的连续体中。Große-Rhode et.al. [5]，例如，提出了一种可以在语法上检查的抽象和具体规则之间的细化关系条件之一抽象规则及其细化必须具有相同的前置条件和后置条件。基于这种限制性定义，他们可以证明，具体规则表达式的应用与相应的抽象规则产生相同的行为。这种方法的缺点是，它不能处理细化规则表达式应该对抽象规则中没有出现的具体级别的元素有额外影响的情况。而且，这种方法不允许根据其应用的上下文对同一抽象规则进行替代性的细化同样，Heckel et. [6]是基于两个图形转换系统之间的语法关系。 虽然这种方法限制较少，因为它允许在具体层面上增加额外的元素，但它如果抽象规则和具体规则之间没有直接的对应关系，则仍然难以适用。此外，它们的目标是将任何给定的具体转换行为投射到抽象级别，而不是像我们的情况那样相反。因此，细化意味着对行为的限制，而不是行为的扩展。在我们的工作中，我们提出了一个更灵活的，语义定义的精炼概念。我们不需要变换规则之间的固定关系，而只需要图变换系统的结构部分之间的固定关系。然后，我们检查在抽象系统中选择的系统状态是否在具体层次上也是可达的，无论通过哪一序列的transformation。通过避免规则之间的函数映射，我们还可以将转换系统与完全不同的行为联系起来，并且我们足够灵活，可以处理替代的细化。R. Heckel，S.Thöne/Electronic Notes in Theoretical Computer Science 127（2005）1011115结论我们已经讨论了表示为图变换系统的实例的动态模型的细化的语义条件。到目前为止，这种技术的应用包括基于建筑风格之间的对应关系对建筑模型的细化。我们正计划通过耦合的CASE工具与编辑器和分析图转换系统，目前进行实验与现有的模型检查器的方法。引用[1] L. 巴雷西河 He ck el，S. Thoêne和D. Varro'.面向服务的体系结构的建模和验证：应用与风格。在Proc. European Software Engineering Conference and ACM SIGSOFT Symposium on theFoundations of Software Engineering，ESEC/FSE 03，第68-77页ACM Press，2003.[2] L. 巴雷西河 He ck el，S. Thoêne和D. 好的动态软件架构的基于风格的改进。第四届IEEE/IFIP软件体系结构会议论文集，WICSA 4，第155-164页IEEE，2004年。[3] A.科拉迪尼Montanari和F.罗西图形处理。Fundamenta Informaticae，26（3，4）：241[4] G.恩格斯豪斯曼河海克尔和圣绍尔。动态Meta建模：UML中行为图的操作语义的图形化方法。 在Proc. UML 2000 - The Uni Fied Modeling Language，LNCS第1939卷，第323斯普林格，2000年。[5] M. Große-Rhode，F. Parisi Presicce和M.西梅奥尼类型化图变换系统的空间和时间细化。 在proc数学Comp.的基础 Science 1998，LNCS第1450卷，第553-561页。Springer，1998年。[6] R. He ckel，A. Corradini，H. Ehrig和M. 我爱你。类型图变换系统的水平和垂直结构。 数学结构。 计算机科学，6：613 -648，1996。[7] A.伦辛克GROOVE模拟器：状态空间生成工具。In M. Nagl，J. Pfalz，andB. Bohlen，editors，P roc.APpli cationofGraphTransformationswithIndustrialRelevan ce（AGTIVE '03 ） ， LNCS第3062卷，第479-485页。Springer，2003年。[8] D. 好的 对可视化建模语言进行系统分析。 在P roc. GT-VMT2002-Int. 图形转换和可视化建模技术研讨会，ENTCS第72卷，第57-70页。Elsevier，2002年。
