基于模型的集成与测试方法的研究与分析

理论计算机科学电子札记164（2006）13-28www.elsevier.com/locate/entcs一种基于模型的减少系统开发时间的集成与测试方法N.C.W.M. Braspenning1 J.M. van de Mortel-Fronczak2J.E. Rooda3埃因霍温理工大学机械工程系P.O. Box 513，5600 MB埃因霍温，荷兰摘要在高科技多学科系统的开发中，需要新的方法和技术来减少非常昂贵的集成和测试任务（在前置时间、成本、资源方面）为了促进这一进程，减少，我们提出了一种方法称为基于模型的集成。该方法允许将尚未物理实现的系统组件的正式可执行模型与其他组件的可用实现集成。模型和实现的组合然后通过验证、验证和测试用于集成系统的早期分析。 这种分析能够及早发现和预防在实际集成过程中可能发生的问题，从而显著减少在实际集成和测试阶段投入的时间。 本文阐述了模型如何为基于模型的集成而开发的组件的模型可用于自动化的基于模型的测试，这允许及时有效地确定组件实现相对于其需求的一致性。结合基于模型的集成和基于模型的测试实际说明了一个现实的工业案例研究。 从这项研究中获得的结果鼓励进一步研究基于模型的集成作为一个突出的方法，以减少集成和测试的误差。保留字：基于模型的集成，基于模型的测试，工业案例研究1介绍像晶圆扫描仪、电子显微镜和高速打印机这样的高科技多学科系统每天都变得越来越复杂这些系统由许多硬件和软件组件组成，通过许多内部连接，这项工作是嵌入式系统研究所负责的TANGRAM项目的一部分。该项目部分由荷兰经济部资助，资助项目为TSIT2026。1 电子邮件（通讯作者）：n.c.w.m. tue.nl2 电子邮件：j.m.v.d. tue.nl3电子邮件：j.e. tue.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.00314N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）13在市场条件下，交货时间（在上市时间的背景下）至关重要，因此必须满足客户设定的严格质量要求。这种不断增加的系统复杂性也增加了所谓的集成和测试阶段所需的工作量。在这些阶段中，系统通过组合组件实现（实现）来实现，随后根据系统需求进行测试。在当前的大多数开发过程中，集成和测试阶段在组件实现可用时开始因此，主要的交付周期负担正在从设计和实现阶段转移到集成和测试阶段[6]。此外，在系统开发过程的后期发现和修复集成和测试问题（目前的方法就是这种情况）可能比在需求和设计阶段发现和修复问题要昂贵100倍[3]。许多研究活动旨在应对这种开发任务的增加（在交付周期，成本，资源方面），涉及基于模型的技术，如需求建模[8]，基于模型的设计[13，17]，基于模型的代码生成[9]和硬件-软件协同仿真[19]。然而，在大多数情况下，这些基于模型的技术被孤立地研究，很少有工作报告将这些技术结合成一个整体的方法。虽然基于模型的系统工程[18]和OMG此外，文献几乎没有提到这种方法的实际工业应用，至少没有提到高科技多学科系统。我们在TANGRAM项目[20]中的研究集中在基于模型的集成方法上，在该方法中，基于模型的技术被开发并应用于工业中，以减少集成和测试工作量。在该方法中，尚未物理实现的系统组件的模型与其他组件的可用实现集成，建立基于模型的集成系统。该基于模型的集成系统用于在实现所有组件之前进行系统级分析。这种早期的分析将集成和测试扩展从其关键位置中剥离出来，并使开发人员能够检测和预防在实际集成期间可能发生的问题（即更早，因此更便宜），最终导致扩展的减少。此外，基于模型的分析技术有助于澄清和改进系统的需求和设计（通常是明确和确定的）到所有组件的需求和设计（通常是不明确的和基于假设的）的经常困难的分解。这些在系统分解中改进的见解最终提高了质量的系统实现。在充分和成功的验证和核实之后，用于基于模型的集成的模型是相应组件的需求和设计的良好表示。当这样一个组件的实现变得可用时，在集成之前确定这个实现是否符合模型（从而符合需求和设计）将是很有意思的N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）1315它进入系统。 当在此分析过程中发现组件的实现和模型之间的差异时，这意味着在实现中发现了需要修复的问题，或者它指出了需求和设计中需要改进的不完整或不清晰的部分。测试一个组件实现相对于一个规范模型的一致性是基于模型的测试研究的主题[7]，为此，几个基于模型的测试工具[14]可用。在本文中，我们描述了基于模型的集成方法是如何扩展与基于模型的测试，以确定组件实现是否符合基于模型的集成开发的模型该方法和扩展已被应用到一个工业案例研究有关ASML[1]晶圆扫描仪。本文的结构如下。首先，在第2节中介绍了基于模型的集成方法以及相关的技术和工具。第3节描述了如何通过基于模型的测试扩展该方法案例研究应用和结果见第4节。最后，在第5节中得出结论并进行讨论。2基于模型的集成在当前的工业实践中，系统开发过程被细分为多个并发的组件开发过程。随后，将得到的组件集成到系统中。组件Ci的开发过程包括需求定义阶段、设计阶段和实现阶段。这三个阶段中的每一个都导致组件的不同表示形式，即组件的需求、设计和实现，在这里分别表示为Ri、Di和Zi。在由多个组件（例如组件C1和C2）组成的系统S的开发过程中，系统需求和系统设计（在此分别表示为R和D）先于组件的开发过程。系统S是组件C1和C2的实现Z1和Z2的集成结果。该集成表示为{Z1，I12，Z2}，其中I12表示连接Z1和Z2的基础设施。图1显示了系统S的开发过程。定义设计设计设计实现实现整合I12整合Fig. 1. 当前系统开发过程在这种工作方式中，只能应用两种类型的系统级分析RR1定义D定义R2D1D2Z1Z216N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）13一方面，可以检查组件级和系统级的需求和设计之间的一致性，例如R与R1，R2和D与D1，D2（这通常意味着要审查大量文档）。另一方面，综合系统实现，例如{Z1，I12，Z2}，可根据系统要求进行测试和设计，研发，只要所有组件都实现和集成。这意味着，当问题发生并需要在集成和测试阶段修复时，在这些阶段投入的时间会立即增加，直接威胁到系统的按时交付。提出了一种基于模型的集成方法，以减少集成和测试的工作量。在该方法中，组件的设计（例如，软件、机械、电子）由通信并发进程的形式化可执行模型表示，用进程代数表示[2]。由此产生的模型，在这里表示为组件Ci的Mi，使组件和系统的形式化分析成为行为通过模型验证（例如仿真），可以检查系统模型的某些迹线的行为，例如{M1，I12，M2}，并将其与预期的系统设计D进行比较。通过模型验证（例如，模型检查），它可以检查系统模型是否满足从系统要求R和系统设计D导出的某些特性这种基于模型的系统分析有助于评估和改进将系统的需求和设计分解为组件的需求和设计的正确性。除了模型支持这些额外的分析技术之外，它们还可以取代集成测试的实现。这意味着模型和实现的集成可以针对系统需求和设计进行测试，而不需要所有组件实现都可用。由于模型通常比实现更早可用，因此系统级的测试可以更早开始。早期测试允许更早地检测和预防系统集成问题，这将导致在实际集成和测试期间投资的工程量减少。图2示出了基于模型的集成方法中的系统S的开发过程，其中Mi表示组件Ci的模型（基于其设计Di），并且其中I12表示允许组件C1和C2的集成的基础结构，组件C1和C2都由模型或实现表示。注意，通过代码生成，软件组件Zi的实现可以基于其模型Mi。在我们的研究中，组件被建模为时间过程算法χ[23]（混合χ[24]的简化版本）中的过程，该算法由埃因霍温理工大学系统工程组开发对于每个组件，对进程的内部行为（分配、保护替代、保护重复、延迟）和与其他进程的外部通信（发送、接收）进行建模。组件系统被建模为所有组件进程的并行组合，通过通信通道连接。χ工具集包含一个模拟器来模拟这样的系统模型。此外，χ工具集还增加了几个后端，以支持其他分析技术，如模型验证、分布式/实时仿真和软件/硬件在环测试，N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）1317定义设计设计设计整合整合I12整合整合图二. 系统开发过程中基于模型的集成方法它们都用于基于模型的集成方法中。正如在引言中提到的，在组件实现与其他组件集成之前，确定组件实现在可用时是否符合用于基于模型的集成的模型是很有趣的。因此，前面提到的一组分析技术被扩展为基于模型的测试。3基于模型的测试基于模型的测试为自动化测试提供了理论和工具，作为手动和脚本测试的替代方案，自动化测试越来越受到关注在基于模型的测试中，一个组件的正式规格模型用于生成测试，这些测试在组件实现上实时执行，导致“通过”或“失败”的测试判决。在TANGRAM项目中，基于输入输出一致性（ioco）理论的测试工具T或 X[21]用于基于模型的测试。虽然正在开发针对定时测试[4]和更复杂数据测试[12]的扩展，但我们实验中使用的T或 X版本仅支持基于模型的无定时离散事件系统测试，而无需复杂数据。如前所述，用于基于模型的集成的模型是在χ中开发的，目前T或 X不支持。然而，T或 X支持TROJKA[10]略加修改的版本，PROMELA，用于模型检查器S引脚[15]。 SPIN也用于模型验证后端，χ工具集[5]，为此开发了从χ到PROMELA的翻译方案[22]。通过将χ到PROMELA的转换与T或 X的基于模型的测试能力相结合，可以确定组件实现相对于用于基于模型的集成的χ模型的一致性这种方法在图3中为系统S可视化，在这种情况下，组件2的实现首先在该图中，用于与M1 ，χ进行基于模型的集成的分量2，M2，χ的χ模型被转换为PROMELA等价物，M2，P。随后，T或 X测试用于与M1、X的基于模型的集成以及稍后用于与Z1的真实集成的实现Z2是否符合RR1定义D定义R2实现D1模型M1Z1D2模型M2实现Z218N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）132PromelaM2、PM2，P.基于模型的{M1，I12，M2}集成基于模型的{M1，I12，Z2}集成{Z1，I12，Z2}的实积分M1，整合I12整合M2，M1，整合I12整合艾科？Z2Z1整合I12整合Z2图三. 基于模型的集成和使用χ和T或 X进行扩展了基于模型的测试的基于模型的集成方法的程序如下：1. 基于部件的设计，对部件进行建模，例如M1和M22. 仅使用模型对集成系统进行确认和验证，例如{M1，I12，M2}，采用χ模拟和SPIN模型检验.3. 对于每个组件：(a) 通过实现替换模型，例如M2byZ2，使用能够与其他组件集成的基础设施.(b) 基于模型的组件实现测试，例如：Z2相对于M2，使用T或 X.(c) 对组合模型和实现进行基于模型的集成测试，例如：{M1，I12，Z2}，通过执行从R和D导出的测试用例。4. 通过执行来自研发的测试用例，对完整系统实现进行集成测试，例如{Z1，I12，Z2}。请注意，在本文中，不同的测试技术用于组件测试（步骤3b，使用基于模型的测试）和系统集成测试（步骤3c和4，使用在集成模型和实现上执行手动导出的测试用例）。其原因是，仅测试方法中使用的基于模型的测试技术所涵盖的方面对于我们研究中考虑的系统是不够的，而基于模型和真实集成测试中使用的技术然而，基于模型的测试原则上可以用于系统集成测试，通过使用集成系统模型，例如{M1，I12，M2}，测试生成的基础，并通过使用集成的组件实现，例如，{Z1，I12，Z2}，作为受试系统。只要集成系统模型的大小和复杂性没有超出测试工具的限制（模型抽象可以用来解决这个问题），并且只要测试工具可以N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）1319访问集成系统实现所需的测试接口。此外，本文没有考虑组合测试技术，如[25]中所述，以基于单个组件的一致性来暗示集成系统的一致性。这种组合测试技术要求模型是完整的，即明确规定任何可能输入的所有允许响应，而为基于模型的集成开发的模型并非如此。4案例研究：ASML激光子系统在前面的章节中描述的基于模型的集成和测试方法已被应用到一个案例研究有关的激光子系统的ASML晶圆扫描仪，这是用于光刻工业的集成电路或芯片的生产在晶片扫描仪中，发生用特定图案（对应于芯片的一层）曝光硅晶片的光刻工艺。晶片扫描仪的激光子系统产生用于该光刻工艺的激光。作为晶片扫描仪一部分的控制器与激光子系统通信，以便获得每次曝光所需的激光量。该通信通过两个双向接口实现：用于命令和响应的串行（RS232）接口和用于多个状态信号的并行接口经验表明，晶片扫描仪控制器和激光子系统之间的接口难以理解、集成和诊断。这主要是由于激光子系统是由第三方制造商生产的，这意味着ASML工程师无法完全了解和控制激光子系统中实现的行为。因此，晶片扫描仪控制器和激光子系统的正确集成对于晶片扫描仪的性能和可靠性是重要的方面由于安全和成本的原因，在案例研究中使用了硬件激光模拟器而不是真实的激光器。这种硬件激光模拟器具有相同的软件和电子组件，并且被指定为与真实激光器相同的行为，但是它没有产生激光的物理组件激光模拟器由ASML开发，用于测试晶圆扫描仪控制器的软件和电子设备，而不需要真正的激光器（包括所需的空间和设施）。由于激光模拟器用于测试晶圆扫描仪控制器，因此激光模拟器的行为满足真实激光器的行为规范非常重要，以避免错误的测试结果，甚至更糟的是，晶圆扫描仪控制器中的错误修复在案例研究中，我们说明了上一节中描述扫描仪控制器和激光器子系统的模型已开发和集成在χ和χ仿真和S引脚模型检验分析随后，使用T或 X的基于模型的测试来确定硬件激光模拟器相对于激光子系统X模型的PROMELA等效物的一致性。这些步骤中的每一个步骤的应用和结果在续集中介绍20N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）13晶片扫描仪C命令响应激光子系统IO命令状态响应LC状态LS步骤1：组件建模激光子系统和与晶圆扫描仪控制器通信的规范文件我们的经验是，建模活动有助于发现和澄清需求和设计文档中的错误、不一致和不完整性图4显示了已经按照后续描述建模的流程（圆圈）和通信通道（箭头）注意，进程IO、LC和LS都是激光子系统的一部分configconfig见图4。 晶圆扫描仪控制器和激光子系统晶圆扫描仪控制器C该过程可以被配置（使用外部配置文件）以执行用于行为验证的特定命令序列例如，文件中规定的操作顺序。I/O接口IO这个进程从C接收命令，在LC或LS处理命令后，它将响应发送回C。激光通信LCThis过程接收的命令从C（由IO传递），并根据其配置（存储在外部配置文件中）执行必要的操作（例如状态更改）并创建相应的响应。激光器状态LS此过程跟踪激光器状态，IO使用该状态响应C发出的激光器状态查询命令。每个过程定义都包含组件的状态和临时行为以及通信行为（包括通信的数据）。这里，通信涉及激光子系统的串行和并行接口。此外，激光子系统过程包含“未知”命令（未指定命令）和“不良上下文”命令的错误处理N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）1321（特定状态下不允许的特定命令）。如前所述，在为基于模型的集成开发的模型中经常使用的时间行为和复杂数据不受案例研究中使用的T或 X此外，在案例研究的步骤2中使用的χ到PROMELA翻译方案和PROMELA语言本身在时间和数据方面都有其局限性因此，原始的χ过程已经适合于转换为PROMELA，并通过应用时间和复杂数据的抽象来使用T或 X这些抽象并不影响在案例研究的步骤2和步骤3由此产生的χ过程是可配置的，因为晶片扫描仪控制器的命令序列和激光子系统的行为可以在外部配置文件中进行修改，而无需修改和重新编译χ系统模型。在案例研究过程中，当硬件激光模拟器无法用于特定激光器类型而必须对另一种激光器类型进行建模时，系统行为建模的这种灵活性显示出其优势。通过对所有工艺的并行组合，得到了由扫描控制器和激光器组成的集成系统模型。在这里，并行组合操作符，如进程代数χ中定义的，被用作两个组件之间的基础设施（对应于图3中的I12）。生成的χ系统模型总共包含350行代码，包括必要的数据定义和函数。步骤2：综合模型的确认和验证步骤1中开发的集成系统模型已使用χ工具集的模型模拟器进行了验证已经执行了几次模拟运行，其中来自规范文档的命令序列（例如，用于打开和关闭激光子系统的命令序列）在晶圆扫描仪控制器进程C的配置文件中指定。根据模拟结果，激光子系统行为符合所有命令序列的规范文件除了验证之外，还通过S引脚模型检查验证了系统模型的某些属性。为了执行这种类型的分析，χ系统模型已被翻译成PROMELA，使用来自[22]的翻译方案。作为如前所述，该翻译方案和PROMELA语言本身在时间和数据方面具有其局限性，然而，在步骤1中应用的抽象产生了适合于翻译成PROMELA的模型。最终的PROMELA系统模型包含1850行代码，其中900行用于表示χ模型中使用的所有数据定义的等价物，300行用于表示χ模型中作为附加过程使用的所有函数的等价物。除了用PROMELA表示的模型外，还必须指定要验证的属性，以便使用SPIN进行模型检查。系统的八个性质已经得到验证：没有死锁，关于22N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）13一个特定的χ语句和六个模型特定的行为属性。检查是否存在死锁或无效的结束状态是S引脚中的标准选项。系统不变量已经通过在翻译的χ语句的前提和后置条件上定义安全属性来检查，其以线性速度表示逻辑（LTL）公式Q（前置条件→后置条件）。两种型号规格行为属性涉及允许的状态转换顺序，例如从其他四个模型特定的行为属性涉及所有可能的动作，回应每一个命令。例如，当激光器接收到“go o”命令时，当其处于“o "状态或”on“状态时，其保持在当前状态并以”not allowed“响应，或者当其处于”standby“状态时接收到”go o“命令时，其进入”o"状态并以“state o”响应。这用LTL公式表示：Q（cmd go o→（（state oUrsp not allowed）（不允许在Ursp上声明）（state standbyU（state ostandby（state o standbyUrsp stateostandby）所有该等性质均已核实，并认为正确。基于这些验证结果以及正确的模拟结果，有足够的证据表明该模型能够很好地代表激光子系统的要求和设计，因此是硬件激光模拟器基于模型的自动测试步骤3a/3b：激光子系统的基于模型的测试在案例研究的这一步中，我们使用在步骤1中开发的模型，并在步骤2中验证和验证，使用T或 X测试工具对硬件激光模拟器进行基于模型的自动测试。如图3所示，T或 X在一侧连接到模型，在另一侧连接到实现（在这种情况下是硬件激光模拟器）。为了将模型连接到T或 X，第2步的PROMELA模型被稍微修改，得到了适合T或X的TROJKA模型。一个TROJKA模型必须是一个开放的模型，这意味着一些渠道的过程是不连接到其他过程。这些不相连的通道是所谓的可观测通道，在这些通道上可以给出测试输入，并可以观察到测试输出。在案例研究中，通过从图4中删除C进程并为进程IO的未连接命令和响应通道提供特殊通道属性OBSERVABLE，获得了具有可观察通道的开放TROJKA模型。仅激光子系统的TROJKA模型包含1000行代码，其中300行用于表示所有数据定义，300行用于表示所有功能。为了将实现连接到T或 X，TROJKA中的抽象命令模型需要转化为真实的命令进行实现，N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）1323对于实现的响应，反之亦然。如前所述，通过串行接口和并行接口发送和接收硬件激光器模拟器（以及真实激光器）的真实命令和响应。不幸的是，从外部直接访问这些接口（如使用T或 X进行基于模型的测试所需）是有限的。 虽然从外部直接访问的功能为串行接口提供，但并行接口并非如此，因为该接口使用嵌入在晶圆扫描仪控制器的电子设备中的ASML由于激光子系统状态空间的较大部分只能通过使用并行接口来达到，因此外部接口访问的这种限制大大然而，仅能通过串行通信测试的简化行为仍然足以证明基于为基于模型的集成开发的模型的T或 X为了通过串行接口进行正确的通信，已在PYTHON中编写了一个适配器组件，该组件接受来自T或 X的测试输入，执行抽象模型命令到实际激光器命令（例如，128位左对齐字符串）的必要转换从激光器子系统接收对命令的响应，在将其转换回模型中使用的抽象响应之后，由适配器组件将其发送回T或 X现在模型和实现都已经连接到T或 X，硬件激光模拟器相对于模型的一致性可以通过基于模型的测试来确定。对于已经执行的所有三个测试运行，使用随机测试选择策略来从TROJKA模型中的命令集合中选择测试输入。通过适配器和提供的直接访问功能将选定的命令发送到激光模拟器，随后观察激光模拟器的响应并将其与模型中指定的行为进行第一次测试的深度有限（少于20个事件），不到10秒就发现了实现和模型之间的差异为了澄清发现的差异，图5显示了已自动测试的激光子系统的状态图在此图中，节点表示模型的状态，实线表示通过串行接口发送的命令（以“LS”开头），虚线表示对命令的响应（以“LS”或“？？”开头）。 顶部和底部的中心状态分别表示实际的激光器状态“待机”和“待机”，编号为“00”和“03”。“状态更改”、“状态查询”和“坏上下文”状态是命令和相应响应之间的请注意，图中未显示的任何其他命令都会导致00 '）。图6显示了第一个基于模型的测试运行的消息序列图，其中请注意，“=”和“？”字符被“eq”和“QM”替换24N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）13'？？= 02“”LS=00“图五、已测试的激光子系统行为因为它们不允许在PROMELA/TROJKA使用。当硬件激光器子系统处于“待机（03）”状态时（对“LS？”是“LS= 03”，从下面数第四个箭头），它接收命令“LS=03”（从下面数第三个箭头）并以当前激光器状态“LS=03”（从下面数第二个箭头）进行响应。然而，根据规范（参见图5），给出进入当前状态的命令（这里是“standby（03）”状态下的命令“LS=03”）应该会导致"bad context“响应（”？？= 02’),which is indicated by the last ‘Expected’ arrow in Figure这种差异导致了进一步的诊断表明，这种不符合是由于硬件激光模拟器错误处理行为的不正确实施在激光模拟器软件中直接修复该错误是不可能的，因为当时所需的知识和工具不可用。因此，为了能够进行进一步测试，对模型进行了小的修改，以便在下一次测试运行中，在处理“坏上下文”错误时，模型和实现之间没有差异第二次测试运行的深度也有限（少于20个事件），并且再次花费了不到10秒的时间，直到发现另一个差异，涉及处理“未知命令”错误。根据激光子系统规范，除“LS= 00”、“LS= 03”或“LS？”之外的任何激光命令，例如00）。然而，当选择这种被给予。进一步'LS=00'LS？'坏断状态上下文（00）查询'？？= 02“”LS=00“'LS=03''LS=00'状态状态变化变化'LS=03''LS=00''LS=03'LS？'不良立态（03）查询N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）1325见图6。 显示差异的诊断表明，这种不一致性也是由于硬件激光模拟器的错误处理行为的不为了能够进行进一步的测试，由T或 X选择的允许的测试输入的集合已经被限制为仅已知命令，即使得对于下一测试运行，将不测试激光模拟器的第三次测试运行中，前两次测试运行中发现的差异不再被检测到，持续了很长时间（测试深度超过1000个事件，花费超过15分钟），没有发现新的差异。虽然没有应用覆盖度量（因为这不是T或 X的当前特性），但第三次测试运行的测试结果提供了足够的证据，证明在实现和模型之间不会发现其他差异。通过基于模型的自动测试发现的两个实现错误在与ASML工程师讨论后，很明显激光模拟器主要用于在标称行为条件下测试晶圆扫描仪控制器。虽然错误可能看起来微不足道，通常不应该26N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）13在使用激光模拟器进行标称测试期间遇到的这些错误，该实验表明，在当前的工业工作方式中，这种错误不容易检测到，并且基于模型的集成和测试等更系统的方法肯定具有潜力。此外，当这些误差保持未被检测时，在晶片扫描仪控制器包含与激光模拟器误差相关的误差的情况下，它们仍然可能具有实质性影响在这种情况下，当开发测试依赖于激光模拟器时，晶片扫描仪控制器中的误差保持隐藏，并且当晶片扫描仪控制器与真实生产环境中的真实激光器一起使用时，这些误差可能在以后引起问题在已经进行的测试实验中，仅使用T或 X的常规测试特征测试了单个命令和响应之间的关系。然而，测试案例研究步骤2中验证的特定行为属性也很有趣，涉及后续状态转换的关系以及响应和当前状态的组合通过定义测试目的，可以将基于模型的测试运行聚焦到这些特定行为，这是T或 X支持的一个功能[11]。5结论将基于模型的系统集成方法推广到基于模型的系统测试方法。该方法和扩展都成功地应用于一个实际的工业案例研究中，通过χ模拟、S引脚模型检查以及分别使用T或 X生成和执行测试，实际说明了基于模型的验证、验证这些基于模型的分析技术促进了文档错误的检测，并提供了组件实现相对于相应需求的不一致性的自动检测案例研究是一个有益的调查的优势和挑战相结合的基于模型的集成和基于模型的测试。使用进程代数χ作为基于模型的集成的基础，允许轻松指定组件的状态，时间和通信行为;此外，χ支持几种复杂的数据结构。在χ中实现的模型可以很容易地集成，允许应用不同的基于模型的系统分析技术。随着这些分析技术的进一步改进，例如SPIN和T或 X的时间和数据扩展，以及通过改进和自动化X工具集的后端，用于使用SPIN进行验证和使用T或 X进行基于模型的测试（直接或通过PROMELA），我们可以实现基于模型的正式系统分析和自动测试生成的强大环境。此外，还需要做更多的工作来促进模型和实现的集成目前，允许模型和实现直接耦合的基础设施正在开发中。这种基于模型的集成基础设施应该能够处理分布式组件的同步/异步通信和实时执行问题。本文实际上说明了一个正式的方法，早期检测和预N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）1327一方面，系统集成问题的预防，另一方面，组件实现与其需求的一致性的时间效率与当前工业实践仅关注实现和通常使用手动测试技术相比，早期预防问题和有效的一致性测试有助于减少集成和测试误差。总之，基于模型的集成方法的当前结果看起来很有前途，但是需要进一步的研究和工业应用，以真正说明在高科技多学科系统的开发中集成和测试的减少。6确认这四个方面都需要有NicolaTrroncka、RenedeVries和WilDenis sssene ne s，以支持PROMELA、T或 X和测试基础设施。我们也感谢JanTretmanss、DraganKosticicc和TANGGRAMprojmber的宝贵意见和富有成果的讨论。引用[1] ASML，网址：http://www.asml.com。[2] 贝滕，J. C. M.和W. P. Weijland，[3] 伯姆湾W.和V.R. Basili，Software defect reduction top 10 list，IEEE Computer34（2001），pp.135比137[4] 博嫩坎普和A. Belinfante，Timed testing with TorX，in：FM 2005：Formal Methods：InternationalSymposium of Formal Methods Europe，Newcastle，UK，Lecture Notes in Computer Science3582（2005），pp. 173-188。[5] Bortnik，E. M.，N. Trcka，A. J. Wij s，S. P. L utt ik，J. M. vandd e Mortel-Fronczak，J. C. M. 好吧，W. J.Fokkink和J.E. Rooda，使用SPIN，CADP和Uppaal分析转台系统的χ模型，逻辑与代数编程杂志65（2005），pp.51-104[6] 布拉特湖。 G.， P. 你好，K。 A？dels wardanddW. 王文，“分布式实时系统的开发与演进”，《信息与软件技术》，2000年第42期。947-958[7] Brinksma，E.和J. Tretmans，测试转换系统：注释书目，在：MOVEP 2000187-195.[8] Broy，M.和O.Slotosch，从需求到验证的嵌入式系统，在：嵌入式软件：第一次国际研讨会，EMSOFT2001，Tahoe City，CA，USA（2001），pp.51-65.[9] Budinsky，F. J.，M. A. Finnie，J. M. Vlissides和P.S. Yu，从设计模式自动生成代码，IBM SystemsJournal35（1996），pp.151-171.[10] 德弗里斯河G.和J. Tretmans，使用Spin的On-the-Challenge一致性测试，在：使用Spin模型的自动机理论验证第四次，ENST98 S 002（1998），pp.115-128[11]德弗里斯河G.和J. Tretmans，Towards formal test purposes，in：Proceedings of the Workshop onFormal Approaches to Testing of Software，FATES61比76[12] 弗兰岑湖J. Tretmans和T. A. C. Willemse，Test generation based on symbolic specifications，in：Proceedings of the Workshop on Formal Approaches to Software Testing（FATES 2004），Linz，Austria，Lecture Notes in Computer Science3395（2004），pp. 1-15。28N.C.W.M. Braspenning等人/理论计算机科学电子笔记164（2006）13[13] Gomaa，H.，“Designing Concurrent, Distributed, and Real-Time Applications with UML,” Addison-Wesley Professional, 2000, 1st[14] Hartman，A.，基于模型的测试生成工具，AGEDIS报告，AGEDIS项目（2002）。[15] Holzmann，G. J.，模型检查器SPIN，Software Engineering Journal23（1997），pp. 279-295.[16] Kleppe，A.，W. Bast和J. Warmer，[17]刘，X.，J.Liu，J.Eker和E. A.李，异构建模和控制系统的设计，在：软件使能控制：信息技术的动态系统，威利-IEEE出版社，2003年页。105-122号。[18] 奥格伦岛基于模型的系统工程原理，系统工程3（2000），pp。38比49[19] 罗森，J.A.，硬件/软件协同仿真，在：DAC439-440[20] TANGRAM项目，网站，http://www.esi.nl/tangram。[21] Tretmans ， J. 和 E. Brinksma ， TorX ： Automated Model Based Testing ， in ： First EuropeanConference on Model-Driven Software Engineering，AGEDIS project，2003.[22] Trcka，N.， Verifyingχmodelsoffindustrialsystem s withithSpin，CommputerScie nceReports05-12，Eindhoven University of Technology（2005）.[23] van Beek，D.一、K. L.男人，M。A. Reniers，J. E. Rooda和R. R. H.李文，《时间Chi的语义与语义学》，计算机科学报告05-09，埃因霍温理工大学，2005年。[24] van Beek，D.一、K. L.男人，M。A. Reniers，J. E. Rooda和R. R. H. Schi Schulelers，混合Chi的一致性和一致性方程语义，逻辑与代数编程杂志68（2006），pp.129-210[25] van der Bijl，M.，A. Rensink和J. Tretmans，使用ioco进行组合测试，在：软件测试的形式化方法：第三届国际研讨会，FATES 2003，蒙特利尔，魁北克，加拿大，计算机科学讲义2931（2003），第100页。86比100