模型转换验证：理论计算机科学电子笔记292（2013）5-25

可在www.sciencedirect.com在线获取理论计算机科学电子笔记292（2013）5-25www.elsevier.com/locate/entcs模型转换的验证--模型转换的研究现状综述Daniel Calegari1乌拉圭蒙得维的亚Repu'blic大学诺拉·萨斯2FacultaddeIngenier'ıa乌拉圭ORT大学乌拉圭蒙得维的亚摘要在模型驱动工程范式中，软件开发基于模型的定义，ELS提供要构建的系统的不同视图和支持（半）自动开发过程的模型转换。为了提高使用这种模式开发的产品的质量和可靠性，模型和模型转换的验证至关重要。 在这种情况下，模型转换的验证有三个主要组成部分：转换本身，所处理的感兴趣物业，以及用于确定物业的验证技术。在本文中，我们提出了一个详尽的文献分析这三个组成部分的模型转换的验证。我们还采取了基于问题的方法，举例说明了可以在模型转换上验证的感兴趣的方面，并展示了如何做到这一点。最后，我们得出结论，需要一个集成的环境来解决模型转换的异构验证保留字：模型驱动工程，模型转换，形式验证。1引言每个传统的软件开发生命周期都由许多人为因素（例如，需求规范、分析和设计文档、测试套件、源代码）支持，这些人为因素主要用作开发指南以及与利益相关者的通信工具。模型驱动工程（MDE，[49]）范式通过设想由工件驱动的软件开发生命周期将这种观点推向了极限，1电子邮件地址：dcalegar@fing.edu.uy2电子邮件：szasz@ort.edu.uy1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2013.02.0026D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5表示要构建的系统的不同视图的模型。它的可行性是基于存在一个（半）自动化的建设过程驱动的模型转换，从抽象的系统模型，并将它们转换，直到生成一个可执行的模型。因此，整个过程的质量在很大程度上取决于模型和模型转换的质量。我们关注模型转换，特别是它们的验证。从这个意义上说，对模型转换进行验证的最低要求是转换以及源和目标模型都是格式良好的。然而，还有许多其他属性可以验证，有太多的验证方法可以做到这一点。这个主题在[2]中被分析为一个三维问题，包括：所涉及的变换，所涉及的感兴趣的属性，以及用于建立属性的形式验证技术。本文的目的是对文献[2]中关于模型转换验证的工作进行全面的回顾。特别是，我们介绍第一个维度而不深入，因为有着名的作品[67，26]讨论这个主题，我们扩展了第二和第三个维度，并在[2]中没有讨论其他方面。我们还遵循基于问题的方法，通过案例研究来举例说明可以在模型转换上验证的感兴趣的方面以及如何验证它们。最后，我们得出结论，需要一个集成的环境来解决模型转换的异构验证本文其余部分的结构如下。我们首先在第2节中详细介绍审查过程。然后，在第3节中，我们快速查看模型转换并定义一个运行示例。在第4节中，我们介绍了必须被验证的转换的不同方面，在第5节中，我们回顾了这些方面在文献中是如何被验证的。在第6节中，我们使用运行的示例来验证属性，并讨论如何验证它们。最后，在第7节中，我们就这一主题提出了一些结论性意见和未来工作的指导方针。2关于文献综述按照系统综述方法的相关流程进行文献综述[50]。我们专注于回答这个问题：哪些策略被用来处理模型转换的验证，以及它们试图解决什么样的问题？该过程分两步进行：（a）在电子数据库中进行网络搜索，以及（b）对作者、会议和参考文献进行并行搜索，以执行网络搜索结果。第一步，首先确定关键词D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）57rect，Springer，IEEEDigitalLibrary，andACM Digital Library，throughtheTimb'oportal3.检索应用于这些数据库中论文的标题、摘要和关键词，或者在我们不允许将检索限制在这些领域的情况下，检索应用于所有检索第二步是通过寻找[2]中引用的论文来加强第一步，并确定与该主题相关的作者和会议通过作者列表，我们在他们的个人网页以及DBLP数据库中进行了第二步帮助我们找到了一些技术报告和小型会议材料，并使我们能够跟踪一些作者工作的演变纳入标准是基于对所发现论文的标题、摘要和关键词的审查，评估它们是否以某种方式回答了最初的问题。我们审议了用英文和西班牙文写的两份文件。通过阅读全文，对这套最初的论文进行了修订。虽然有些论文不能被认为是高质量的，因为他们没有经过严格的审查过程后发表，我们特权的内容，有利于回答最初的问题。由于篇幅原因，我们在此不包括完整的文献综述。这项工作的扩展版本与每篇论文的描述可以在[18]中找到。第3章模型转换在MDE生态系统中，一切都是模型，甚至代码也被认为是模型。在这种情况下，模型是系统或其环境的抽象。每个模型都遵循一个元模型，即引入某种模型的语法和语义的模型。同样地，一个元模型符合某个元模型。元元模型通常是自定义的，这意味着它可以通过自己的语义来指定元模型通常使用UML类图来定义[36]。然而，还有其他几种专用语言用于此目的，例如MetaObject Facility（MOF，[35]），为Eclipse建模框架定义的Ecore元数据模型（EMF，[31]）和Kernel MetaMetaModel（KM 3，[5]）。除了元模型定义了一种通常具有具体语法的建模语言之外，还可以使用与元模型相同的语言来表示模型。此外，对于表示模型实例，以及作为元模型的一种“实例”的模型最后，层次结构中的每个元素都可以使用XML元数据交换（XMI，[39]）表示。在某些情况下，有一些条件（称为不变量）不能被这些语言的结构规则捕获，在这种情况下，建模语言补充了另一种逻辑语言，例如对象约束语言（OCL，[38]）。让我们介绍一个著名的类到关系模型转换的例子，它最初在[10]中介绍，后来成为事实上的标准3Timbo。http://www.timbo.org.uy/8D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5Fig. 1. 类和关系元模型模型转换的例子我们将使用[47]中提出的变换图1左侧的元模型定义了UML类图，其中的类可以包含一个或多个属性，可以属于一个类层次结构，并且可以声明为持久的。 每个属性都有一个类型，该类型可以是另一个类或原始数据类型（字符串、布尔、整数等）。属性可以被定义为主要属性。关联是在类之间定义的，具有从源到目的地的方向。一个额外的约束是每个类必须至少有一个属性和至少一个主属性（它们可以被继承）。另一方面，关系模型符合图1右侧的元模型。每个模型都包含一些表和一些列。其中一些列是相应表的主键。表可以与零个或多个外键相关联。每个外键都引用一个表，并与构成该键的多个列MDE范例的第二个构建块是模型转换，它也可以被认为是一个模型。正如[26]中所指出的，模型转换与程序转换密切相关。“Their differences occur in themindsets虽然程序转换系统通常基于面向数学的概念，如术语重写，属性语法和函数式编程，但模型转换系统通常采用面向对象的方法来表示和操作其主题模型。Kleppe等人[51]将模型转换定义如下：一个转型的定义。转换定义是一组转换规则，它们共同描述了源语言中的模型如何转换为目标语言中的模型。转换规则描述了源语言中的一个或多个结构如何转换为目标语言中的一个或D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）59图二、模型转换概述如从[6]中提取的图2所总结的，模型转换基本上将符合给定源元模型MMa的模型Ma作为输入，并产生符合给定目标元模型MMb的另一模型Mb作为输出。模型转换可以被定义为模型Mt，它本身符合模型转换元模型Mmt。最后一个元模型，以及MMa和MMb元模型，必须符合一个元模型（比如MOF或Ecore）。转换定义由转换引擎执行。该模式定义了模型到模型的转换。还有模型到文本和文本到模型的转换，其中目标和源模型，re-models，只是不符合任何特定元模型的字符串。在不失一般性的情况下，我们将只考虑模型到模型的转换（从现在开始只是转换，或模型转换）。正如[67，66]中所指出的，然而，这种模式可以扩展，因为在[26]中进行了详尽的研究撇开细节不谈，作者识别了模型转换的多种可变性，例如，它可以是双向的，它可以将多个源模型作为输入和/或产生多个目标模型作为输出，它的规则应用策略可以是确定性的、非确定性的或交互式的，源模型和目标模型可以处于不同的抽象级别或不处于不同的抽象级别（水平转换与垂直转换），源模型和目标模型可能符合相同的元模型，也可能不符合（内源转换与外源转换）。除了这些方面之外，还有几种定义和执行模型转换的方法，从直接操作，其中转换通常是在访问模型的内存表示的编程语言中开发的（例如Java元数据接口[27]），到关系（也称为关系）。声明式），包括将转换规则定义为源元素和目标元素之间的数学关系（例如查询/视图/转换（QVT）关系[37]），通过基于图转换，包括将模型视为类型化属性标记图并应用图转换技术10D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5图3.第三章。类到关系转换的源模型和目标模型(e.g.[83]第83话在我们运行的示例中，转换基本上描述了持久类如何转换为表。类的属性和关联被转换到相应表的列中，并且主键和外键也被适当地设置。主键是为定义为主要的属性定义的，外键是为与其他类（包括类层次结构中的类）的关联定义的。下面我们展示了使用ATL声明性符号的持久类到表规则定义。转换使用了一个预处理步骤，该步骤将类的特征（属性或传出关联）以高质量的方式表示。有了这个中间结构，定义规则就更容易了，下面的规则将持久化类映射到表。rulePersistentClass2Table{ fromc： SimpleClass！类（c.is_persistent和c.parent.oclIsUndefined（））到t：SimpleRDBMS！表（名称<-c.name，<- c.flFeatures->select（f |not f.isForeignKey）->collect（ft|跟踪），pkey<- c.flFeatures->select（f |f.isPrimary）->collect（ft|英尺迹线），fkeys<-c.flFeatures->select（f |f.isForeignKey））}在图3中，有一个源模型的例子（在UML类图符号中，带有构造型）和它对应的目标模型（在类似KM 3的符号中）。4验证什么？在本节中，我们将关注[2]中介绍的第二维：通过验证模型变换来解决的感兴趣的也有其他作品[56，84]通过定义要处理的属性集来引入验证问题。不过，这些建议的内容，大部分都包含在前一项建议内。因此，我们提出了[2]中确定的属性类别接下来，我们解释每个类别，而不深入[2]中已经提出的那些方面，并在必要时扩展它们以添加更多（子）类别。我们还包括在其他作品中使用标准化命名法处理的属性。D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5114.1存储相关属性这个类别指的是转换的计算性质和转换语言的如[2]中所介绍的，转换规范符合可以拥有自身属性的转换语言在这种情况下，有四个感兴趣的属性前两个属性被标识为执行时属性。它们是Termination属性，它保证目标模型的存在，即转换执行完成任何格式良好的转换规范，以及Determinism（a.k.a.一致性）属性，该属性确保目标模型对于给定源模型和转换规范的唯一性。这些属性与充分表达（即图灵完备）变换语言的不可判定问题有关在这种情况下，“[…]正式证明它们不能依靠一个特定的转换的规范来完成【...】要么TL [转换语言]保持尽可能的通用（和强大），使这些属性不可判定，但转换框架提供了检查足够条件的能力，确保它们保持特定的转换;或者这些属性通过TL的构造来确保，通常通过牺牲其表达能力来确保根据这一点，在第一种情况下，当证明特定的变换规范时，这些性质也可以被识别为与变换相关的性质（如下一节所定义第三个属性，被标识为设计时属性，是类型，即确保转换规范w.r.t.的格式良好转换语言。类型检查的过程可能发生在编译时或运行时。由于模型转换是模型，并且模型具有元模型（定义转换语言），因此这个问题的解决方案与Conformance和Model Typing密切相关，这将在下一节中介绍最后，我们引入了第四个属性，在[2]中没有提到，执行语义保持属性。这个执行时间属性声明转换执行必须按照转换语言语义的定义按预期进行与此相关，并且与Typing属性密切相关，转换规则之间也必须保持一致性。例如，某些语言不允许输入模型的元素被匹配多次（冗余问题）。如果这个属性不成立，则可能应用矛盾的规则，例如，两个规则应用于同一元素，意味着不同的事物。此外，应用于层次结构的元素的规则可能比应用于同一层次结构的较低级别中的元素的另一规则更具限制性。在这种情况下，会有一些模型不符合第二条规则。4.2转换相关属性这个类别指的是转换的建模性质。如[2]中所介绍的，转换是指需要确保转换正确行为12D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5在这种情况下，验证的第一步是严格关注转换所引用的属性的这个子类别称为在源/目标模型上。正如[84]中所指出的为了保证生成的模型是目标语言的语法结构良好的实例[w.r.t.结构性和非结构性限制]。这引入了第一组属性，称为连接和模型类型。Concrete现在已经很好地理解并在建模框架中自动检查。还有第二组称为N-Ary Transformations Properties：同时在多个模型上操作的转换，例如模型组合，合并或编织，需要检查专用属性但核查的利益超出了这类问题。当验证一个模型变换时，我们希望将其元素作为一个整体而不是单独考虑。在这个意义上，一些作者，如[16]，使用转换模型的概念，即由源和目标元模型，转换规范和良构规则组成的模型。这种转换模型可以是隐式的，也就是说，我们假设每个元素都是连接的，或者是明确的，也就是说，我们真的构建了一个具有不同目的（例如跟踪或验证）的统一结构。这个模型陈述了元素是如何相互关联的，这些关系引入了一些句法和语义问题。从这个意义上说，有一些属性称为Model Relationship，它们将源元模型的元模型元素和目标元模型联系起来，试图确保任何输入模型的某些元素或结构将被转换为输出模型的其他元素或结构。当这些关系不能仅仅通过查看单个转换规则来推断时，或者当转换语言不允许表达某些关系并且必须使用另一种约束语言时，就会出现这个问题。这也被称为保持变换不变量或结构对应。除了源模型和目标模型之间的结构关系之外，还有一些语义属性必须保留，称为模型语义关系，也称为语义正确性或动态一致性[84]。这些属性一般依赖于元模型的语义或转换的种类一些感兴趣的属性是语义等价，（弱）双相似性和属性保存，时间属性，重构和细化。最后，我们添加了第四个类别，称为函数行为，在[2]中没有考虑，它指的是确定变换是否表现为数学函数。特别地，变换可以是单射的、满射的、双射的或至少是可执行的（即，存在满足变换的有效的源和目标模型对还可以考虑转换中的各个规则来分析这些属性。这些属性在[16]中介绍。此外，还有一个特殊的属性称为语法完整性，它指的是（在某些情况下）需要通过转换规则完全覆盖这也在[56]中作为元模型覆盖提出，它引入了一个问题，如果转换不D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）513覆盖整个元模型，那么这会导致一些无法转换的输入模型。从功能的角度来看，句法完整性意味着转换是一个整体功能。当考虑一个特定的变换时，决定性也是一个函数属性。事实上，正如[16]中所介绍的，当一个变换是完全的和确定的时，它被称为函数的。4.3总结发言我们已经看到了通过模型变换的验证来解决的感兴趣的属性的分类。这种分类以前在[2]中介绍过，它识别了语言相关和转换相关的属性，第一个属性涉及转换的计算性质和转换语言的目标属性，第二个属性涉及转换的建模性质。我们通过添加两个子类别来扩展此分类，这些子类别基于其他相关作品来处理属性当遵循基于MDE的软件项目时，正式验证主要集中在第二类属性（与转换相关）上，而第一类属性（与语言相关）通常被认为是由开发工具自动验证的文献中所述性质的总结见表1.一、5如何验证？正如[30]中所指出的，一个属性可以被验证或确认，这导致了验证和确认之间众所周知的区别形式上，验证的目的是满足所施加的条件换句话说，验证是证明我们正在以正确的方式构建产品的过程，而验证是证明我们正在构建正确的产品的过程。我们专注于验证，特别是形式验证，即使用形式方法进行验证。虽然形式验证技术可能很昂贵，但它们有助于保证关键应用程序的正确性，而其他验证技术是不可接受的。与形式验证相反，还有其他技术可以检测错误或提高置信度，但它们不能以确定的方式证明任何属性在本节中，我们将重点介绍[2]中介绍的第三个维度：用于建立属性的形式验证技术我们通过定义两个新的验证技术类别来扩展以前的5.1推理、模型检查、测试、静态分析或构造我 们 介 绍 这 第 一 类 ， 它 指 的 是 用 于 验 证 的 技 术 逻 辑 推 理 （ 英 语 ： Logicalinference）定理证明）包括使用数学14D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5表1文献中讨论的特性总结存储相关属性终止[15][28][29]决定论[2016- 05 - 24][ 2016 - 05 - 24][2016-05-24][2016 - 05 -05]打字[52][62]、[81]保存执行。Sem等[2016- 04- 25][2016- 04- 25][2016 - 04 -25]转换相关属性源/目标一致性[2009年12月27日][2009年12月27日][2009年12月27日][60][61][58][59][76][79][82]n元[22][48][68]联系我们[25][26][27][28][29][2010 - 10-15][60][61][58][70][73][76][80]语义关系一般[17][59][76][82]第二届世界卫生大会Sem等当量[12][23][44][58]第二届世界卫生大会[71][74][78][84]第二届世界杯足球赛时间[25][30]第二届世界卫生组织大会重构[第四十二届]细化[19][65][77]功能行为一般[16个]合成Comp.[25][40][56][58][75][87]一个系统的表示和必须被验证的属性，以及该语义域中允许对该表示进行推理的逻辑，从前提到结论。这个过程通常使用- orem证明软件进行，并且通常只是部分自动化。模型检查也包括使用系统的数学表示，证明包括对数学模型的系统详尽的探索。第一种方法通常有很高的验证成本，而第二种方法有众所周知的局限性，如状态爆炸问题。另一方面，测试依赖于为属性构建测试策略，包括根据这些策略随后执行系统（部分或全部）。虽然测试通常被认为是一种验证策略，但它也可以用于验证目的。然而，众所周知，测试只能显示错误的存在，而不能显示错误的不存D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）515在。最后，我们可以找到基于静态的策略16D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5分析，即对模型转换的分析，而不是实际执行它。静态分析通常包括半决策技术。从这个意义上说，它们是有效的，但它们不能保证设计的整体正确性。为了完整性，我们还考虑了通过构造变换而保持的性质的满足，例如。通过使用特殊的转换语言，如DSLTrans [8]。5.2元模型或模型级别此类别由抽象级别w.r.t.转换中涉及的元素，它也被称为在线和在线验证[4]，以及输入无关和输入相关验证[2]。元模型级验证使用元模型信息来验证任何格式良好的模型实例的属性，而模型级验证使用任意源模型。正如[84]所指出的正因如此，第二种在很多情况下是一种实用而有价值的辅助手段，但它无法确保零故障水平质量，因为它检查了有限数量的具体情况。然而，由于模型级验证发生在较低的抽象级别上，因此可以验证的属性范围比使用元模型级验证时要大得多5.3规范或实施正如[30]中所介绍的，验证可以在模型（规范）级别或实现级别上完成。规范级验证只涉及在某些转换语言中对转换的规范，以及因此为该转换语言定义的语义。相比之下，实现级验证还意味着考虑转换引擎执行转换的方式。据我们所知，在文献中发现的验证技术是第一种类型，因为它假设任何转换引擎都符合转换语言的语义，并且属性不依赖于转换的执行方式，包括确定性、终止和执行语义属性的保持5.4变换独立或依赖在[2]中引入了这个维度。变换独立技术是那些证明任何变换的性质的技术，因此它们确保没有对特定源模型做出任何假设。相反，依赖于变换的技术依赖于特定的模型变换。转换独立性可以通过默认保留属性的转换语言来实现，也可以通过构造转换来确保属性。D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5175.5总结发言我们已经展示了如何将验证技术分为不同的类别：（a）用于验证的技术类型，（b）抽象级别w.r.t.转换中涉及的元素，（c）抽象级别w.r.t. 转换的实现，以及（d）依赖/独立w.r.t转换规范。值得一提的是，这些类别是正交的，即存在对应于一个以上类别的验证技术。该分类中文献中讨论的验证技术总结见表2。6通过实例在本节中，我们回到第3节中介绍的类到关系的例子来说明几个验证属性，并讨论如何解决验证问题。6.1连接和模型类型除了基本的一致性需求之外，通常还有建模语言的结构规则无法捕获的不变量。不变量是格式良好的规则，对于任何符合Meta模型的模型，这些规则必须始终保持.不变量可以在元模型、元模型和模型上定义。在这个例子中，以下不变量必须在模型上保持不变• 所有关联都有不同的名称（类也是如此）• 一个类的所有属性在它的所有者类和它继承• 在类的父关系中没有继承循环• 如果一个类是持久的，那么它的所有超类也是持久的。• 如果一个类是持久化的，它至少有一个属性标记为primary• 所有表都有不同的名称• 表中的所有列都具有不同的名称• 每个表必须至少有一个主列。此外，模型上可能的不变量有：• 所有的家庭都有不同的名字• 每个人在一个家庭中都有一个独特的名字不变量可以使用像OCL这样的约束语言来表示，在第4节中已经说过，这种一致性检查现在是使用自动检查器在建模框架这些检查器可以基于SAT求解器或模型检查，如[3，32]所示。这种验证是在模型级别进行的，但也有其他替代方法，例如使用逻辑推理进行验证。在这种情况下，我们可以形式化元模型、模型和18D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5表2文献中讨论的验证技术总结INFmodCHKstaAnatescon遇到modSPEImptraindtraDEP[3、9]√√√√[4、61、33] √√√√[15、21、17][58、60、76][79，82]√√√√[1，22]√√√√[77个国家]√√√√√√[16、57、28][68、43、41][73，85，89]√√√√[63、84]√√√√[7、11、19、25][30、40、32]√√√√[第四十四届]√√√[42、65、78]√√√√√√[54、55]√√√√√[71，70]√√√√√[48，86]√√√[75个]√√√√[87，56]√√√√[12、8、52][62、74、√√√√D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）51981][23日]√√√√不变量在一些正式的语言，例如在一阶逻辑，然后使用证明助理[60，58，79，82]。此外，使用这种策略，可以在元模型级别执行验证，忘记模型并考虑转换并证明后配置。20D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5假设前提条件和变换规则都成立，如[17]所做的那样。对于我们正在运行的示例，可以证明的一个简单属性是Table中列的长度必须大于零。这个属性的成立是因为每个属性都被转换为一个列，并且每个类至少有一个属性。 这些信息分别在转换规则和源不变量中给出。这种方法的另一个步骤是[76]中提出的方法，其中在归纳构造演算[24]中给出模型，元模型和转换的表示，它们可以提取正确的转换。这需要将转换指定为表单的类型阿克斯： 第一卷（十） →（重复： Psl.O（x，y））其中Pil和Psl是源和目标元模型类型，I（x）指定了要应用的转换的源模型x的先决条件，O（x，y）指定了输出模型y所需的属性。这个表达式的证明允许自动构造函数f，使得给定任何x满足前提条件I（x），则后置条件O（x，fx）将被满足。最后，[61]中的一种补充方法提出了一种基于一阶逻辑的断言语言，描述了转换下模型的一些特征。然后，他们可以使用SWIProlog [88]作为推理系统来推导出在应用转换规则如果要验证的6.2模型关系变换模型提供了关于由变换连接的元素之间的关系的有用信息。有了这个，可以推断出一些其他的关系，这些关系仅仅通过观察单个元素是不明显的在我们的例子中我们可以用下面的属性来说明这一点：如果c是d的子类，c由于规则PersistentClass2Table使用了源元模型的特性，因此不能简单地推断出该属性。有很多方法可以证明这个性质。首先，我们可以使用形式语言来陈述它，并使用证明助手来证明它。我们也可以使用断言的语言，并证明这个属性可以从最终断言导出。我们在讨论一致性和模型类型时探讨了这些替代方案。另一种选择是定义一个转换契约，说明转换的前置条件和后置条件（或单个规则），并检查该契约是否成立。这个契约可以用OCL编写，然后使用OCL检查器或其他模型检查器进行验证，如[19，32]所示。它也可以使用专用工具编写，然后使用一些特定的算法进行验证，如[25，40]。D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5216.3功能行为我们的示例有一些“功能性”需求。如[16]中所定义的，可以检查某些属性是否在考虑特定规则或整个模型变换时成立。作为一个例子，规则PersistentClass2Table是可执行的，因为存在满足它的有效模型对（图3中的那些）。由于该规则是转换中的顶级规则，我们可以推导出整个转换也是可执行的。此外，这个规则不是单射的。考虑到转换将作为层次结构根的持久类映射到表，而派生类被继承，并且它们的属性映射到前一个表的列。然后，我们可以找到一个反例，它有相同的目标（一个有两列的表），其中一个是从一个有两个属性的类中产生的，另一个是从两个通过继承相互关联的类中产生的，每个类都有一个属性。遵循同样的思想，规则和转换都不是完全的（语法完整性），因为它们只适用于持久化类，而非持久化类永远不会被转换。在这种情况下，很明显，语法完整性是不可取的。这些属性可以通过将它们编码为转换模型上的UML/OCL一致性问题来验证，如[16]中所定义的。然后，可以使用OCL检查器。另一种替代方法是通过对跨导的静态分析来验证它们形成规则和底层元模型，如[75]。6.4决定论与终结论正如我们在上一节中已经说过的，这两个性质是最难证明的，因为它们与不可判定问题有关。实现它们的一个替代方案是使用某种语言，它通过构造来保证两者，如[8]中所介绍的然而，这个选项明显降低了表达能力。其他替代方案是用某种形式语言表示转换模型以执行逻辑推理，如[58]，或使用静态分析，如[55]。 然而，最常用的替代方法是将转换表示为 图重写问题，允许执行关键对分析，如[15，28，43，41，57，85]。6.5执行语义执行语义的保存是转换引擎开发期间的验证问题。然而，在定义模型转换时，必须解决一致性需求。作为一个例子，我们可能不想要冗余的规则，实际上我们的例子没有冗余。冗余规则的一个例子是将属性映射到列，但仅适用于持久化类。和以前一样，我们可以将这些需求编码为转换模型上的一致性问题，并使用模型检查器，如[3]，或使用静态分析，如[75]。此外，我们还可以像[60]那样使用逻辑推理22D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5另一种可能的方法是[89]，其中转换被表示为有色Petri网（CPN，[46]），它允许对CPN属性进行形式化的探索特别是，作者可以验证是否存在在执行过程中从未启用的转换，即所谓的Dead Transition Delay或L0-Liveness。只有两个属性没有在示例中考虑：类型和模型语义关系。正如我们之前所说的，类型化与连接和模型类型化密切相关。此外，由于我们使用的是结构模型，因此我们没有动态属性，而动态属性是语义属性的主要来源。我们也可以强制一些语义属性，但我们决定让读者参考[18]以获得更多示例。7结论和今后的工作我们对模型转换的验证进行了全面的文献综述，模型转换的结构遵循[2]中提出的三个维度我们扩展了以前的审查，并遵循基于问题的方法，举例说明可以在转换中验证的感兴趣的方面，并讨论如何验证它们由于空间原因，我们留下了一些细节，可以在[18]中找到。在这一点上，很明显，不仅对于变换的具体化，而且对于它的形式验证，都存在几种替代方案，这取决于在每个具体情况下必须解决的那些性质当考虑双向、高阶和多模型变换时，这个问题会在这个意义上，MDE构建的系统和传统软件系统之间存在一些并行性：需要异构的多逻辑规范，因为不同的系统具有不同的方面，这些方面在不同的语义域中得到最好的规范在上一节中介绍了一个这样的例子，其中一个小规模的例子介绍了不同的问题，每个问题最好通过几种策略来解决。为了应对这种情况，通常会提出软件开发人员之间的职责分离。一方面是MDE领域的专家，另一方面是正式验证领域的专家。这就产生了不同的技术逻辑空间[53]，即具有一组相关概念、知识体系、工具、所需技能和可能性的工作环境。一般来说，MDE专家定义模型和转换，而形式验证专家进行验证过程，通常由一些（半）自动生成过程辅助，该过程将MDE元素转换为专家用于验证目的的语义域中的形式表示与此相关，文献中提到的最常见的转换方法是关系和基于图的这里的要点是，这些方法与传统的编程语言（直接操纵，操作等）密切相关。引入了由传统代码验证方法执行的验证问题。此外，关系型和基于图的D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）523方法定义了最容易转换为形式域的元素，保留了它们的语义。摆在我们面前的景观使我们考虑一种异质的验证策略，与[20，69]中的思想密切相关。在这些著作中，作者定义了一种环境，在这种环境中，特定语言以它们的“自然”语义来描述此外，不同的语义域有不同的正式推理工具，而且由于语言之间有正式的这些思想都是基于制度理论[34]。在这个思想的基础上，我们可以以某种一致和相互依赖的方式将元模型和变换表示为所谓的制度，以及不同逻辑（也是制度）中的变换性质，以及它们的翻译（形式上，制度（共）态射）到几个逻辑中，目的是证明变换性质。模型既可以表示为机构，也可以表示为元模型机构中的例如，考虑到我们正在运行的示例，我们可以用XMI表示模型，用MOF表示元模型，用QVT表示转换。这些语言可以被定义为机构，并且可以从它们转换为不同的逻辑（也被指定为机构），例如一阶逻辑，重写逻辑，模态逻辑等。如果在OCL中指定了一致性需求，则可以将不同的元素转换为重写逻辑并执行[13]中定义的为了将这些想法付诸实践，我们可以使用异构工具集（Hets，[69]），它旨在支持异构多逻辑规范。Hets是一个解析，静态分析和证明管理工具，结合了各种针对特定语言的工具。如今，该工具支持许多逻辑（例如FOL，重写逻辑和模态逻辑）和工具（例如IsabelleHOL [72]和Maude [64]）。此外，它还提供了证据管理功能，用于监控异构规范的整体正确性，而其不同部分则使用可能不同的证据系统进行验证无论如何，值得指出的是，这个框架的实例化并不像看起来那么直接。首先，我们需要正式地说明制度理论中的每一个MDE构建块，其次，我们需要对这些逻辑进行任何可能的和有用的翻译在这个理论中，这些表象可能既不直接，也不此外，Hets中的任何新逻辑都可以在其自身的语义域中支持形式验证。然而，这需要定义一个隔音系统。在某些没有这种证明系统的情况下，其定义可能非常昂贵。例如，在[61]中，作者介绍了一种用于断言的语言和一个半自动推理系统，它没有被正式指定为一个可靠的证明系统。24D. Calegari，N.Szasz/Electronic Notes in Theoretical Computer Science 292（2013）5引用[1] Akehurst ， D. ， S. Kent 和 O. Patrascoiu ， A relational approach to defining and implementingtransformations between metamodels，Software Systems Modeling2（2003），pp. 215-239[2] Amrani，M.，L. Lucio，G.塞利姆湾Combemale，J. Dingel，H. Vangheluwe，Y. L. Traon和J. Cordy，研究模型转换的形式验证的三维方法，在：模型转换的验证和验证（VOLT）（2012）。[3] Anastasakis，K.，B. Bordbar，G.乔治和我。Ray，On Challenges of Model Transformation from UMLto Alloy，Software Systems Modeling9（2010），pp.69比86[4] Asztalos ， M. ， L. Lengyel 和 T. Levendovszky ， Towards Automated ， Formal Verification of Mod