基于属性图转换的模型转换形式概述-2006理论计算机科学电子笔记

理论计算机科学电子笔记152（2006）3-22www.elsevier.com/locate/entcs基于类型化属性图转换的模型转换形式概念综述Hartmut Ehrig1， 卡斯滕·埃里希2德国柏林工业大学摘要在本文中，我们给出了一个概述的形式化概念的模型转换的基础上类型化属性图转换的可视化语言之间。我们从一个基本概念开始，其中视觉语言仅由属性类型图定义，并通过基本类型化属性图转换系统进行模型转换。 我们继续考虑到应用条件，约束，生成图gram- mars和操作语义的基本概念的不同种类的扩展。主要目的是讨论模型转换的形式正确性准则，包括语法正确性，功能行为和语义正确性。关键词：模型转换，概述，形式概念，类型化属性图转换，图转换1介绍通过模型驱动架构（MDA）[20]，对象管理组织（OMG）定义了一个基于建模和模型到实现的自动映射为了定义模型和元模型，OMG已经建立了众所周知的标准Meta-Object Facility（MOF）[19]和统一建模语言[25]，一方面，这些标准为元模型方法中的模型转换提供了坚实的基础另一方面，图形变换[22，9，11]提供了一个固体1Email：ehrig@ c s. tu-berlin. D e2Email：karste n e@cs. tu-b erli n. D e1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.0114H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）3模型转换的基础。定义良好的数学背景允许清晰地定义视觉语言的语法和语义以及分析技术，例如用于模型转换的终止准则或关键对分析不同的模型转换方法发表在文献中，如ATOM3[5]、GreAt [1]和VIATRA[27]，并在商业MDA工具中实现，如ArcStyler [2]和XDE [21]。在本文中，我们讨论了在[15，13，10]的意义上，类型化属性图变换可以支持视觉语言和模型变换的形式化定义的由于我们的主要重点是模型转换，这应该是基于源语言和目标语言的抽象语法，我们只考虑抽象语法层次的可视化语言在本文中。其主要思想是：用类型化属性图变换来描述模型变换，源模型和目标模型必须用类型化属性图来表示。这不是一个限制，因为任何模型，特别是视觉模型的底层结构，由于其多维扩展，最好通过类型化属性图来描述用类型化属性图变换进行模型变换，是指将模型的底层结构作为类型化属性图，按照一定的变换结果进行变换。结果是一个类型化的属性图，它显示了目标模型的底层结构。基于图变换的模型变换可以由属性图变换系统GT S=（AT G，Prod）来定义，该系统由属性类型图ATG和变换产生集Prod组成。源模型的抽象语法图可以由类型图ATGS上的所有（或子集）实例图指定。相应地，目标模型的抽象语法图由属性类型图ATGT上的所有（或子集）实例图指定。类型图ATGS和ATGT都必须是属性类型图ATG的子图（参见图1）。开始模型转换时，实例图AGS的类型为ATGS，它的类型也为ATG。在模型转换过程中，中间图是通过ATG类型化的。请注意，此类型图可能不仅包含ATGS和ATGT，还包含仅转换过程所需的其他类型、关系和属性结果图AGT是在ATG上自动键入的。如果它也是在ATGT上键入的，它满足了语法正确的一个主要要求。数据类型在转换过程中被保留。定义可视化语言的模型转换的主要思想H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）35、AT G，IncSATG，，IncTrAzTG，S，，，，，，，，，T，、、类型AGS类型AGi、、、、、、、、类型 AGTPJpp，，AGSpiz.. .zAGikz.. .L zAGTFig. 1. 模型转换过程上述基本概念在第3节中有更详细的定义。第2节中的一个小案例研究说明了这一基本概念。特别是，它描述了哪种正确性的要求是有用的，以及它们如何可以制定在我们的方法在正式的基础上。在第3节中，我们分析了上面讨论的基本概念。由于基本概念只有有限的表达能力，我们在第4节中给出了几个扩展的概述。特别是，我们讨论了使用的产生式与应用条件，Meta模型与不同种类的约束，生成图文法以及源和目标语言的操作语义此外，我们分析了模型转换的正确性的后果，根据[24]，正确性包括语法正确性，功能行为和语义正确性。 V ar'o和Pataricza在[2 6]中已经提出了正确性准则。在结论部分，我们总结了类型化属性图变换理论对模型变换的形式化概念的支持程度以及有待进一步研究的问题确认我们要感谢Gabor Karsai和Gabriele Taentzer组织了第一次关于图和模型转换的国际研讨会，并感谢审稿人提出了一些有用的意见，从而改进了最终版本。2模型转换案例研究为了说明我们将在第3节中介绍的基本概念，我们简要回顾了[7，10，14]中提出的从UML 2.0状态图到Petri网的模型转换。源建模语言：简单版的状态图状态图的类型图TS如图2所示。事实上，TS是一个E图（见[10]），其中图节点由矩形表示，数据节点由圆角矩形表示，图边缘由带铭文的实线箭头表示，6H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）3sm2step从StateMachinesmname字符串stnameisInit布尔状态结束状态trans2cond过渡Cond字符串易名中国事件sm2conf到触发conf2state开始step2transstrans2actact2event图二. 作为E-图的节点属性边由带铭文的虚线箭头在此示例中，没有边属性。数据类型签名DSIG=Sig（string）+Sig（boolean）由字符串和布尔值的签名给出，其中图中只显示了排序二、类型图TS与最终DSIG-代数Z一起定义了属性类型图ATGS=（TS，Z）。 TS可以被认为是Meta模型的提取UML 2.0状态图事实上，这个Meta模型是对标准UML元模型的一个适当的限制，它显式地引入了几个仅在标准中隐式存在的状态图概念（例如状态配置等）。我们考虑一个statemachines的网络状态机。单个语句机通过将状态层次结构分解为状态配置Conf并将并行转换分组为Steps来捕获特定类的任何对象的行为。请注意，图2中的状态图类型图允许非有效状态图的图。例如，一个Step可以通过边缘sm2step与两个状态机连接。出于这个原因，可以使用生成语法语法- mar来精确定义源建模语言（参见[10]）。目标建模语言：Petri网事实上，在文献中有几种Petri网的变体。我们考虑位置/变迁网，弧权重为1，每个位置上最多有一个标记，类型图TT如图所示。3 .第三章。参考Meta模型为了使源和目标建模语言相互关联，我们使用引用Meta模型[27]。例如，RefState类型的引用节点（图1B中）。4）将源State与目标Place相关联。在图的符号图4的左侧和右侧对应于图4。2步骤Conf行动H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）37StateMachineSC型图PN型图smname：sm2step普雷sm2conf普雷从Conf步触发到conf2state事件中文（简状态step2transs开始地方plname：String token：反式act2eventPostsrc邮政isInit：布尔转换stname：Stringendtrans2act行动cond2statetrans2condR1R2r3 r4R5R6参考事件参考状态Cond后弧弧前普雷雷茨地方弧前图3.第三章。作为E-图的Petri网型图见图4。 类型图：StatechartsPetri nets图3和图3分别示出，其中数据节点和节点属性在对应的图节点下方的框中列出，例如分别具有目标“String”的“State”的节点属性 2由图中的“State”的属性“name：String”和“isInit：Boolean”给出四、示例状态图：生产者-消费者-系统作为一个例子，我们将把我们的模型转换应用到生产者-消费者-系统。图图5给出了生产者-消费者-系统状态图的具体语法和转换后的生产者-消费者-系统Petri网的具体语法。生产者-消费者-系统状态图的抽象合成图如图6和图7所示。图7显示了转换后的生产者-消费者-系统Petri网的抽象语法注意，图7是在图3中的Petri网类型图上类型化的，图6是在图2中的状态图类型图上类型化的。字符串plname令牌布尔邮政后弧Postsrc普雷格特反式8H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）3图五. 示例状态图：生产者-消费者-系统具体图（上半部分）和转换后Petri网的具体图（下半部分）见图6。 生产者-消费者-系统状态图从状态图到Petri网的模型转换从状态图到Petri网的模型转换由3层转换产生式给出，图8显示了每层的一个产生式。我们在[13，10]意义上的类型属性图的双推出（DPO）方法中使用产品，并在[8]意义上扩展了负应用条件（NAC）。在图8中，我们只显示了每个规则的左手边（LHS）、右手边（RHS）和NAC（如果不为空），而接口图由LHS和RHS的交集给出，其中公共项具有相同的编号。为了得到一个基于Petri网Meta模型的目标图，在模型转换后删除源状态图和参考节点和边。H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）39LHSsm2step步骤R2R62：反式参考步骤RHSLHS1：国家R1R5地方参考状态stname = nisInit = trueplname = ntoken = trueNAC1：国家stname = nisInit = trueR1参考状态LHS1：国家stname = nisInit =见图7。 转换后的生产者-消费者-系统Petri网模型转换分以下3个步骤完成在我们的例子开始与图。6我们得到图。七是最终结果。InitState2Place[layer = 0，X={n：String}]StepFrom2PreArc[层= 1，X={}]NAC=RHS删除步骤[layer=2，X={n：String}]1：StateMashinesmname=nRHS2：反式1：StateMashine图8.第八条。层0、1、2的典型转换产品• 每个状态图状态都是用目标Petri网模型中的相应位置建模的，其中这样一个 位 置 中 的 令 牌 表 示 对 应 的 状 态 最 初 是 活 动 的 （ 参 见 生 产InitState2Place）。为每个有效事件生成一个单独的位置。否定应用条件（NAC）确保我们只能对每个状态应用此规则一次，因为只有当状态尚未通过类型为r1的边连接到RefState时，InitState2Place才适用于该状态。RHS不C1：步骤R2 2：参考步骤R6 3：反式从7：会议conf2state1：步骤R2 2：参考步骤R6 3：反式从普雷特格7：会议弧前conf2state普雷10H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）3• 每个状态图步骤被投影到一个Petri网转换。自然地，Petri网应该模拟如何退出和进入状态图中相应的状态，因此应该相应地生成转换的输入和输出弧（参见StepFrom2PreArc）。此外，触发transition应该消耗触发事件的token，并且应该根据动作生成token到目标（接收者）事件（与之相关的位置• 最后，我们通过另一组图转换结果从源和参考Meta模型中删除所有模型元素来清理联合模型例如，生产DeleteStep删除一个带有相应RefStep的Step。应用所有删除的产品后，我们得到图。7 .第一次会议。3可视化语言与模型转换的基本概念在本节中，我们将介绍如何使用类型化属性图转换来定义可视化语言和建模转换的基本概念这一基本概念在导言中已作了概述，现在将作更详细的介绍特别讨论了模型转换正确性的形式化要求3.1视觉语言在本节研究的基本概念中，Meta模型MM仅由属性类型图ATG组成，即MM=ATG，而 视 觉 语 言 VL 是 由 在 ATG 上 键 入 的 所 有 属 性 图 AG 定 义 的 ， 写 作VL=AGraphsATG。请注意，这是对视觉语言的一个非常基本的描述，更详细的描述将在第4节中进行。根据[15]，属性图AG=（G，D）由图G和具有排序符号S和操作符号OP的集合的给定数据类型签名DSIG=（S，OP）的数据类型代数D组成。这允许考虑具有节点属性的图。在[13]中，这个概念被扩展到也允许边属性，其中G不是经典图，而是具有从图边到数据节点的边属性边的E-图一个属性型图ATG=（TG，Z）是一个属性图，其中TG是图的部分Z是最终的DSIG-代数，对每个类s∈S，Zs={s}.属性型图ATG=（TG，Z）的例子在第2节的图2-4中给出，其中只显示了图的部分TGAG与一个属性图态射一起给出了ATG上的属性图H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）311→→→类型：AG ATG，称为类型态射。图中给出了类型化属性图的示例第2节中的6-7。在第5节中，我们将考虑更一般的情况来定义分别对应于Meta建模和图语法方法的视觉语言。然而，在这两种情况下，定义都基于属性类型图ATG。3.2模型转换定义模型变换MT：V L S的基本思想基于图变换的V L T已经在引言中讨论过了（见图1）。①的人。根据4.1，我们假设有视觉语言VLS=AG图ATGS和VLT=AG图ATGT基于ATGS和ATGT具有相同的数据类型签名DSIG。为了实现模型转换，我们构造了一个新的属性类型图ATG，并构造了包含incS：ATGS→ATG和incT：ATGT→ATG的数据类型。在第2节的图4中给出了ATG、insS和incT的示例，其中ATG不仅包括ATGS和ATGT，还包括附加类型和关系，这是模型转换所需要的模型转换MT：V LS→V LT基于GT S从V LS到V LT定义为：MT=（V LS，V LT，ATG，GTS）其中，除了V LS，V LT和属性类型图ATG之外，我们还具有在ATG上类型化的属性图转换系统GT S=（AT G，Prod），其中产生式Prod如[13，10]中所定义一般来说，Prod将在多个层中给出Prodn（0≤n≤k0），其中在每个层Prodn中的产品尽可能长地应用，然后转到层Prodn+1或在n=k0的情况下完成。这导致分层模型变换序列MS_M_TviaGT_S，其中源模型MS和目标模型M_T分别由属性图AG_S和AG_T给出，即MS=AGS和MT=AGT。一般来说，目标是从AGS∈V LS开始，要求模型转换序列AGS通过GT S导致唯一的AGT∈V LT。在这种情况下，我们将有MT（AG S）= AG T，这表明MT：V L SV L T具有功能行为。 总的来说然而，除非我们确保满足适当的正确性条件，否则我们不能确保实现这个目标，这将在下面讨论在第2节中给出了模型变换MT的一个例子，其中类型图包含如图所示图4和图8中的生产产品0、产品1和产品2的典型示例。 请注意，这些产生式中的大多数都有负的应用条件，这在4.1节中作为基本概念的扩展进行了讨论12H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）3\→3.3正确性要求在引言中，我们已经指出，一般来说，我们有以下三种正确性要求：句法正确性、功能行为和语义正确性。3.3.1基本概念在我们本节研究的基本概念中，基于GT S的模型变换MT：V LS→V LT的语法正确性意味着对于每个AGS∈V LS，存在一个模型变换序列AGS通过GT S生成AG T，其中AGT∈V LT，即AGT在ATGT上类型化。语法正确性可以通过AG到AGT的ATGT-限制来保证，AGS通过GT S来限制 AG 。 将 AG ： AG→ATG 型 属 性 图 AG 限 制 为 包 含 型 图 ATGT ：ATGT→ATG，即构造拉回图AGT，DincAGAGT型（PB）J，T.J.AG型JATGTATG从而得到AG类型的子图AGT由类型AGT ：AGT→ATGT.确保语法正确性的另一种方法是，对于ATG ATGT中的每个标签，存在一个删除产生式，前提是ATG中的所有标签都用于生成产生式。第2节中的案例研究满足此条件。如果有可能为每一层单独显示MT的语法正确性3.3.2功能行为基于GT S的模型变换MT：V LS V LT的函数行为意味着我们具有GT S的局部连续性和终止性，这意味着MT定义了从V LS到V LT的函数。对于并行独立的直接变换，局部连续性可由局部Church-Rosser定理证明。临界对分析允许分析所有的并行依赖，cies和我们得到的局部concilience，如果我们有严格的concilience的所有关键对。这个结果被称为局部同余定理，也被称为临界对引理，并且已经在[13]中证明了类型属性图然而，到目前为止，该结果仅针对没有负应用条件（NAC）的产品而已知因此，目前这一结果并不H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）313→适用于我们的案例研究，其中大多数产品都有NAC。如第2节所述，在[10]中提供了生成语法语法，其允许得出以下结论：假设模型转换源语言限于由语法语法生成的状态图，则我们的案例研究中的模型转换是局部连续的分层图变换的终止准则已经在[7，10]（另见[17]）中针对分层标记和类型化属性图变换系统进行了展示，并在这些论文中已经为我们的案例研究进行了验证。总之，我们的案例研究3.3.3基本格在基本的情况下，我们对源语言和目标语言V LS和V LT没有显式的行为。这意味着没有明确的方式来表明模型转换MT是行为保持的，因此语义正确。在我们的案例研究中，源语言和目标语言的模型也没有明确的行为。因此，我们只能检查图中给定状态图和转换后的Petri网的语义兼容性5，或者通过操作语义来扩展源语言和/或目标语言（见4.4节）。如果只有目标语言具有形式语义，我们可以通过模型转换为源语言定义两种语言都有操作语义的情况将在4.4节中研究。4扩展形式概念在本节中，我们将讨论可视化语言和模型转换的基本概念的几个形式化扩展。我们分别介绍每个扩展，并讨论有关模型变换正确性的具体后果。对于模型转换的大多数应用程序域，同时考虑这些扩展中的几个是有意义的。4.1基于图变换系统的模型变换及其应用条件在第3节中，我们假定模型变换MT的基本概念是：V LS V LT，MT是由一个类型化的属性图变换系统GT S用无应用条件的产生式来定义的，因为[13，10]中理论的主要部分只适用于这种基本情况。然而，在第2节的案例研究中，我们已经使用并解释了14H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）3⇒→→→◦负应用条件（NAC）。实际上，NAC是最常见的一在[8，10]中，我们定义了更一般的积极和消极应用条件。其中一个主要结果表明，对于每一个图约束constr，都存在一个等价的应用条件appl（constr）。这意味着对于每个通 过 （ p ， m ） 的 直 接 变 换 G H ， 其 中 匹 配 m 满 足 应 用 条 件 appl（constr），结果图H满足图约束constr。这个扩展对基本概念中的语法正确性没有直接的影响，但是当我们考虑由类型图和约束定义的视觉语言V LS和V LT时，它是重要的（见4.2）。关于功能行为，该扩展支持显示终止，因为[7，10]中的终止标准假设非删除层具有NAC的产物。然而，对于局部同余，这种推广引起了问题，因为[8，10]中的局部同余定理必须推广到具有应用条件的产生式即使对于NACs来说，这似乎也是一项重要的任务。这个扩展对语义正确性的影响必须结合扩展4.4来讨论。4.2基于约束Meta模型的可视化语言在基本概念中，我们假设视觉语言V LS和 模型变换MT的V LT：V LS→V LT分别由属性类型图ATGS和ATGT完全定义。在Meta模型然而，对于视觉语言，Meta模型分别由类图CDS和CDT定义这些Meta模型大致对应于我们的类型图ATGS和ATGT。然而，在Meta模型方法中定义V LS和V LT的模型这促使我们的概念扩展Meta模型的视觉语言VL也由约束，即MM（AT G，Constr），其中Constr是一个合适的一组约束。在类型化属性图变换的理论中，已经存在图约束的概念（见[16，8，10]），它特别允许在类图中表达多重性约束（见[23]）。原子（正）约束PC（a）由a：PC构成，一般图约束是原子图约束上的布尔公式.一个图G满足PC（a），如果对每个内射图态射p：PG存在一个内射图态射q：CGS.T. q a=p。除了图形约束，我们还可以考虑数据类型约束，由方程或一阶公式给出的数据类型签名的约束ATGS和ATGT的DSIG。 一个属性图AG=（G，D）满足H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）315⇒→→数据类型约束data-constr，如果DSIG-代数D满足data-constr（对于方程的情况，请参见[12一方面，数据类型约束可以用作语言中所有属性图AG的全局不变量，另一方面作为规则的应用条件在这种情况下，规则只能应用于属性图AG，如果AG满足规则的数据类型约束。在这样的数据类型约束中，我们可以要求AG的某些属性满足特定条件。虽然某些类型的OCL约束已经可以用图和数据类型约束来表示，但是还没有直接的方法来仅使用这些约束来表示出于这个原因，我们建议定义除了图和数据类型约束，类似于UML 2.0的OCL约束，一种新的类型的属性图的约束，称为graph-OCL约束。在[6]中，我们提出了如何定义syn-tax和满足这些约束的第一个想法使用这些思想，Meta模型MM=（AT G，Constr）可 以 包 括 三 种 约 束 Constr= （ Constr1 ， Constr2 ， Constr3 ） ， 其 中Constr1、Constr2和Constr3分别是图、数据类型和图-OCL约束的集合。目前，对于特定的视觉语言使用哪种约束是开放的。在扩展版本中，具有Meta模型MM=（AT G，Constr）的可视化语言VL由在ATG上类型化的所有属性图组成，其满足Constr中的所有约束。这种延伸具有重要的后果对于模型变换MT：V LS→V LT的语法正确性，因为我们必须要求每个AGS∈V LS不仅存在模型转换AGS通过GT S转换AG T，其中AGT在ATGT上键入，而且AGT满足目标语言V LT的Meta模型MMT（ATGT，ConstrT）的约束ConstrT。由于AGS∈V LSsat-是源语言的约束条件ConstrS，因此我们必须为syn-MT的战术正确性，即相应的转换序列AGS<$AGT与ConstrS和ConstrT兼容。对于图形约束，已经有一些技术可以通过转换来确保满足将图形约束转化为相应的应用条件（参见[16，8，10]）。如何在模型转换的上下文中使用它是开放的。对于作为全局不变式的数据类型约束，在基本情况下没有问题，其中inclusion inc S：ATG SATG和inc T：ATG TATG是数据类型保持。对于规则约束和全局约束，在数据类型敏感扩展的情况下（见4.5.3），[12]中用于代数规范的众所周知的技术可以支持验证过程。然而，在这种情况下如何处理图-OCL约束是完全开放的，并且肯定是与图-OCL约束有关的有趣的研究课题。 对于功能行为和语义正确性，16H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）3→只要不改变模型变换的图形变换系统，就没有直接的后果4.3基于图文法生成的可视化语言定义视觉语言的另一种替代方法是图形语法方法，如DIA GEN[18]或GENGED[3]，其中视觉语言VL由所有可以由相应的图形语法生成的图形给出。作为第3.1节中基本情况的扩展，我们现在考虑这样的情况，即视觉语言VL由类型化属性图文法GG=（AT G，Prod，AG0）生成，其中Prod是一组产生式，AG0是一个属性开始图，两者都是在ATG上类型化的（参见[15，13，10]）。这意味着视觉语言VL由下式给出：V L={AG|AG0AGviaProd} AGgraphsATG对于第3节中考虑的模型变换MT：V LS→V LT，我们现在假设V LS和V LT由类型化属性图文法GGS=（ATGS，ProdS，AG0S）生成的扩展，GGT=（ATGT，ProdT，AG0T）。基本概念的这种扩展对于MT的语法正确性具有以下结果：V LS V LT，其中MT=（V LS，V LT，ATG，GTS）基于GT S=（AT G，Prod）：首先，我们不是从任何图AGS∈VLS开始模型变换，而是从起始图AG0S开始。解决这一问题的方法是对AG0S∈V LS构造一个变换序列AG0S通过GT S生成AGT，使得也存在一个生成变换序列AG0T通过GGT生成AGT，这意味着AGT∈V LT.对于每一个其他的AGS∈V LS，通过定义V LS，我们有一个生成变换序列AG0S通过GGS生成AGS。为了证明AGS的语法正确性，我们建议解决以下混合Concurrence问题：给定AG1S通过GT S的变换AG1T，其中AG1S∈V LS和AG1T∈V LT，以及通过GGS的直接变换AG1S通过AG2S，我们必须构造变换序列AG2S通过GT S的变换AG 2T和AG1T通过GGT的变换AG2T，从而得到以下混合连续图：AG1SviaGTSzAG1T通过GGScz 通过GTS通过GGT茨AG2SZAG2TH. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）317→⇒⇒⇒∈∈⇒∈让我们回想一下，基于GT S的模型变换MT：V LS→V LT在语法上是正确的，如果对于每个AGS V LS，存在通过GT S的变换序列AGS<$AGT，其中AGT V LT。这导致以下结果。事实4.1（模型变换的语法正确性）给定分别由图文法GGS和GGT生成的视觉语言VL S和V L T，那么基于GTS的模型变换MT：V L SV L T在语法上是正确的，如果可解问题和混合一致性问题。证据 给定AG S∈ VL S，通过定义VL S，我们有生成变换序列AG0S通过GG S生成AG S。 解决这个问题会得到一个变换序列AG0T→AGJT→ GG T，其中AGJTV L T。由于混合收敛问题也可以解决：我们有对于每一个分歧-变换序列AG0S的直角变换AG1SAG2SviaGGS→AGS viaGGS一个单一的混合连续图，通过组合导致以下组合的混合连续图：AG0SviaGTSzAGJ通过GGSczviaGTS通过GGT茨AGSzAGT最 后 ， AGJT∈V LT 和 AGJT 通 过 GGT 表 示 AGT∈V LTs. t 。 底 部 序 列AGS→AGT→GT S暗示语法正确性。Q当然，仍然需要找到合适的技术来解决混合收敛问题。 对于第二个问题，可以使用临界对分析的技术来显示类型化属性图转换系统的局部一致性（参见[15，13，10]）。4.4具有操作语义的可视化语言到目前为止，我们只从句法的角度考虑了视觉语言现在，我们扩展的基本概念的视觉语言VL考虑到操作语义的VL。根据[24]，这意味着我们假设有一个模拟规范。在我们的上下文中不18H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）3→⇒在这种情况下，VL的操作语义由下式给出：Sim（V L）={AG}{AG j}|AG，AGJ∈ VL &AG通过GTS（V L）}其中，Sim （VL ）中的每个AG都可以被认为是VL 的模拟场景（参见[24]）。对于在第4节中考虑的模型变换MT：V LS→V LT，我们现在假设我们有V LS和V LT的扩展分别基于类型化属性图转换系统GT S（V LS）=（ATGS，ProdS）和GT S（V LT）=（ATGT，ProdT），给出了一种基于操作语义的这个基本概念的扩展当然对MT的语义正确性有影响：V LS V LT。更确切地说，这种扩展首先允许在以下形式基础上定义语义正确性方法：模型变换MT：基于GT S的V LS→V LT，具有基于GT S（V LS）和GT S（V LT）的V LS和V LT的操作语义分别被称为语义正确，如果对于每个变换序列AG1S→AG1TviaGT S，其中AG1S∈V LS 和 AG1T∈V LT ， 以 及 每 个 模 拟 步 骤 AG1S→AG2SviaGT S （ VLS ） ， 有 一 个 变 换 序 列 AG2S→AG2TviaGT S 和 一 个 模 拟 序 列AG1T→AG2TviaGT S（V LT），导致下面的混合连续图：AG1SviaGTSzAG1T通过GT S（V LS）cz 通过GTS通过GT S（V LT）茨AG2SZAG2T有趣的是，上面语义正确性的混合连接图在形式上与4.3节中语法正确性的混合连接图非常相似。实际上，只有图文法GGS和GGT分别被图变换系统GT S（V LS）和GT S（V LT）所这意味着，正式的技术开发，这是适合解决混合concilience问题，可以应用于显示语法以及语义的正确性。最后，让我们注意到，对于某种应用，放松语义正确性的条件情况可能是不是每个单个模拟步骤AG1S→AG2S→ GT S（V L S）在语义上是有意义的，而是只有合适的模拟序列AG1S→AG2S→ GT S（V L S）才是有意义的。在这种情况下，我们必须用语义上有意义的序列AG1S→AG2SviaGT S（VLS）来代替混合连续图中的单个步骤H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）319⊆→→4.5其他形式扩展除了上面讨论的基本概念的扩展之外，让我们简要地提到一些其他的形式扩展。然而，在这些情况下，分析相应的模型转换的正确性的后果将更加困难4.5.1具有继承的用[4]中引入的具有继承性的属性类型图来代替基本概念中的属性类型图ATGS、ATGT和ATG这是由面向对象范式中的类继承概念，特别是UML Meta模型中的继承概念[25]所激发的，并且允许类型化属性图转换系统和语法的更有效表示，从而允许可视化语言和模型转换的语法和语义。4.5.2基于视图的可视化语言方法在3.1节的基本概念中，我们假设可视化语言VL的Meta模型仅由一个属性类型图ATG组成。与UML的情况类似，我们现在考虑VL的不同视图，这些视图由Meta模型的适当限制定义。更确切地说，我们现在讨论用于视觉语言VL的基于视图的方法，其中VL由不同的视图V1，...，V n，并且每个视图Vi由属性类型图ATG i ATG（i = 1，.，n）。如果V LS和V LT都被不同的视图替换，那么表示模型转换也是有意义MT：VLS→VLT，即模型变换MTi：VLSi VLTi。在这种情况下，关于视觉语言的视图的一致性的众所周知的问题也意味着视图M Ti的模型变换MT。4.5.3数据类型敏感类型图扩展代替在基本概念中考虑的保持数据类型的类型图包含incS：AGTS→AGT和incT：AGTT AGT，我们允许数据类型敏感的类型图包含。这意味着我们还允许不同的数据类型签名DSIGS、DSIG和DSIGT包含DSIGSDSIG和DSIGTDSIG。从实际的角度来看，这似乎合理，因为一般来说，不同的可视化语言V LS的数据类型而V LT也会不同。然而，从理论的角度来看，这种扩展会引起一些问题，因为目前的类型化理论20H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）3M[13，10]中的属性图变换系统本质上是基于一类保持单射和数据类型的属性图态射。5结论类型化属性图转换的概念是一种强大的技术，不仅可以建模可视化语言，还可以定义可视化语言之间的模型这不仅包括这些概念的形式定义，还包括模型转换的正确性，这当然是一个重要的研究课题。关于正确性，我们区分语法正确性，功能行为和语义正确性。本文根据可视化语言和模型转换的基本概念，将可视化语言定义为仅由属性类型图组成的Meta模型，并将模型转换定义为类型化属性图转换系统。在一个案例研究中（见第2节），我们展示了如何定义这样一个从简单的状态图到Petri网的模型转换到目前为止已知的类型化属性图转换理论（参见[15，13，10]）支持根据上述基本概念显示模型转换的功能行为。事实上，[7]中基于临界对的局部连通性定理和终止准则允许验证相应类型属性图变换系统的连通性和终止性。然而，基本概念只允许对可视化语言和模型转换的简单情况进行建模。为此，我们讨论了基本概念的几个扩展，包括应用条件，约束，生成图文法和操作语义。特别地，我们提出了不同类型的约束，不仅包括图和数据类型约束，这些约束已经在文献中研究过[16，8，10，12]，而且类似于UML的OCL约束，一种新的类型化属性图的约束，称为graph-OCL约束（参见[6]）。我们声称，基于属性类型图和所有这些约束的可视化语言和模型转换方法有可能至少与文献中已知的大多数Meta建模方法一样强大[5，1，27]。本文综述了模型变换中基本概念的不同扩展是如何影响模型变换的正确性准则的。当前的类型化属性图转换理论还不能支持扩展的H. Ehrig，K.Ehrig/Electronic Notes in Theoretical Computer Science 152（2006）321理念的但至少它是一个很好的基础，并为未来有关这些问题的研究提供了明确的指示。引用[1] A.阿格拉瓦尔湾Karsai，Z. Kalmar，S. Neema，F. Shi和Vizhanyo A.设计了一种简单的图形转换语言，用于软件和系统建模。Journal on Software and System Modeling，2005。审查中[2] ArcStyler http://www.arcstyler.com网站。[3] R.巴铎一个基于代数图文法的可视化语言的通用图形编辑器。在Proc. IEEE Symposium onVisual Languages（VL[4] R.巴尔多赫Ehrig，K. Ehrig，J. de Lara，U. P