嵌入式系统质量评价新方法：异构、模块化和可配置系统的质量平台

--理论计算机科学电子笔记116（2005）113-131www.elsevier.com/locate/entcsQUACK：新一代集成嵌入式系统的质量平台1MauroP ezz`e2AndreaBaldini3GiovanniDenaro2朱塞佩·利帕里4马特奥·罗西5达维德·罗盖6摘要在过去的两年里，QUACK项目研究了一种评估异构、模块化和可配置嵌入式系统质量的新方法，即，由许多硬件和软件组件组成的系统，通常嵌入在具有实时要求的设备中，并以不同版本和配置的系列生产。 该项目的主要目的是克服传统技术在处理所涉系统类别所引起的许多新方面和新问题方面的局限性。本文综述了QUACK项目的最后结果：即一种新的质量评估方法异构、模块化和可配置的嵌入式系统，贯穿整个软件过程。保留字：嵌入式系统，质量评价，异构性，模块化1这项工作得到了意大利大学和研究部在COFIN 2001项目2 个 G.Denaro 和 M.Pez z`earewithUni versi t`adegliStudidiMilanoBic o cca ， viaBicoccadegli Arcimboldi 8 ， I-20126 ， Milano ， Italy. 电 子 邮 件 ： denaro ，pezze@www.example.comdisco.unimib.it3A. 巴尔迪尼是都灵理工大学，Corso Duca degli Abruzzi 24，I-10129，都灵，意大利 电子邮件地址：baldini@polito.it4个G. 利帕里是与ScuolaSu perioreS。Anna，PizzaMartiridellaLiberta'33，I-56127，Pisa，意大利 电子邮件地址：lipari@sssup.it5百万。Rossi is with Politecnico di Milano，Via Ponzio 34/5，I-20133，Milano，Italy.电邮地址：rossi@elet.polimi.it6个D. RogaiiswithUniversit`adegliStudidiFirenze，ViadiSantaMarta3，I-50139，Firenze，意大利电子邮件地址：rogai@dsi.unifi.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.082114M. Pezzè等人理论计算机科学电子笔记116（2005）1131介绍异构、模块化和可配置的嵌入式系统由多个异构组件组成，这些组件共享硬件和软件资源。这类系统通常有几个版本和配置，这些版本和配置是通过适当组合不同的组件子集获得的。即使在同一个系统中，这些组件也可以通过不同的实时和安全要求来表征。这类系统目前应用于几个应用领域，包括但不限于汽车、铁路、太空、国防、可穿戴计算和家庭。新一代汽车的车载系统很好地适应了这类系统。它们结合了几种硬件设备，例如，DVD、GSM和GPS设备，并提供许多复杂的软件服务，例如，互联网设施，汽车报警监控和所有可用设备的综合控制。组件在不同的临界水平下具有安全性和实时性要求：例如，汽车报警监控系统的故障可能会产生严重后果，而互联网设施的故障不会产生重大损害。不同的汽车型号使用不同的可用组件配置，例如，基本型号可能不包括GPS和互联网设施，而顶级型号可能包括所有设施。通过改变、添加或更新组件的子集来获得配置这些系统的关键特性要求高质量，传统的测试和分析技术无法轻易满足这些要求，因为传统的测试和分析技术无法掌握这些系统的复杂性，也无法有效地处理同一系统的许多变体。对这些系统的许多配置和版本进行独立验证通常是不切实际的。随着越来越多的配置和具有高质量要求的系统版本的开发，需要新的技术，这些技术允许重用关于组件质量及其在不同配置之间的相似性的知识，从而减少对每个系统的检查QUACK项目在过去两年中研究了一种新的方法控制异构、模块化和可配置嵌入式系统的质量。建议的方法（我们称之为QUACK方法后，该项目的首字母缩写）合并不同的技术，用于不同的开发阶段或不同类型的需求。QUACK方法包括检查初始需求和导出系统测试的形式化方法;运行时监控技术，用于自动捕获不同配置中组件的行为，并在不同配置之间比较这些行为M. Pezzè等人理论计算机科学电子笔记116（2005）113115分析和模型检查，以验证具有实时和容错要求的系统的属性;嵌入式组件的测试用例生成和测试用例在测试环境中的自动部署本文报道了QUACK项目的结果。第2节概述了QUACK方法，指出了建议的技术以及解决的阶段和要求。第三节提出了系统需求的形式化方法第4节介绍了为组件和基于组件的软件系统生成质量义务和测试用例的技术。第5节介绍了为验证实时和容错要求而提出的方法第6节介绍了从UML设计文档中自动导出测试用例的技术。最后，第7节总结了项目的结果，并概述了正在进行的研究工作。2异构、模块化和可配置嵌入式系统质量的综合方法图1说明了QUACK方法的主要元素，并指出了本文中介绍相应方法的部分。该图确定了在异构、模块化和可配置嵌入式系统开发的三个主要阶段对质量评估的支持需求。规格：系统的新版本或配置的开发独立于系统内部架构识别预期行为的文档。在当前的实践中，系统规范通常用自然语言表达设计：系统规格根据对现有版本和配置（系统系列）的检查，并确定要重复使用、调整、添加或替换的组件，将现有配置转换为新配置，从而映射到合适的架构上模块化设计通常用图形化的视觉语言来表达，例如，合适的UML子集部署：最终组件，无论是新的还是重用的，都集成到软件架构中以产生新系统。合适的中间件技术，例如，Java 2企业版平台[46]，可以方便部署。116M. Pezzè等人理论计算机科学电子笔记116（2005）113Fig. 1. QUACK方法QUACK方法包括四套方法，用于支持每个阶段的系统质量评估，从而旨在预测尽可能多的故障识别和排除。每组方法都利用了特定阶段可用的不同信息。根据QUACK方法：(i) 系统规范通过时序逻辑形式化。执行正式规范以识别指定需求的不一致性和不完整性，并用于自动生成系统测试的测试套件M. Pezzè等人理论计算机科学电子笔记116（2005）113117(ii) 运行时监视器收集有关不同组件的功能行为以及现有配置和版本中的动态交互模式的数据。收集的数据用于生成支持识别新版本和配置的潜在错误行为的不变量。集成测试套件是基于不变量生成的。(iii) 可扩展性分析和模型检查用于验证实时性和容错性，以解决系统的基于组件的性质(iv) UML设计图的自动分析，支持自动生成测试套件，用于最终系统及其组件的最终生产测试。所提出的技术是高度自动化的，因此有助于提高最终系统的质量，对整体成本的影响很小的发展过程。不同方法的集成非常简单：尽管集成方法可以获得最佳结果，但每种方法都可以独立用于验证不需要所有分析步骤的系统。3实时嵌入式系统的形式化描述初始（非正式）规范被转换为时序逻辑规范，用于早期分析，包括：• 通过模型检查对系统进行基于一致性的验证。• 通过定理证明对模块化系统进行演绎验证。• 通过状态和事件对实时系统进行规范。• 通过直接执行其行为规范的实时系统的代码派生。本节描述了如何在QUACK方法中实现上述方法。由于QUACK方法所涵盖的问题范围很广，因此已经开发和研究了不同的互补形式主义。探索的方法基于三种时间逻辑：OTL [24]，与UML兼容;TRIO [20]，适用于离散和连续实时系统的规范和验证（通过模型检查和定理证明）; TILCO [31]，可以产生表达，118M. Pezzè等人理论计算机科学电子笔记116（2005）113直接可执行和可验证的规范，从中可以自动生成代码。尽管UML在工业界被广泛接受，但它仍然缺乏有效地处理时间约束的强大建模机制。Lavazza，Morasca和Morzenti提出了一种对UML对象约束语言（OCL）的扩展[36]，称为对象时态逻辑（OTL）[24]来处理时间方面。OTL只是简单地向OCL 2.0标准库添加了两个类，Time和Offset。类时间模型的时刻，而类偏移模型的距离之间的两个时刻。时刻是指当前时间，它扮演着时间原点的角色类Time和Offset 允许定义时态逻辑的典型时态运算符（即Always ，Sometimes，Until等），从而对定时方面进行建模。OTL允许用户以定量的方式对时间进行推理，因此可以表达事件B必须在事件A之后最多l个时间单位发生的属性。时间和偏移量可以是离散的，也可以是密集的，这取决于建模的应用程序，从而使用户具有很大的灵活性和表达能力。OTL公式相对于当前时刻进行计算，该时刻是隐式的。类Time的原语eval在OCL中用于计算与当前时刻不同的时刻的谓词。例如，给定一个Time类的对象t和一个谓词p（它是一个OclExpression），如果p在时刻t保持不变，则t.eval（p）返回true（一个布尔值）。关于OTL在QUACK方法中的使用的进一步细节可以在Lavazza等人的论文中[25]第10段。虽然OTL是一种非常有前途的方法来建模面向对象应用程序的行为，但它还很年轻;此外，目前还缺乏一套用于验证OTL特定系统的工具。另一种更成熟的基于逻辑的实时系统建模方法是TRIO时序逻辑[20，35]。为了支持QUACK方法，开发了TRIO规范的模块化实时系统庸医方法通过模型检查和定理证明支持应用程序的验证。虽然许多当前的模型检查器（最值得注意的是流行的SPIN [21]）使用线性时态逻辑（LTL，[41]），它只具有未来时态运算符，来表达过渡系统的属性，但TRIO [20]可以表达未来和过去关于当前时刻的属性（这在TRIO公式中是隐式的QUACK项目研究了如何在SPIN中处理具有过去和未来算子的公式（详见[42]），以及如何应用M. Pezzè等人理论计算机科学电子笔记116（2005）113119−使用TRIO公式执行模型检查的原则（详见[34]）。[34]中描述的技术围绕着“事件生成器”的概念，它探索了组成系统的对该空间的穷举搜索将在算法的复杂性中产生组合爆炸，因此为了使基于事件生成器的方法可行，引入了一些优化。这些优化集中在TRIO模块的“输入”和“输出”变量的概念上，特别是，an “output” variable can beQUACK方法通过TRIO规范的定理证明补充了模型检查，重点是语言的模块化特征，允许指定基于组件的系统。为了支持QUACK方法中基于TRIO的定理证明，修改和扩展了PVS中TRIO的编码，并开发了PVS支持的TRIO演绎证明的组合框架。复合框架是围绕一个新的时间操作符（+d，称为“while-plus”），并在一个声音复合推理规则的在这里，我们用一个简单的例子来概述这种方法 设S是由n个模C1，...组成的系统，Cn.设每个模i = 1，.，n与关于其环境的行为的假设E i和模块本身的行为属性Mi相关联，即，每个模块i = 1，...，n与以下形式的一个规范相关联：假设Ci的环境在E i中的行为，我们可以保证该模块在M i中的行为。通常，系统S具有其自身的与之交互的环境。设E是我们对S的环境所做的假设S的特征在于以下形式的全局规范：假设S的环境行为与E中的一样，我们可以保证复合模块的行为与M中的一样。为TRIO语言开发的合成推理规则让我们从Cis的局部指定的有效性中推导出S关于QUACK技术中基于TRIO的定理证明的更多细节可以在Furia和Rossi的论文[17]中找到在定理证明的背景下，组合性的概念也被探索TILCO。TILCO时态逻辑使用定理证明来确保TILCO编写的规范的重要属性，例如安全性120M. Pezzè等人理论计算机科学电子笔记116（2005）113和活力。[8]中所示的TILCO表达算子（动态区间，有界hap- pen）允许以可读的形式表达非常复杂的性质。[7]中提出的TILCO的扩展（CTILCO，即，通信TILCO）为复杂系统的组合/分解和过程通信提供了一种新的模型。在CTILCO中，可以从几个相互关联的过程中获得规范，并且可以进行定理证明以验证不同过程之间相互作用的正确性在QUACK方法的背景下，PVS的使用进行了研究，并已产生的策略，以证明TILCO表达式，这种策略是基于特设引理的基本TILCO运营商。在[19]中讨论了使用类状态和类事件概念的组合（而不是将指定字母表限制为任何一种项目）对作为QUACK方法的一部分，关于CTILCO应用的案例研究可以在Bellini等人[9]的论文中找到。TILCO方法最重要的特征是规范的可执行性[5]。TILCO规范可以在实时环境中执行，其中确定每个时刻的系统输出的计算成本是有界的和可预测的。执行过程需要在一个较低级别的语言称为基本时态逻辑的TILCO规则的转换。由于这种形式主义，有可能获得一个时间推理网络，其演变产生系统的反应行为。这个过程已经被一个合适的编译器自动化，以产生一个模拟推理网络的文件;这个文件由TILCO执行器加载，它根据输入历史产生输出在QUACK方法中，从特定执行实现实时系统的开发步骤一个新的集成开发环境，称为Dev-TILCO，已经创建，以更好地回答高生产力的开发工具的工业要求。在Dev-TILCO中，可以通过考虑正式部件和传统编程语言模块（C++源代码）来执行正式规范设计[6]。开发过程从一个设计开始，该设计将单个进程和交互的时间行为与可执行代码分离。与系统事件相关的时态谓词（输入或输出）的名称在规范中声明和使用。这些声明被自动处理以获得编程语言对象，这些对象连接到TILCO执行器（以执行行为规范），并可与应用程序的其他源代码一起使用，以便构建M. Pezzè等人理论计算机科学电子笔记116（2005）113121由时间约束的形式描述所规定的可执行程序。与事件驱动编程中的谓词类似，事件与特殊函数相连接，这些函数可以自定义为与程序的“经典环境”（如类型化内部变量、函数或线程）进行交互4基于代理的系统的新配置的测试开发一个新的异构、模块化和可配置的嵌入式系统通常是基于修改已经使用的同一系列系统的模块子集在一般情况下，一些组件被删除，另一些被修改，还有一些被添加。已经存在的组件经常被直接重用或进行小的修改。由于新组件触发的交互中的细微差异，新组件的集成可能导致故障。例如，让我们考虑一个系统，其中一个组件负责动态选择最佳目录来定位某些项目。此外，让我们考虑这个组件替换和更新以前的组件，在同一系统的另一个配置中，该组件能够在固定目录中定位项目。在这种情况下，当星表不能动态定位或在某些执行条件下变得不可用时，新系统可能会失败，这在以前的配置中从未发生过。新系统在许多情况下可能会正确运行，只有在特定情况下才会失败。测试和分析基于组件的软件的问题已经在去年进行了研究[44，40]，但到目前为止提出的解决方案并没有解决问题的所有方面。Binder提出的可测试性设计技术，并由Martins等人提出的自测试组件扩展，假设组件适当地配备有用于测试的内置设施[11，30]。Liu和Richardson提出的逆向元件需要测试仪设计人员的大量工作，因此意味着大量成本[28]。Edwards提出的BIT包装器需要详细了解组件设计，因此并不总是适用于第三方COTS [12]。在QUACK项目期间开发的技术源于Pavlopoulou和Young [39]的永久测试的基本思想，并利用Ernst等人[13]的不变检测技术。该技术不需要了解组件内部结构的具体知识，也不需要详细了解规格，从而克服了以前工作的主要可用性限制。该技术适用于一个或多个组件122M. Pezzè等人理论计算机科学电子笔记116（2005）113图二.自动记录组件的行为。交互和刺激记录器被插入系统和被监控组件之间用新的替换以获得新的系统，并且基于三个主要阶段：数据收集，不变检测和组件验证。在数据收集阶段，目标系统被自动配置为收集关于组件之间以及组件与环境之间的交互的信息。不变检测阶段将运行时收集的信息提取为：I/O不变量描述了系统和被监控组件之间交换的数据的属性，交互不变量，其描述被监视组件与系统的其它组件代表记录器交互的集成测试数据记录过程如图2所示。互动和刺激- ULI记录器捕获组件与系统的交互。它们可以基于不同的技术。在QUACK原型中，我们为Java设计了在系统启动时绑定的非侵入式记录器。I/O不变量蒸馏器I/O不变量M. Pezzè等人理论计算机科学电子笔记116（2005）113123通过Daikon（Ernst et[13]，它适用于简单的标量变量和集合。交互不变量提取器计算一个正则表达式，该表达式总结了组件和系统之间的交互模式。最后，测试数据生成器根据不同的标准过滤记录仪数据，以选择适合集成测试的收集数据的合理子集。在组件验证阶段，验证并测试新组件与系统的兼容性。验证基于数据收集阶段收集的变量。当用已在其他版本或配置中使用的新组件替换组件时，将对照系统不变量检查新组件的不变量。然后对识别出的问题进行分析，以发现新系统中的潜在问题。测试基于在数据收集阶段收集的集成测试数据的执行。预言机是从系统不变量自动派生的。关于QUACK技术用于测试基于组件的系统的新配置的更多细节可以在Mariani和Pez `e的论文[2 9]中找到。5验证非功能特性实时系统的正确性不仅取决于它不仅取决于产生结果的时间，而且取决于产生结果的时间。时态逻辑规范支持对早期需求的时态属性的分析。时间约束也必须在设计和部署级别进行验证。在设计层面，我们为每个活动分配一个最坏情况下的执行时间，并计算所有活动的最坏情况交错，以查看是否满足约束。基于构件的实时嵌入式系统的研究大多集中在软件设计阶段。直到最近才考虑到诸如截止日期之类的非功能性约束。特别是，基于组件的软件开发技术最近才被应用到安全关键的实时系统的设计和实现，几乎没有实际效果。在实时系统中充分应用基于组件的设计方法之前，还需要解决许多问题实时系统通常由多个并发的循环任务组成。因此，其组件的第一个要求是多线程，即，组件必须能够执行一组并发线程。没有一种方法明确地解决包含多个124M. Pezzè等人理论计算机科学电子笔记116（2005）113一个线程。OMG已经提出了UML-RT profile，性能、性能和时间规格[37]。此概要文件允许使用UML设计实时应用程序。然而，该轮廓不太适合基于组件的设计。Isovic、Lindgren和Crnkovic [23]在时隙移位调度器[16]的上下文中提出了一个类似的想法，但在他们的方法中，组件由一个单一的线程组成QUACK方法解决了指定包含执行线程集的组件的问题，特别关注指定每个组件的调度策略的问题。事实上，在多线程实时系统中，调度器扮演着重要的角色。固定优先级调度通常用于实时系统，其中每个线程被分配一个以整数表示的固定优先级。但是，如果一个组成部分是孤立开发的，就不清楚如何确定优先次序。一个组件的开发人员可以将组件内部线程的优先级此外，不同的组件可能想要使用不同的调度策略，诸如最早期限优先（EDF）、静态或非抢占式调度。如果不同的组件需要不同的装配工，那么就不可能在最终系统中装配所有组件QUACK中提出的方法使用分层调度框架：每个组件可以指定自己的调度器;系统实现全局调度器，该全局调度器选择要执行的组件，并调用所选组件的调度器来选择要执行的线程Quack还考虑使用时间隔离技术：由于每个组件都是孤立开发的，因此在最终系统组装之前，有必要对其进行隔离分析和测试。Quack提出了一种技术，可以将实时系统中时间保护的一般方法是资源预留框架[32，33]。Rajkumar [43]提出的基本思想是，每个任务都被分配了一个服务器，该服务器保留了处理器可用带宽的一小部分：如果任务试图使用超过分配的带宽，则会减慢速度。该框架允许任务在系统中执行，就好像它在专用虚拟处理器上执行一样，其速度是处理器速度的一小部分。通过使用资源预留机制，可调度性分析问题被简化为在不考虑系统其余部分的情况下估计任务最近，已经提出了许多技术来扩展资源M. Pezzè等人理论计算机科学电子笔记116（2005）113125保留框架到分层调度[26，45]，但到目前为止，它们都没有在基于组件的软件开发的上下文中完成在QUACK中，我们开发了一种方法，用于指定和分析基于组件的实时系统，其中每个组件由一个或多个并发线程组成，并可以指定自己的调度策略。在我们的方法中，每个组件被分配的处理器带宽的最小部分，它是从其他组件的干扰保护。我们开发了一个组件的数学模型来计算最佳的服务器参数分配给一个组件，以确保满足时间约束。详细说明和分析的方法，层次，卡尔调度策略的组件为基础的系统，可以发现在这卷的文件利帕里等人。[27]第10段。与嵌入式系统相关的另一个非功能性方面是可靠性，也就是说，即使在系统本身或外部环境发生故障的情况下，故障注入是一种可用于评估系统（硬件或软件）可靠性的技术[22]，它涉及对故障和错误的研究，以便重新创建特定的故障场景来测试系统的容错架构。Bernardeschi，Fantechi和Gnesi提出了一种在规范级别注入故障的方法，并展示了如何使用模型检查来验证规范级别的容错性[10]。QUACK完善并扩展了该方法，并通过分析SCA系统（Sistema ContaAssi，轴计数器系统）评价了结果，如[15]所述。SCA是一种铁路信号装置，用于确定给定的铁路区段是空闲的还是仍然被列车占用。通过检查进入和离开特定PRA的轮对数量来计算铁路的状态，即， 铁路上的检测点。 如果进入该区段的轮对数量等于离开该区段的轮对数量，则PRA是空闲的。该信息由控制和采集单元（称为UCA）使用，以通过适当的信号量启用或阻止下一列列车进入该区段。SCA模型上的注入是通过连接一个合适的SDL块（模拟故障注入器）到UCA单元的SDL模型来完成的。此块包含一个SDL进程，称为故障注入器进程，它使用扩展有限状态机（EFSM）对故障注入活动进行建模。该EFSM可以根据要执行的故障注入的类型来确定。设计了一个合适的SDT模拟器界面，其中包含一些主要的SCA信号和命令，用于配置、激活和停止In。126M. Pezzè等人理论计算机科学电子笔记116（2005）113喷射器;在模拟特定场景时，可以使用消息序列图（MSC）跟踪系统的演变。容错行为可以使用一个或多个MSC来验证，表示系统必须以容错方式对错误信号做出反应的场景：如果MSC被违反，SDT验证器返回MSC，指示容错场景被违反的方式，从而允许修改SDL系统以纠正错误。Banci等人在本卷的论文中详细阐述了[15[4]的文件。6生产结束测试QUACK方法包括一种用于异构、模块化和可配置嵌入式系统的最终生产（EOP）测试技术，这在行业中是强制性的。这种技术能够将测试场景（由设计人员给出或从模型生成）转换为测试命令。测试命令由被测系统周围的测试模拟器处理。通过这种方式，从高级场景开始，可以使用常见工业模拟器的测试环境自动生成功能测试场景本节介绍了该技术的最关键点，即翻译过程。设计级别和最终命令之间存在很大的差距，测试设备，即，在翻译阶段的输入和输出之间。一方面，在设计阶段，系统描述通常是通常，这些描述采用消息的形式，表示系统的用户视图。例如，诸如“电话呼叫（号码：123-4567）”和“挂断”的消息在移动电话的描述中将是非常常见的。另一方面，测试命令通常是标准测试模拟器的低级命令，在模拟器命令集中声明并高度定制。例如，典型的测试命令可以指一组测试资源，诸如端口和接口。为了填补这一空白，我们定义了一个中间概念：测试级消息。测试级消息是测试命令的消息表示。为了构建测试级消息，我们使用自底向上的方法，即，我们从模拟器的命令集和代表测试环境的执行器开始。模拟命令消息通常需要设置系统的工作环境。例如，模拟蜂窝电话的命令CALL需要环境中存在蜂窝网络，否则M. Pezzè等人理论计算机科学电子笔记116（2005）113127图三. 翻译过程不能打电话。环境编程对于测试设计人员来说是一项艰巨的任务，因为需要大量的环境消息，而且环境中的错误设置可能会改变测试结果。为了减少工作量和错误，我们的技术为每个测试级消息提供了一个默认的环境。默认环境由测试引擎创建，同时默认观察消息的结果设置测试环境的转换过程分为准备和转换阶段，如图3所示。测试准备阶段确保测试用例符合目前的测试环境。这是通过根据一组预先定义的要求（表示为规则）检查测试用例来实现的，如果这些要求得到满足，则可以进行翻译。这个阶段是完全自动的。测试翻译阶段包括三个步骤：映射步骤在设计级的信息和测试命令之间建立对应关系。这个步骤的输入是一个设计级测试用例，之前在测试准备阶段确认过，而输出是一个非空的测试级序列图集。映射步骤执行三个不同的操作：解析消息多态性;将设计层消息转换为测试层消息;以及添加默认环境和观察消息。当设计级消息可以以不同的方式（例如，使用语音控制或键盘）发送到系统时，它是多态的这意味着翻译不是唯一的，即，存在对应于相同设计级别消息的不同测试消息。多态性的分辨率可以是完全的（遵循完全或部分覆盖标准，例如，随机）或手动（由测试设计者执行）。除了多态性之外，映射步骤是自动的。预排序步骤将最小定时属性分配给测试消息。测试设计人员可以指示消息的特定定时或分配默认定时，并按顺序使用最小的命令间延迟128M. Pezzè等人理论计算机科学电子笔记116（2005）113以保持测试执行时间尽可能短定序步骤将在映射步骤生成的测试级序列图连同由预定序步骤添加的定时一起翻译成测试环境可直接理解的命令列表。这一步主要基于测试引擎。测试引擎是在专用工作站上运行的软件;测试引擎使用时间轮控制模拟器。时间轮广泛用于硬件世界中的仿真环境中。 延迟使用划分为刻度或槽的时间轮来跟踪，每个槽代表一个时间单位。 软件指针在计时轮上标记当前时间。随着模拟的进行，指针在每个时间步向前移动一个时隙。 事件列表跟踪未决事件，当指针移动时，模拟器处理当前时间的事件列表。在时间轮上，我们直接向模拟器指示定时命令，因此第一个操作是将每个测试级消息转换为一组模拟器命令，并通过测试准备阶段保证存在性和唯一性。在预排序步骤期间插入的消息之间的最小延迟由测试命令继承由于每个测试命令都有一个相关的执行时间，测试引擎必须提前将每个命令发送到适当的模拟器。此外，测试引擎使用时间轮来跟踪测试资源的使用情况。事实上，即使注入消息所需的所有定时都得到遵守，也可能发生某些其他消息所需的环境设置在这种情况下，测试被宣布为失败。关于翻译过程的更多细节可以在[1，2，3]中找到。7结论异构、模块化和可配置的嵌入式系统在许多应用领域越来越受欢迎，因为该技术引入的可扩展性允许以低成本生产复杂的系统。然而，这类系统需要新的质量要求，传统的规范、测试和分析技术无法满足这些要求本文提出了一套评估异构、模块化和可配置嵌入式系统质量的新技术。所提出的技术涵盖了目标系统类软件过程中的所有主要质量评估需求，支持：具有实时需求的基于组件的系统的定义和验证;隔离组件及其集成的评估;可扩展性M. Pezzè等人理论计算机科学电子笔记116（2005）113129基于组件特性的组合系统的容错特性、嵌入式组件测试用例的生成以及测试用例在测试环境中的自动部署到目前为止，我们将所提出的技术应用于最初的一组案例研究，包括我们的研究合作伙伴提供的工业系统，从该领域的文献中提取的知名示例，以及说明组件技术使用的结果是有希望的，即使是初步的。我们现正继续进行实验，旨在提高我们对QUACK方法的信心及知识，并完善及调整单一技术。引用[1] Baldini，A.，A. Benso，S. Mo，A.陈文辉，一种基于UML的系统级功能测试，载于《集成设计与过程技术学报》[2] Baldini，A.，A. Benso，P. Prinetto，S. Mo和A. Taddei，Towards a unified test process：fromUML to end-of-line functional test，in：Proceedings of the IEEE International Test Conference2001（ITC600-608[3] Baldini，A.，A. Benso，P. Prinetto，S. Mo和A. Taddei，系统测试的有效设计：分层体系结构，在：IEEE国际测试会议2002（ITC930-939[4] Banci，M.，M. Becucci，A. Fantechi和E. Spinicci，铁路信号系统的基于组件的SDL模型的验证覆盖率，在：第二届基于组件的软件测试和分析国际研讨会论文集（TACoS[5] Bellini，P.，A. Giotti和P. Nesi，TILCO时序逻辑规范的执行，在：第八届复杂计算机系统工程国际会议（ICECCS'02）会议记录，78比88[6] Bellini ， P. ， A. Giotti ， P. Nesi 和 D. Rogai ， TILCO Temporal Logic for Real-time SystemsImplementation in C++，in：Proceedings of the 15th International Conference on SoftwareEngineering and Knowledge Engineering（SEKE[7] Bellini，P.和P. Nesi，Communicating TILCO：a model for real-time system specification，in ： Proceedings of the 7th International Conference on Engineering of Complex ComputerSystems（ICECCS四比十四[8] Bellini，P. and P. Nesi，TILCO-X an extension of tilco temporal logic，in：Proceedings of the7th International Conference on Engineering of Complex Computer Systems（ICECCS15-25[9] Bellini ， P. ， P.Nesi 和 D. Rogai ， Validating component integration with C-TILCO ： A casestudy ， in ： Proceedings of the 2nd International Workshop on Test and Analysis ofComponent- Based Software（TACoS[10] Bernardeschi，C.，A. Fantechi和S. Gnesi，Model checking fault tolerant systems，SoftwareTesting，Verification and Reliability12（2002），pp.251-275[11] 宾德河，面向对象系统的可测试性设计，ACM通信37（1994），pp. 87比101[12] 爱德华兹，S.，A framework for practical，automated black-box testing of component-basedsoftware，Software Testing，Veri fication and Reliability（STVR）11（2001）.130M. Pezzè等人理论计算机科学电子笔记116（2005）113[13] 恩斯特，M.，J. Cockrell，W. Griswold和D. Notkin，Dynamically discovering likely programinvariants to support program evolution ， IEEE Transactions on Software Engineering27（2001），pp.99比123[14] Fantechi，A.和E. Spinicci，SCA SDL模型的故障注入，技术报告，QUACK技术报告，DSI（2003）。[15] Fantechi ， A. 和 E. Spinicci ， Modeling and validating a multiple-configuration railwaysignaling system using SDL，Electronic Notes in Theoretical Computer Science82（2003）。[16] Fohler，G.，静态调度系统中分布式复杂周期与硬非周期任务的联合调度。第16届实时系统研讨会论文集，意大利比萨，1995年。[17] 富里亚角A.和M. Rossi，一个用于正式验证模块化系统的组合框架，在：第二届国际基于组件的系统测试和分析国际研讨会，巴塞罗那，西班牙，2004年，已提交出版。[18] Gargantini，A.和A. Morzenti，Automated deductive requirement analysis of critical systems，ACM Transactions on Software Engineering and Methodology（TOSEM）10（2001），pp. 255[19] Gargantini，A.，A. Morzenti和E. Riccobene，使用计数器来建模事件之间的时间关系，在：Proceedings of State-oriented vs. Event-oriented thinking in Requirements Analysis，FormalSpecification and Software Engineering，Pisa，Italy，2003。[20] Ghezzi角，D. Mandrioli和A. Morzenti，TRIO：A Logic Language for Executable Specificationsof Real-Time Systems，The Journal of Systems and Software12（1990）.107-123[21] Holzmann，G.J.，SPIN模型检查器，IEEE软件工程学报23（1997），pp. 279-295.[22] Hsueh，M.，T. Tsai和R. Iyer，Fault injection techniques and tools，Computer30（1997），pp.75比82[23] Isovic，D.，M.我和林格伦。陈志荣，系统开发与实时组件，在：Proc. of ECOOP 2000Workshop 22 - Pervasive Correct-based systems ， Sophia Antipolis and Cannes ， France ，2000。[24] 拉瓦扎湖 S. Morasca和A. Morzenti，双语教学法 到 的 用UML开发时间关键系统，在：关于用UML进行关键系统开发的UML'03研讨会论文集，旧金山，美国，2003年，慕尼黑工业大学报告TUM-I 0323。[25] 拉瓦扎湖S. Morasca和A. Morzenti，用UML开发时间关键系统的双语言方法，在：第二届基于UML的软件测试和分析国际研讨会（TACoS'04）会议记录[26] 利帕里湾和S. K.张文龙，等离子体光谱仪的结构与性能研究，国立成功大学光电工程研究所硕士论文，2001。[27] Lipari，G.，P. Gai，M.特里马尔基湾Guidi和P.Ancilotti，基于组件的实时系统的层次框架，在：第二届基于组件的软件测试和分析国际研