基于模型驱动的质量感知应用程序开发及设计验证的系统方法和工具环境介绍

理论计算机科学电子笔记133（2005）101-117www.elsevier.com/locate/entcs通过模型驱动验证Anders Henriksson，Uwe Aßman安德斯·亨里克森1，2瑞典林雪平大学詹姆斯·亨特3德国卡尔斯鲁厄信息研究中心摘要基于对象管理组织OMG的模型驱动架构（MDA），提出了一种新的质量感知应用程序开发方案--质量驱动开发（QDD）我们认为，软件开发的领域，如实时系统，不应该只依赖于代码验证，但也对设计验证，并表明，一个稍微扩展的MDA过程的机会，集成系统开发与设计验证。作为该方法的一个实例，我们介绍了HIDOORS项目的基于MDA的工具环境[10]。在这个环境中，实时模型检查器被解释为MDA意义上的平台。UML设计可以用验证标记进行注释，这些标记不仅可以编译成代码，还可以编译成验证平台（模型检查器）的设计验证模型。通过这种方式，实时设计的模型检查被集成到模型驱动的开发过程中，并允许早期验证。该方法可以很容易地转移到其他验证技术。我们给出一个初步的对可能的验证平台进行分类，并分析其相互作用。分析表明，对于质量感知的应用领域，标准的MDA方法应该扩展一个或多个MDA堆栈模型驱动验证（MDV）。由此产生的方法，质量驱动开发（QDD），据我们所知，是第一个在模型驱动开发中集成代码生成和验证的系统方法关键词：模型驱动架构，模型驱动验证1 电子邮件地址：andhe@ida.liu.se2 电子邮件地址：uweas@ida.liu.se3电子邮件：jjh@fzi.de1571-0661 © 2005由ElsevierB. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.08.060102A. Henriksson等人理论计算机科学电子笔记133（2005）1011介绍如果在质量感知的应用领域，如实时场景，软件应该开发，需要适当的静态验证机制。信任一个系统需要认证，而认证需要证明软件的功能和质量特征（符合特定功能、资源限制、时间约束、软件的活跃性或公平性等）。因此，对于质量感知领域，功能性和非功能性需求都起着重要作用，并施加强大的压力来证明最终产品符合其规范。MDA是一种新颖的、有前途的多平台开发架构和过程[12]。它有很多优点。例如，它承诺在许多平台上重用设计模型。使用参数化和其他映射技术，将设计规范（平台无关模型，PIM）转换为平台特定的实现模型（PSM）。MDA还解决了设计老化问题。在开发过程中，代码和规范之间的关系往往会在一段时间后丢失，因为当实现发展时，规范不再更新。由于MDA维护了设计和实现级别之间的映射，因此可以在设计中更好地跟踪实现更改，并且可以更容易地更新设计。不幸的是，对于验证感知的应用领域，特别是嵌入式和实时软件，很少有人注意将所需的验证技术集成到MDA中。由于在这些领域中，验证必须在代码级别上进行，因此导致了两个MDA能够解决但尚未解决的问题。首先，设计往往根本没有得到验证。 因为无论如何系统必须在代码级别上进行认证，因此将代码与设计验证相关联的额外费用并不具有吸引力。当然，这会导致设计老化。其次，即使设计的验证已经完成，它也会很快老化。设计模型可以被生成和检查，但由于证明必须在代码级重复，设计验证在过渡到代码后就被丢弃了。换句话说，在质量感知软件领域，问题在于设计验证没有与设计、代码或代码验证集成在一起这表明，MDA虽然针对质量感知的应用领域，如实时和嵌入式系统，但尚未提供必要的集成验证技术。本文试图填补这一空白，并提出了一个扩展的MDA模型驱动验证（MDV）。对于MDA+MDV的集成方法，我们使用质量驱动开发（QDD）的概念。A. Henriksson等人理论计算机科学电子笔记133（2005）101103本文总结了HIDOORS项目[10]的观察结果，其中除了通常的代码生成 和 代 码 验 证 之 外 ， 还 设 想 了 实 时 UML 模 型 的 设 计 验 证 。 在HIDOORS中，实时UML设计是用实时模型检查器来验证的（第二节）。3）。为了验证和代码生成的集成开发，我们开发了一个实时UML profile [5]，它完善了OMG的SPT profile [11]。该配置文件用于代码生成，以及使用实时模型检查器进行设计验证。在这个框架中，我们发现MDA应该扩展到支持设计验证。引入第二种是有利的，用于验证的平台堆栈，与传统的MDA堆栈并行（Sec.3）。这导致了设计和代码验证的新验证平台的定义，以及这些平台最终验证模型的平台堆栈（第二节）。4）.我们表明，在HIDOORS中，使 用 了 两 个 验 证 平 台 ： 模 型 检 查 器 和 最 坏 情 况 执 行 时 间 分 析（WCETA），它分析生成的Java系统。我们概述了传统MDA堆栈与模型检查器和WCETA的验证堆栈之间的相互作用（第二节）。4.2）。因此，本文的基本观察是，质量感知软件的MDA需要通过模型驱动验证（MDV）扩展到质量驱动开发（QDD）。据我们所知，QDD是质量感知应用领域中MDA的第一种方法。QDD具有更多的优势。由于与MDA的紧密集成，MDV支持早期验证。HIDOORSMDV支持在开发过程的早期，甚至在单元测试之前，对实时设计进行模型检查。如果模型检查器验证了设计，代码就有更好的机会是正确的，这意味着代码验证变得更简单。其次，由于模型驱动开发的好处，所使用的验证平台可以很容易地与其他平台交换。在HIDOORS框架中，所使用的模型检查器可以与另一个模型检查器交换。最后，MDA和MDV栈有很多交叉融合。由于设计验证有助于代码验证，而代码验证又支持设计验证，因此保留和维护设计是值得的。由于设计不仅用于代码生成，还用于设计验证，因此鼓励开发人员始终保持设计和代码一致。因此，QDD减少了设计老化的影响。在下文中，如果设计模型是根据其需求模型进行验证的，我们将讨论设计验证。特别是，这包括时序要求已被证明适用于设计的情况。相反，如果实现模型根据其需求进行了验证，则我们称之为代码验证104A. Henriksson等人理论计算机科学电子笔记133（2005）101牙买加WCETAUPPAALUPPAALJava字节码模型实现模型Java代码（PSM）定时自动机模型（PSM）平台无关（UML）模型（PIM）计算独立模型（CIM）MDA/MDV堆栈目标图1.HIDOOORS模型栈：MDA和MDV。模型(This这意味着我们用代码识别特定于平台的实现模型。）我们将构造型和标记值总结为标记标记，因为它们标记UML设计，即，断言非标准的特定于域的信息。通常，模型栈是不同抽象级别上的分层模型集。2质量驱动的HIDOOORS在HIDOORS中，MDA堆栈用于为选定的目标平台生成目标实现。MDV本质上是对现有MDA堆栈的补充，支持为代码分析和模型验证添加额外目标的验证任务。MDA堆栈与MDV添加一起形成了HIDOORS可靠性驱动开发的QDD堆栈，如图1所示。2.1用于模型验证用于模型验证的HIDOORSMDV堆栈用于验证系统的UML模型中表达的约束与最终目标总是实现的MDA相反，用于模型验证的MDV堆栈的最终目标是作为模型检查器输入的验证模型MDA堆栈中的两个第一级对于MDA和验证是相同的 其中MDA的平台特定模型包括在Java代码中，MDV的平台特定模型是一个时间自动机[2，1]。MDV模型堆栈的最后一级是模型检查器的输入模型模型验证工作在系统的抽象模型上。在这个级别上，并不是所有关于目标实现的细节都是可用的运行时平台。为了使模型验证可行，必须做出一些假设。在模型验证期间，假设时间预算A. Henriksson等人理论计算机科学电子笔记133（2005）101105在UML模型中使用注释形式给出的HIDOOORS配置文件等于预算代码的最坏情况执行时间，并且这些预算保持不变。模型验证验证模型约束，且仅在假设成立的情况下验证才有效。WCETA使用与MDA相同的堆栈，但用于不同的目的。与用于模型验证的MDV堆栈类似，用于代码分析的MDV堆栈旨在用于验证。在这种情况下，目标是最坏情况执行时间分析（WCETA）引擎。WCETA和模型验证工作在不同抽象级别的模型上。虽然模型验证验证了模型中的约束，但它对最终实现和运行时平台做出了假设。WCETA分析将验证这些假设是否适用于所选运行时平台上的最终实现。3HIDOOORS模型驱动验证过程HIDOOORS中的模型驱动验证（MDV）包括两个主要步骤。第一步是根据模型验证模型约束，第二步是根据实现验证模型约束。这两个步骤与HIDOORSMDA一起构成了HIDOORSMDV流程，如图2所示。在HIDOORS开发环境中，用户从需求工程开始，指定系统的功能和约束。在需求工程之后，用户使用HIDOORSprofile [5]在UML中指定系统设计的系统建模当系统被建模时，模型约束在模型验证步骤中被验证。模型验证假设建模的时间预算将保持不变，并假设时间预算等于最坏情况下的执行时间，然后根据这些假设验证模型中的时间限制。接下来是一个决定，如果模型验证步骤验证了模型化的约束将保持不变，则该过程可以继续，否则必须采取一些措施来纠正模型。当模型验证步骤失败时，这意味着至少有一个模型化的约束在任何平台上的已实现系统中都不成立，给定模型化的时间预算，不可能实现被打破的约束。下一个问题是系统是否可以被改造以更好地满足约束。在这些情况下，当系统不能被改造，以满足必要的模型约束，下一个问题是，如果系统的要求可以放宽，使系统可行。如果这是不可能的，所需的系统是不可行的，106A. Henriksson等人理论计算机科学电子笔记133（2005）101图2.HIDOORS模型验证过程。无法建造。当系统模型已通过模型验证步骤时，模型代表可行系统。接下来要做的是为系统选择一个目标平台。给出了目标平台和系统模型，实现了系统。接下来是MDV过程中的第二个主要步骤，验证模型的实现。模型验证对所实施的系统进行了某些假设。现在到了实现验证步骤，以验证模型的实现方式是否符合这些假设。当实现验证失败时，这意味着实现打破了模型验证所做的一个或多个假设。这意味着在某些情况下，所实现的系统将不会完全填充建模的约束。A. Henriksson等人理论计算机科学电子笔记133（2005）101107控制器火车栅极铁路路传感器图3. 以火车为例。如果实现验证失败，第一个问题是模型是否可以重新实现或重构，以保持验证。如果系统不能被重新实现，那么下一个问题就是系统是否可以被重定向到另一个拥有更多资源的平台。当没有平台存在时，系统可以实现，那么模型就不能实现。在这种情况下，需要重新建模。最后，当找到一个可以在可用目标平台上验证的实现时，系统已经实现，它将满足给定平台上的模型约束。3.1例为了说明MDV过程，将使用traincrossing示例作为运行示例。图3显示了列车穿越场景的概述。在这个例子中的主要目标是设计控制器，打开和关闭门在列车通过时，在列车交叉口。在该示例中涉及四个对象，当列车接近时检测列车的传感器、应当关闭的门、检测列车已经离开列车道口的传感器以及根据来自传感器的信号起作用并操纵门的控制器。从实时的角度来看，控制器的响应时间受到限制。 响应时间必须是列车到达闸门时闸门关闭。 这个想法是 当列车通过闸门时，列车具有最大允许速度，该速度与传感器和闸门之间的固定距离一起产生关闭闸门的时间预算。该系统是在UML建模使用类图，消息序列图和状态车。图4显示了列车闸机系统的UML模型。UML模型用构造型和来自HIDOORSprofile [5].HIDOORS的刻板印象和标签价值观108A. Henriksson等人理论计算机科学电子笔记133（2005）101图4.用UML建模的火车穿越示例profile表示模型的UML元素之间的关系和约束，例如时间约束和缓冲器大小。3.2模型约束模型验证步骤的目的是验证假设模型正确，建模的约束条件是否成立。UML模型是平台无关的，也就是说，没有关于目标平台上可用资源的信息。为了能够在这个抽象层次上执行任何有用的验证任务，必须对更详细的抽象层次做出一些假设。假设与方法相关的时间预算等于目标平台上实现的方法的最坏情况执行时间模型中的时间约束用消息序列图和状态图中的相对截止期表示。缓冲器约束被表示为与接收器相关联的缓冲器大小。使用符号模型检查器检查约束。模型验证通过模型进行-A. Henriksson等人理论计算机科学电子笔记133（2005）101109图5. HIDOORS模型检查工具链。检查图5所示的工具链。模型检测工具链包括四个主要步骤：类图到状态图转换器Transformer，消息序列图到状态图合并，时间自动机生成和最后的模型检测。模型检查工具链的第一步是类图（CD）到状态图（SC）的转换。CD至SC Transformer是一个“降低引擎”。该Transformer分析类图中表示通信模式的类之间的约束，并以状态图的形式实例化实现该通信模式所需的对象。接下来是消息序列图（MSC）到SC的合并。使用HIDOORS配置文件，用户可以在MSC和SC中表达时序约束。MSC到SC将MSC中表达的定时约束合并到对应的SC中。然后，状态图被用作用于生成适合于模型检查的SC的时间自动机[2，1模型检查工具链的最后一步是模型检查本身。在HIDOORS项目中，UPPAAL [3，8]模型检查器用于验证时序约束和缓冲器大小。模型检查器本质上110A. Henriksson等人理论计算机科学电子笔记133（2005）101检查时间自动机中某个状态的可达性。因此，表示系统模型的时间自动机是以这样的方式构造的，即每当一个约束被打破时，相应的时间自动机就进入错误状态。模型约束的检查可以通过检查时间自动机中错误状态的可达性来执行。当一个模型检查器发现一个不可到达的状态时，它只是返回声明这个事实。另一方面，如果模型检查器发现一个状态是可到达的，它将返回一个“跟踪”，显示如何到达状态。只要发现错误状态是可达到的，就可以通过分析模型检查器产生的“跟踪”来找到被打破的约束，以确定3.3模型的可扩展实现验证系统时序的正确性当分析发生在实现层面时，整体的时间安排和调度应该已经通过模型检查进行了验证。需要做的是证明实现与模型是一致的。HIDOOORS项目使用最差情况执行时间分析（WCETA）作为此确认的基础当从模型转移到实现时，将纯设计信息与实现的细节清楚地分开是很重要的。理论上，模型中的定时信息应仅取决于控制硬件和软件外部的因素。在实践中，时间预算通常需要考虑可能竞争硬件资源的不同任务的相对计算难度。尽管如此，人们应该能够在不改变模型或使其模型级验证结果无效的情况下改变用于实现的硬件。然后，WCETA的作用被降级为证明特定的实现遵守以下时间：在模型中给出的。由于MDA的目标是从模型中自动生成代码，因此必须注意模型中时间约束的解释和应用。MDA代码生成过程可以引入具有系统相关实现的新子类（在下文中称为助手类）。新帮助器类中的方法必须满足与原始类中相同的计时约束。这与正确的子类型化的一般约束相似。一个子类必须是可用的，只要它的超类可以被使用。在函数域中，这意味着子类中的每个方法都具有等于或弱于超类中等效方法的前置条件，以及等于或强于A. Henriksson等人理论计算机科学电子笔记133（2005）101111重写方法。以此类推，所有的资源约束都是后置条件。换句话说，一个合适的子类必须满足它从父类重写的每个方法上的一旦确立了这一原则，验证实现的时间由于整个时序关系已经通过模型检查进行了验证，WCETA可以集中验证单个方法调用的时序。这些方法调用只需要填充模型中给定的时间约束从模型到实现涉及几个步骤。UML模型必须首先转换为代码。在HIDOORS中，这意味着Java代码。然后将Java代码编译为字节码。Java的平台独立性意味着这一步也可以是独立于实现的。当Java字节码被编译成机器码时，平台依赖性将在下一步中引入。WCETA然后被用来分析这一机器代码结合处理器和高速缓存与各自的时钟频率和内存总线频率的详细说明。通过使用Java虚拟机的解释器，可以消除字节码到机器码的转换。尽管代码将保持平台独立性，但其执行却不独立.事实上，时序分析会更加困难，因为字节码需要和解释器一起分析分析即时编译是非常困难的。因此，HIDOORS工具旨在将所有字节代码编译为时间关键任务中的机器代码。将字节码编译成机器码和为子类使用适当的子类型关系的组合意味着可以使用WCETA的标准技术。关键是将时间约束从UML模型传递到最终的本机代码。结果不是模型的一部分，而是构成特定实现的验证证据。更改目标平台将需要重新运行WCETA，但模型检查结果仍然适用。4QDD中的验证和验证平台在查看了HIDOOORS的示例之后，本节将研究QDD中验证和运行时平台的关系。我们观察到，验证的目标在验证模型之间引入了强耦合，并提高了开发人员保持所有规范一致的动力，在软件演化过程中也是如此。112A. Henriksson等人理论计算机科学电子笔记133（2005）101图6. QDD中的验证和运行时平台在下文中，原型和标记值被称为标记标记，因为它们标记UML设计，即，断言非标准的域特定信息。4.1平台类型标准MDA构建在运行时平台上。由于MDA是一个过程，它重用设计规范，模型，用于多个平台，它的重点是重用。 因此，MDA不关心设计的正确性，这对于质量感知应用程序来说是一个主要的缺点。然而，MDV采用模型驱动开发来验证平台上的模型。它的重点不是重用，而是设计模型和代码的验证。MDV旨在通过将设计转换为可以检查、验证或证明的形式平台分为以下几组，形成了QDD的平台（见图1）。6）：多个平台。这些是MDA的标准平台，如组件模型、机器、操作系统等。验证平台。这些平台可以象征性地或在测试环境中执行设计或模型。代码验证平台。这样的平台是用于测试代码正确性的测试环境。测试平台。测试平台在体外测试环境中执行代码。这些可以是单元测试平台，回归测试平台，如JUnit等。试验台 测试平台在运行时A. Henriksson等人理论计算机科学电子笔记133（2005）101113平台，但引入额外的运行时检查，例如，动态类型测试、异常测试等。设计验证平台。验证平台提供了一种形式化的语言，系统的特性可以通过这种语言进行静态验证。设计验证平台验证设计模型（设计验证）。设计模型比代码更抽象。例如Petri网模型、CSP模型或实时状态图模型。代码验证平台。分析平台。这些平台与抽象解释有关[6]，即，代码的符号执行，以证明系统的功能WCETA对HIDOORS的分析（第3.3）就是一个例子。功能验证平台。 在这些平台中，代码在功能和非功能需求方面得到充分验证。在质量感知软件的开发中，所有这些验证和验证平台都发挥着重要作用，因为系统的功能应该在系统运行之前得到验证或检查。因此，安全关键领域的系统开发需要代码和验证之间的紧密相互作用。对于这些应用程序来说，单独的MDA（只考虑架构）是不够的。这种情况下的典型情况是，验证平台可能比另一个平台更抽象或更高级。这意味着系统模型以比代码更抽象的形式表示。例如，模型检查验证模型假设代码的某些特性，这些特性必须在以后由其他验证平台（例如WCETA）证明或测试。因此，模型检测平台更抽象，看到的系统细节更少。另一方面，在更抽象的验证中，证明抽象系统的特征模型检查之所以有效，是因为它假设交互对应于常规语言（通常是一种抽象）。这就是QDD吸引人的原因：为了证明系统特性，需要一组抽象的验证平台，这些平台相互关联，并允许对系统质量做出结论。4.2QDD中MDA和MDV的相互作用本节研究验证平台和运行时平台之间的关系。对于验证平台的验证和测试，必须将信息添加到PIM中。这可以通过添加标记规范来完成。在下文中，我们以HI- DOORSQDD为例，研究不同类型的验证标记如何相互作用114A. Henriksson等人理论计算机科学电子笔记133（2005）101图7.翻译一个与PIM相关的刻板印象HIBU翻译。左：转换为Java类模型（PSM），右：转换为状态图与MDA的标记。例4.1对于相互作用分析，让我们从HIDOORS分布图中给出一个例子（图7）。该配置文件包含一个关联原型HIBu Bubcher，它可以被注释为二进制关联，表明两个事件类通过FIFO Bubcher与生产者/消费者协议进行通信。构造型可以用一个标记值大小来丰富，该标记值大小指定了构造型的大小。一旦被注释到PIM的关联中，构造型就可以被转换成标准的PSM。在这种情况下，代码生成会插入一个缓冲器助手类，用于维护长度大小的缓冲器。HIDOORS使用Java，所以buffer是一个Java类。另一方面，构造型意味着一个协议，FIFO协议，它可以被转换成一组状态图，表示所有涉及的类。4状态图可以转换为一组时间自动机，并输入模型检查器验证平台。假设需求发生了变化，减少了运行时平台的可用内存。然后，应当改变PIM，使得缓冲器的尺寸减小。在QDD中，不仅可以很容易地重新生成代码，而且可以使用模型检查器平台来验证更改后的设计。记住这个例子，我们可以观察到，与验证相关的标记至少有三个目的：代码生成，断言假设，以促进在更高级别的验证平台上的证明，以及为较低级别的验证平台设计知识断言首先，markup服务于4这项翻译工作正在进行中。A. Henriksson等人理论计算机科学电子笔记133（2005）101115用于在标准MDA堆栈中生成代码（这是众所周知的）。然后，标记可以验证用于验证模型的知识。首先，标记可以断言关于较低级别的验证模型的假设，最后是代码。这些约束较低级别的模型，为它们生成证明义务。断言假设是抽象的结果。由于较低级别的验证平台或运行时平台的一些细节本质上，断言假设定义了在更高级别模型中证明的引理，这些引理在更低级别模型中得到证明因此，断言提供了高级模型中的证明和低级模型中的证明之间的接口从本质上讲，断言假设弥合了更高级别验证模型的证明中的证明差距，因为标记为较低级别的验证平台生成了证明义务。最后，QDD中存在一种对偶效应。在PIM中，可以指定关于设计知识的断言，编码设计知识，以帮助在以后的阶段进行验证。通常，设计师对系统的了解比代码分析或代码验证所能证明的要多。一般来说，完全验证对于一个系统来说可能是相当困难的，但是，它可以通过额外的设计知识断言来帮助。然后，代码验证提供与设计级别上的断言相关 我们称之为设计支持的代码验证。在功能需求验证中也发现了设计支持的验证。它的优点是，在完全验证过于困难的情况下，它可以实现相对验证[4，9]。4.3QDD如何应对设计老化我们已经证明，验证模型通过两种现象相互关联，即断言假设为较低级别的模型生成证明义务，以及为较低级别平台上的证明设计知识断言这有几个后果。首先，每个抽象层次上的证明支持其他抽象层次上的证明特别是，设计知识断言支持代码验证。设计验证可以在模型上完成，断言假设可以简化它们。因此，可以在早期检查应用程序的错误，并且大大提高了开发人员对系统的信任，甚至在执行代码验证之前。由于设计模型的验证可用于证明系统的功能，因此在代码验证后不要将其丢弃，而是在系统发生更改时使用它来重新验证系统因此，我们认为，116A. Henriksson等人理论计算机科学电子笔记133（2005）101验证模型之间的这两种关系在软件维护中产生了一种强烈的趋势，即保持PIM设计模型、验证模型和PSM的一致性。因此，QDD吸引了开发人员来培养他们的设计模型。5相关工作关于一个系统的证明可以在通过引理或映射耦合的不同抽象层次上完成的想法是抽象解释的中心思想[7]。然而，在这种情况下，抽象的解释是手工创建的，而不是从设计模型派生的。QDD在这里取得了进步，因为它将几个抽象级别的验证思想嵌入到模型驱动的开发中，其中设计和目标模型的区别起着重要的作用。通过将抽象解释识别为特定平台，MDA和抽象解释可以统一。当然，本文只是朝着这个方向迈出了第一步，还需要做更多的工作Heyer他开发了一种技术，通过用户断言来弥合Dijkstra最弱前提演算中的证明缺口。如果一个事实不能被证明系统自动证明，但很明显，用户可以断言它，整个证明可以继续。从本质上讲，这种方法似乎比系统的全自动验证更深入。尽管很少有实验使用这种技术进行，但它似乎在模型驱动的验证中变得更加重要。6结论我们已经表明，质量感知软件的MDA需要通过模型驱动验证（MDV）扩展到质量驱动开发（QDD）。据我们所知，QDD是质量感知应用领域中MDA的第一种方法通过在模型驱动开发中进行集成设计验证，我们能够及早发现实时PIM的错误。传统的方法，测试或代码验证，发现错误很晚。由于发现错误的时间越晚，纠正错误的成本就越高，因此QDD应该为提高开发人员的生产力提供领先优势。其次，如果在几个不同的抽象层次上并行进行，验证应该会变得更容易。开发人员应该能够检测到使用传统测试很难发现的错误。一方面，PIM中的断言假设有助于设计验证，并且可以在代码验证稍后进行。另一方面，设计知识主张-A. Henriksson等人理论计算机科学电子笔记133（2005）101117当代码验证不可能时，它们简化了代码验证，或者使之成为可能。此外，验证模型和代码（PSM）之间的这些强大关系创造了保持设计和实现一致的激励，从而解决设计老化问题。最后，QDD为质量感知的应用领域提供了MDA的一个优雅的扩展。当将验证工具视为平台时，验证引擎变得与运行时平台非常相似。这使得QDD能够将验证技术和面向平台的开发统一到一个统一的模型驱动框架中。引用[1] Rajeev先生时间自动机计算机辅助验证，第8-22页，1999年[2] 作者声明：David L.迪尔时间自动机理论。Theoretical Computer Science，126（2）：183[3] Johan Bengtsson，Kim Guldstrand Larsen，Fredrik Larsson，Paul Pettersson和Wang Yi。1995年的UPPAAL。系统构造和分析的工具和算法，第431-434页[4] S. Bonnier和T.海尔COMPASS：一种可理解的断言方法。计算机科学讲义，1214：803-？？，一九九七年。[5] HIDOORS财团。hidoors uml profile for high-integrity distributed object-oriented real timesystems. http://www.hidoors.org。[6] P. Cousot和R.库索比较伽罗瓦连接和扩大/缩小抽象解释的方法。In M. Bruynooghe和M.Wirsing，编辑，Programming Language Implementation and Logic Programming，卷631计算机科学讲义。Springer，1992年。[7] 帕特里克·库索和拉迪亚·库索抽象的解释框架。Journal of Logic and Computation，2（4）：511[8] Alexandre David，M.奥利弗·穆勒和王毅。 UML状态图的形式化验证实时扩展。软件工程的基本方法，第218- 232页[9] 蒂姆·海尔。软件工件的语义检测从理论到实践。林雪平大学博士论文，2001年。[10] 卡尔斯鲁厄詹姆斯·亨特。信息研究中心高完整性分布式面向对象实时系统。http://www.hidoors.org。[11] 对 象 管 理 组 （ OMG ） 。 UML Profile for Complexability ， Performance ， and TimeSpecification，2002。 http：www.omg.org/uml.[12] 对象管理组（OMG）。MDA指南，2003年。 http：www.omg.org/mda.