理论计算机科学电子笔记236（2009）5-19www.elsevier.com/locate/entcs模型转换D'enesBisztraya，1ReikoHeckela，2HartmutEhrigb，3a联合王国b德国柏林科技大学软件技术与信息学院摘要模型转换不仅可以用于代码或特定于平台的模型生成，还可以用于指称语义定义，例如使用进程代数作为可视化建模语言的语义。编程语言的指称语义是组合的。为了在模型转换的情况下享受类似的属性，源模型的每个组件在目标模型中应该是可区分的，并且映射与句法和语义组合兼容。由于类型化图是可视化模型的自然表示，因此模型转换通常由类型化图转换来描述。本文提出了一个形式化的定义的组合映射类型图的语义域。为了验证组合性，建立了利用负应用条件的图变换实现映射的一个示例组合转换，映射UML组件图中描述的体系结构模型CSP。关键词：组合性，图变换，范畴论，类型图，模型驱动工程，指称语义1介绍由于可视化语言的广泛使用，出现了模型转换的新应用。模型转换技术不仅用于代码或特定于平台的模型生成，还用于软件重构、语义定义、形式验证甚至架构迁移目的[11]。这些应用程序中的大多数被假定为保持参与者模型的结构，即，它们应该是合成的。组合性是模型转换的一种属性，根据[21]可以以两种不同的顺序组合类似于函数组合，即给定两个变换f：A→B和g：B→C，可以将它们组合为变换gf：A→C。而1电子邮件：dab24@mcs.le.ac.uk2电子邮件：reiko@mcs.le.ac.uk3电子邮件：ehrig@cs.tu-berlin.de1571-0661/Crown版权所有© 2009由Elsevier B. V.出版。CC BY-NC-ND许可证下开放访问。doi：10.1016/j.entcs.2009.03.0116D. Bisztray等人/理论计算机科学电子笔记236（2009）5→O顺序合成显然是任何变换的基本性质，我们感兴趣的是空间合成。空间组合类似于指称语义学的组合属性。对于简单的数学表达式，我们假设表达式2+ 5的含义由2，5的含义和+运算符的语义决定，即[[2+ 5]]=[[2]][[5]]。图1. 组合语义映射在模型转换方面，组合性如图1所示。通过转换sem，将由A、B两个组件和连接器c组成的系统映射到语义域。结果是语义表达式sem（A）、sem（B）和sem（c）的集合，使得它们的组合表示整个系统的语义。组合性是指称语义的一个重要属性，因此也是在现有建模人工制品和语义域之间建立映射的模型转换的一个重要属性。没有组合性，模型转换的模块化规范和验证将是不可能的。图2描述了一个典型的语义验证场景。将建模语言（ML）映射到语义域（SD）并生成编程语言（PL）代码。为了验证语义一致性，编程语言的语义通常必须通过映射PL SD来定义。 如果三角形交换，则生成的源代码在语义上是正确的。虽然不同的模型实例很多，但它们都是由建模语言的基本元素（BE）组成的。 在组合转换的情况下，映射可以根据基本构建块来描述，从而实现各种语义属性的模块化验证。模型和指称语义可以表示为Meta模型的实例。通过类型图和实例图提供了数学模型。模型转换可以用图转换来描述。在本文中，我们提出了一个概念的组合性的任何全函数定义的图之间的图transformation- tions集（表示模型）。给出并证明了简单图变换和具有负应用条件的图变换的组合性条件。BEMLzPL为ZJ，SD图2. 语义验证D. Bisztray等人/理论计算机科学电子笔记236（2009）571212本文的组织结构如下。第二节对相关方法进行了总结.在第3节中正式介绍了组合性。在第4节中，给出了简单图变换的组合性条件，并在第5节中推广到具有负应用条件的图变换。 在第6节中，介绍了组成模型转换的案例研究。第七节是论文的结论。2相关工作关于图变换的验证，已经发表了几篇文章。为了保证结果的唯一性，文[12]提出了重合度和临界对分析的概念在AGG [1]中可以找到一个工作实现，用于检查关键对[5]。终止标准在[6，17]中介绍。AGG [4]中还提供了终止检查的实现。这些定义通过引入变换单元而应用于文[14]中具有基本控制条件的在[21]中讨论了双向转换中的组合性在可用作模型和语义域之间的语义关系的双向转换方面，有两种值得注意的方法：三重图文法（TGG）[20]和QVT [18]。TGG有可靠的工具支持[10]。3形式化组合在本节中，组合性被正式介绍。由于本文中提出的结果是通用的语义域，我们提供了一个一般的，公理化的定义。定义3.1（语义域）语义域是一个三元组（D，±，C），其中D是一个集合，±是D上的偏序，C是一个全函数C[]：D→D的集合，称为上下文，使得d±e=<$C[d]±C[e]（±在上下文下是封闭的）。等价关系是±的对称闭包。源和目标模型及其语义都表示为类型化图。为了清楚起见，我们给出了我们使用的类型化图的定义定义3.2（类型图和类型图态射[7]）给定类型图TG=（VTG，ETG，sTG，tTG），VTG和ETG分别称为顶点和边标号字母表。然后，一个图G的元组（G，type）与一个图态射类型：G→TG一起被称为一个类型图。给定类型图GT=（G1，type1）和GT=（G2，type2），一个类型图态射f：GT→GT是一个图态射f：G1→G2，使得2型<$f=1型。8D. Bisztray等人/理论计算机科学电子笔记236（2009）5\S它认为，（））implies （ ）的情况下（ ）的。G1fG2=12 3 4 5 67J、TG语境的概念是组合性的核心在集合论中，图D在图G中的上下文C由C=GD给出。 上下文C不一定是一个图，因为可能有悬挂边。 为了正确地分离上下文和包含图，我们需要一个特殊的上下文集SC和图集SG。定义3.3（复合性）一个语义映射sem：具有上下文集 SC和图集SG的图 TG→（D，±，C）是复合的，如果对任何内射m0：G0→H0和推出（1），G0，GJ0∈SG，存在上下文E∈SC ，其中sem（H0 ）<$E[sem（G0 ） ]和 sem（ H0J）<$E[sem（GJ0）]G0GJ0（1）JmJ0JH0H0J直观地说，组合性的概念如图3所示。从G生成的语义表达式包含从L通过包含态射m导出的语义表达式。图3. 组合性的直观方法定理3.4假设一个合成映射sem：图TG→（D，±，C）。然后，对于所有变换G=p，mH，通过规则p：L→R，具有单匹配m，sem L±sem R sem G±sem H证明 推出（1）意味着sem（G）<$E[sem（L）]和sem（H）<$E[sem（R）]。L R（一）J JG HD. Bisztray等人/理论计算机科学电子笔记236（2009）59→→→ ◦◦→现在，E[sem（L）]±E[sem（R）]，因为sem（L）±sem（R）和±在上下文下是封闭的。 因此，sem（G）<$E[sem（L）]±E[sem（R）]<$sem（H）Q定理3.4中的陈述对于作为±的对称闭包而得到的关系φ也成立。4基本图变换在第3节给出抽象定义之后，在这一节中，我们证明了由图变换指定的语义映射的组合性的一个条件，没有负的应用条件。 我们假设语义映射sem由一个类型图转换系统GTS=（TG，P）定义，该系统由一个类型图TG和一组类型图产生式P组成。定义4.1（非终止性）一个图G关于一个类型化的图变换系统GTS=（TG，P）是非终止的，如果对G适用的变换系统GTS =（TG，P）∈P。非终止图的符号是G。定义4.2在源图G0上的语义映射sem的结果是sem（G）= G当且仅当存在变换Gp1 G... GpnG，0n规则0⇒1n−1np1，...，p n∈P，它是终止的。重要的是要注意，只有局部连续和终止的[7]变换才能为源图产生唯一的结果。因此，sem也需要局部一致性。定义4.3（可分语义）一个语义映射sem：图TG→（D，±，C）关于一组上下文SC和一组图SG是可分的，如果对于所有的推出（1），G∈SG和C∈SC，它成立，如果H然后是G或者CB G（一）J JC H我们回顾初始推出的定义[7]，因为它在整个论文中被广泛使用。定义4.4（初始推出）给定一个态射f：A AJ，一个单射态射b：B A称为f上的边界，如果存在f和b的推出补使得（1）是f上的推出初始。（1）在f上的初始性意味着，对于每个具有内射bj的推出（2），存在唯一的具有内射bj和cj的态射bj：BD和cj：CE，使得bJb=b，cJc≠c，且（3）是推出。B称为边界对象，C称为关于f的上下文。10D. Bisztray等人/理论计算机科学电子笔记236（2009）5→BBbABB DbJzA(1)F（三）(2)FJJ JJJC阿J CCEcJAC对于变换sem：G0，Gn，我们创建一个bounce图B和一个上下文图C通过初始推出。边界图是G0的最小子图，它包含m0的标识点和悬挂点。下一个定义是语义映射的IPO兼容性。虽然通过未知的上下文E定义了兼容性，但IPO兼容性定义了它通过上下文图的语义定义4.5（IPO相容性）一个语义映射sem：具有集合SC和SG的图TG→（D，±，C）是初始推出相容的（IPO相容的），如果对任意单射m0：G0→H0和m0上的初始推出（2），我们有sem（H0）sem（C）[sem（G0）]和C∈SC，G0∈SG。BG0（2） m0JJCH0引理4.6如果一个语义映射sem：GraphsTG→（D，±，C）具有集合SG和S C是IPO兼容的，那么它也是组合的。证明给定pushout（1）具有单射态射m0：G0H0和初始pushout（2）在m0上.初始pushout的封闭性[7]意味着pushout（2）+（1）在MJ0上也是初始的。B（二）J的g0（1）JGJ0mJ0JCH0H0J由于sem与（2）是IPO相容的，所以sem（H0）∈sem（C）[sem（G0）]且G0∈SG.由于（2）+（1）也是初始推出，sem与它相容，因此sem（H0J）∈sem（C）[sem（GJ0）]，GJ0∈SG. 因此，sem是可比较的，E=sem（C）∈ SC。Q初始保持图变换的定义受到三重图文法的启发[20]。我们假设一个隐式的源模型不被转换影响，而转换构造目标模型。定义4.7（保初值）A（typed）图变换t：G0=零如果Gn关于其初始图G0是非删的，则称Gn是保初始图.一个（类型化）图变换系统GTS=（TG，P）是保初的，如果所有变换序列都是保初的。D. Bisztray等人/理论计算机科学电子笔记236（2009）511→ ± C SS∈ G∈ G虽然初始保留看起来与非删除相似，但是目标模型的元素可以通过转换过程被删除或修改定理4.8（基本组合性定理）一个语义映射sem：具有集合G和C是复合的，如果它是初始保持的和可分离的。证明主要的论点是基于嵌入定理[7]。 对于transfor-mationsem：G0生成Gn，我们创建一个boundaries图B和一个context图C。的边界图是G0的最小子图，它包含m0的标识点和悬挂点.Pushout（2）是m0的初始推出。BBbG0，i，dzGdn GBGsemazG（二）m0J J0塞姆阿a，n（二）Jc00n（3）第一次见面JsemaJC0H0C0H0zHnsemb（4）semb公司简介CmHm由于t是初始保持的，所以上面的一致性图[7]可以与初始推出（2）一起使用。G0代替D，因为它在整个变换中保持不变。因此，m0相对于sem是一致的，并且存在sem和m0上的延伸图[7]。转换sema仅表示sem的特定规则应用顺序。这实质上意味着（3）是推出，并且Hn是sem和m0的推出对象，因此可以在不对H0应用变换sem的情况下确定。当sem（G0）=Gn且husG0≠Gn是终止的时，Hn可能不是终止。不存在于G0中的H0的部分不被sema中的规则转换到语义域，但是上述推理对于C0也成立。C0上的扩张图是pushout（4）和sem（C0）=Cm。Hm的终止也是未知的。根据并发定理[7]，并发生产可以是为bH0Hm和H0Hn创建。 因为变形是初始的-保持，所得到的态射hn和hm是包含（或恒等式），并且存在扩张图（5）和（6）。由于推出是唯一的，所以（5）=（6），因此HA=HB=H。H0semazHnH0hn Hn米（5）hasemb（六）semBJSEMAJCZHBCZHmzHAHmHB这导致下图。 由于G nS和C mC，语义是可分离的，它们是终止的（即，没有语义规则适用），H也必须如果H是终止的，这意味着sem（H0）=H。12D. Bisztray等人/理论计算机科学电子笔记236（2009）5BG0semazGn（二）Jc0了c0（3）第一次见面JSEMAH0JzHnsemB（四）semB（五）semBcz czsemaczCmHmzH根据推出的合成性质[7]，（2）+（3）和（4）+（5）是推出，因此大的（2）+（3）+（4）+（5）平方也是推出。以来H是一个推出对象，H∈=Gn+BCm=Cm[Gn]，这意味着sem（H0）=sem（C0）[sem（G0）]. 因此，sem是IPO兼容的，根据引理4.6，也是作曲的。Q5基于NAC的第四节证明了具有不可删规则的图变换的组合性。然而，为了控制转化，还需要使用负应用条件（NAC）可分离语义的定义（定义4.3）在允许存在否定应用条件的情况定义5.1（负应用条件[7]）一个简单的负应用条件是NAC（x）的形式，其中x：L→X是态射。态射m：L→G满足NAC（x），如果在MJ中不存在态射p：X→G，其中p≠x=m：Lx XMpJ，sG在定理5.6成立之前，给出了必要的定义。定义5.2（粘合和创建点）给定一个（类型化的）图生成p=（L<$-1K-→rR）。• 胶合点GP是L中不被p删除的那些节点和边，即GP=1V（VK）=1E（EK）=1（K）。• 所创建的点CP是R中由p创建的那些节点和边，即CP=rV（VK）\VK<$rE（EK）\EK。D. Bisztray等人/理论计算机科学电子笔记236（2009）513图4. 带创建点的14D. Bisztray等人/理论计算机科学电子笔记236（2009）5⊆⊆→ ± CS创建点的概念如图4所示。由于C节点被删除，因此仅有的粘合点是两个A节点。它们不会被图中的规则删除。 四、 所创建的点是 统治可能的是，B节点总是-如果存在的话-在图转换系统的每个产生式规则中的粘合点。 这意味着节点类型B是一个特殊的类型，它的实例永远不会被删除。 这一观察导致了已经存在于开始图中的常量类型的定义，而不是在整个转换过程中删除定义5.3（常量类型）给定一个类型化图变换系统GTS=（TG，P）。常数类型CT TG=（V CT，E CT）是类型图T G中的那些节点和边，它们的实例不被任何产生式p ∈ P删除或修改。 即 CT={v ∈ V TG|<$p ∈ P：v = type V（w）<$w ∈ GPpi}<${e ∈ETG|<$p ∈ P：e =type E（f）<$f ∈ GP pi}.在实例图中，常量点是常量类型的那些节点和边。构造性变换的定义受到三重图文法的启发。虽然NAC仅包含非常数元素，但初始图仅由常数点组成。这样一来，国家艾滋病理事会就可以集中精力处理转型的目标要素。定义5.4（构造变换）一个图变换t：G通过嵌入m0：G0→H0具有NACs的Gn是构造性的，如果(i) G0和H0只包含常值点，即 （G0）型、（H0）型、CT型。(ii) 所有NAC都由非恒定点组成，即， 对于每个NAC（n），n，pw的L→N具有n∈x∈N\n（L），其中type（x）∈/CT推论5.5一个构造性的快速变换：G_（？）保持初始值，因为G由不通过变换删除的常数点组成。定理5.6（nacs的合成性定理）给出一个语义映射sem：具有集G和SC的图TG（D，P）由具有常数类型CTTG的图变换系统GTS=（TG，P）描述.那么，如果它是可分离的和建设性的，它就是组合的。证明该证明基于基本组合性定理。为了将嵌入定理应用于定理4.8的证明中，证明了当存在NAC时，m0和c0由于等效的左NAC可以从右NAC构造，因此在整个证明中，如果没有明确相反地说明，则假设NACs是左NAC。在NAC的情况下，如果变换不仅是边界一致的[15]，而且是NAC一致的[16]，则扩展图存在。根据并发定理的综合构造，给出了一个并发规则pc和一个并发匹配D. Bisztray等人/理论计算机科学电子笔记236（2009）515z1，s∀∈ni←−←−−→、→→、gc存在[7]。并发规则pc基本上是一个specific的所有规则的合并sem：G0表示生成目标图Gn的规则应用顺序通过在源图G0上应用pc。在包含NAC的图转换中，对于并发规则pc存在并发NACpc。为了实现NAC一致性，我们必须证明，|= NAC pc，其中NAC pc是并发NAC，g c是由t诱导的并发匹配，k0：G0→H0是包含态射[16]。由于（H0）型<$CT，这从引理5.7得出，因为满足任意NAC的态射q：NC→H0的存在将意味着对于x∈NC\n（LC ）且type（x）∈/CT ，也有type（q（x））=type（x）∈/CT，其中ch与（H0）型<$CT是矛盾的。Q引理5.7p c的所有NAC都是非常数的，前提是pP具有非常数NAC。用数学归纳法对sem的长度进行了推导：基础 n=1. 我们有pc=p0，它具有假设的性质。G n.诱导步骤。 考虑tn：G0<$nGn<$Gn+1，通过规则p0，p1，.， pn. We可以通过y归纳法假设pJ=N<$−LJ <$−K J−→RJ（中国中国NJp0，p1，...， p n−1）和p n：N jL nK nR n具有非常数NAC。我们必须证明所有的NACs都是非常数的。Ni，Nj，，，nei，injJ，，NiJ（一）LJc，，KcJRcJNjJ（三）Ln，，Kn Rn，，nJMceJc，，nJjenJlJz，sJrJgcJLc，， Cc，，KC（二）E，，_CnRcKngn+1gcKch公司简介tJzJHCJG0，，DnZJZJGn，， DGn+1根据并发定理与NAC的综合构造，由yG0=n+n1Gn+1导出的pc与NACs的并发规则为pc=Lc<$l−k−cKc−r−k−n Rc（匹配gc：LcG0，匹配hc：RcGn+1）。并发NAC pc由两部分组成。情况1nJi：LC→NiJ定义为ni：LJC→NifrompJc。通过构造性的假设ii，我们有一个v∈xi∈Ni\ni（LJC），其中t型（xi）∈/CT。 设xJi=ei（xi），使得t ype（xJi）=t ype（xi）∈/CT. 更进一步，xJi∈NiJ\nJi（LC）、我16D. Bisztray等人/理论计算机科学电子笔记236（2009）5因为否则pushout和pullback（1）意味着，ni（yi）=xi，因此xi∈ni（LJC），这是一个矛盾。因此，nJi是不恒定的。壳体2nJjJ：LC→NJj定义为nj：Ln→Nj，其中nJj：E→Nj通过推出（3）−（5）。NjJJ，，Z，，NjJ，，nJjJ（五）（四）nJjLc，，Cc E如果（4）的推出补数Cc不存在，则导出的NAAC总是为真。通过假设pn有xj∈Nj\nj（Ln），其中t ype（xj）∈/CT. 因为（3）是一个推出和拉入back，所以有nXJj=z1（xj）∈Nj\NJj（E）和type（XJ）=type（xj）∈/CT. 同样，使用推出（4），其中t ype（y j）=t ype（XJj）∈/CT，其中（Z → N j j）（y j）= x jj。最后，<$xJjJ=（Z→NjJJ）（yj）∈NjJ J\njJJ（LC）because（5）是apushout anddpullback，其中ty pe（xJjJ）=type（yj）∈/CT。 你是我的朋友常数Q6应用于案例研究组合性是类型化图变换在语义验证领域的一个重要性质。在这一节中，我们将使用[3]中所提到的映射来给出所提出的理论概念为了改善软件系统的内部结构、性能或可伸缩性，引入了称为重构的行为保留更改[9]。由于今天的应用程序趋向于面向服务，我们处理重构商业工作的宣传片。我们使用UML活动图指定服务实例执行的工作流程[19]。 UML的相关片段的语义表示为一种指称风格，使用CSP [13]作为语义域，并通过图形转换规则定义从UML图到CSP过程的映射。 行为保持的语义关系可以使用CSP过程上的一个精化和等价关系来表示，并使用FDR2 [8]进行检查6.1CSP简介在本节中，我们简要介绍CSP的必要概念。一个进程是一个组件的行为模式，它包含一系列事件。过程是使用递归方程定义的，称为过程函数。 第6.2节中使用的ProcessExpressions基于以下语法。P：：=事件→P|P||Q|R，，D. Bisztray等人/理论计算机科学电子笔记236（2009）517±||→PrefixOperatora P执行actiona，然后行为类似于P。并发进程P Q的行为就像P和Q参与锁步同步一样。形式上，UML模型是由属性类型化图表示的元模型的实例。 CSP的抽象语法也可以表示为一种打印的图表。 CSP的基于类型图的元模型在[2]中定义。 这 这样，语义映射可以定义为类型化图转换。CSP是定义3.1意义上的语义域。D是CSP表达式的集合，可以是跟踪，失败或发散细化，因为它们在上下文下是封闭的[13]。上下文是过程表达式E（X），其中唯一出现一个可区分的过程变量X。6.2执行虽然变换机制受到TGG的启发，但变换是在Tiger EMF Transformer [22]中实现的，因此它是单向的。图5. 操作和活动边为了在实践中提出定义，在下面的.图5显示了它们的具体语法。图6和图7中的规则负责创建边缘流程，以及将边缘流程编织到从操作创建的事件。属性值A和B表示在规则的两侧具有相同值图6.边缘规则的实现图6中的边规则为相应的边创建了过程定义。在CSP表达式上定义的NAC检查是否存在类似的过程定义。如果不存在，则匹配的边尚未被变换。因此，它创建了空的A=过程定义。图7中的Action规则从相应的action创建一个事件，并将其插入到相关流程的定义中。NAC仅由CSP表达式组成，其工作方式与Edge规则中的工作方式相同18D. Bisztray等人/理论计算机科学电子笔记236（2009）5SSS图7. 行动规则6.3组合性证明这种语义转换是复合的，如果它是终止的，局部连续的，可分离的，整合的和建设性的。在AGG [1]中，可通过临界对和终止分析来证明终止性和局部连续性语义映射基本上读取架构模型并创建相应的CSP表达式集。这些规则都不会删除从CSP元模型中键入的任何元素。因此，CSP元模型的所有元素都是稳定类型，因为它们的所有实例都是这个语义映射中的稳定点。 此外，NAC仅在CSP表达式上定义。这三个观察结果与定义5.4的假设相对应，因此转换是建设性的。为了证明可分性，需要定义集合SC和SG我们定义一组图AD代表两者。AD是H0的一组子图，使得如果G中存在ActivityNode，则所有传入和传出的ActivityEdges连 接 到 节 点 的 节 点 也 应 该 存 在 。 由 于 sem 中 的 每 个 转 换 规 则 都 将 单 个ActivityNode转换为语义域，因此每个节点类型在sem中都有相关的产生式规则。当ActivityEdges被转换为进程时，它们在ActivityNode周围形成一个框架，从而实现它们的转换。因此，边界图仅由ActivityEdges组成。如果所有传入和传出的ActivityEdges都包含在相关节点中，则在子图中触发所有相应的规则因此，在启用先前禁用的规则的合并过程中不会创建新的结构。因此，如果C0和G0是AD的，那么如果C0和G0是终止的，那么H也是。7结论本文对类型图和语义域之间的映射给出了组合性的概念。语义映射用类型化图变换表示。作为主要结果，组合性的条件已被建立简单的图变换以及具有负应用条件的图变换，并定义了必要的概念。 给出了一个组合转换的例子，D. Bisztray等人/理论计算机科学电子笔记236（2009）519图为CSP。未来的工作包括基本控制结构的图变换研究以及高级控制流程的研究。确认这项工作部分由SENSORIA项目IST-2005- 016004赞助。引用[1] AGG -属性图语法系统环境（2007）。URLhttp://tfs.cs.tu-berlin.de/agg[2] Bisztray，D.和R. Heckel，使用CSP的业务流程转换的规则级验证，在：第六届图形转换和可视化建模技术国际研讨会（GTVMT[3] Bisztray，D.，R. Heckel和H. Ehrig，Verification of architectural refactorings by rule extraction，in：Proc. of Fundamental Approaches to Software Engineering（FASE[4] Bottoni，P.，M. Koch，F. Parisi-Presicce和G. Taentzer，高级替换单元的终止与模型转换的应用。，电笔记理论。Comput. Sci. 127（2005），pp. 71比86URLhttp://dblp.uni-trier.de/db/journals/entcs/entcs127.html#BottoniKPT05[5] Bottoni，P.，G. Taetzer和A.Schuürr，基于关键点分析和上下文分层图变换的视觉语言的有效分析，在：IEEE视觉语言国际研讨会（VL'00）会议录，IEEE计算机协会，2000年，第100页。59.[6] Ehrig，H.，K. Ehrig，J. deLara，G. Taentzer，D. Vo和S. V'o-G yap ay，模型转换的判定准则，in：M.Cerioli ， editor ， Proc. of International Conference on Fundamental Approaches to SoftwareEngineering（FASE49-63.[7] Ehrig，H.，K.埃里希大学Prange和G. Taentzer，[8] Formal Systems Europe Ltd， FDR2用户手册（2005）。URLhttp://www.fsel.com/documentation/fdr2/html/index.html[9] Fowler，M.，K. Beck，J. Brant，W. Opdyke和D. Roberts，[10] Fujaba工具套件（2007）。网址http://wwwcs.uni-paderborn.de/cs/fujaba[11] 赫克尔河，R.科雷亚角马托斯，M。El-Ramly，G. Koutsoukos和L. Andrade，[12] He ckel，R.， J. M. Küster和G. Tae ntzer，类型属性语法转换系统的构造，在：Proc. 第一届国际图形转换会议（ICGT '02）（2002年），pp. 161-176。[13] 霍尔角A. R.，[14]Küster，J. M.，模型转换、软件和系统建模的定义和验证5（2006），pp. 233-259.[15] 兰伯斯 湖具有负 面应用条件 的粘合剂高水 平替换系统 ，技 术报告，Te c hnis cheUni versit？atBerlin（2007）。[16] 兰伯斯湖H. Ehrig，F. Orejas和U. Prange，具有负面应用条件的粘合剂高水平替换系统，在：Proc. 应用和计算范畴理论研讨会（2007）。[17] Levendovszky，T.，联合Prange和H. Ehrig，具有内射匹配的dpo变换的终止准则，电子。注意Theor。Comput. Sci. 175（2007），pp.87比10020D. Bisztray等人/理论计算机科学电子笔记236（2009）5[18] MOF Query/View/Transformation（QVT）Final Adopted Specification（2005）.URLhttp://www.omg.org/docs/ptc/05-11-01.pdf[19] OMG，统一建模语言，2.1.1版（2006）。URLhttp://www.omg.org/technology/documents/formal/uml.htm[20] S chürr ，A.，具有三重graph grammar s的grapht ranslators的性能，在：P roc。 的中间体 WorkshoponGraph-Theoretic Concepts in Computer Science （ WG'94 ） ， Lecture Notes in Computer Science903（1994），pp. 151-163.[21] Stevens，P.， QVT中的双向模型转换：语义问题和开放性问题，在：第10届模型驱动工程语言和系统国际会议（MODELS1-15。[22] 团队T D、 网址http://www.tfs.cs.tu-berlin.de/emftrans
