存储卡轻量级规范测试：MMC系统验证和自动化测试技术

理论计算机科学电子笔记111（2005）73-91www.elsevier.com/locate/entcs存储卡的轻量级规范测试：一个案例研究Seung Mo Cho和Jae Wook Lee1，2移动解决方案实验室，企业技术运营软件中心Shinsa-Dong，Kangnam-Ku，首尔，韩国摘要随着移动设备市场的扩大，开发可靠存储卡的需求也在增加。三星是存储卡业务的主要参与者之一，也在努力改进其存储卡产品的验证过程。为此，我们进行了一个试点项目，采用正式方法和基于规范的测试技术来验证我们的MMC（多媒体卡）系统。被测系统（SUT）是一个MMC卡，它用两种语言实现，Verilog for RTL和C for firmware。为了测试MMC卡，我们用Esterel形式化了MMC主机的完全通用的行为模型它也被用作测试预言机，以自动化SUT的测试。然后，在Seamless验证环境我们进行了基于网络的测试和随机测试。关键词：多媒体卡，基于规范的测试，Esterel，无缝1介绍我们的现代生活在很大程度上依赖于许多携带计算机的系统。手机是一个最明显的，也是最复杂的例子。一部手机的源代码有100多万行。还有许多其他的例子，如电烤箱，交通灯控制器，发电厂管理系统和汽车导航系统，具有不同的尺寸和复杂性。这些系统被称为嵌入式系统。1 电子邮件：seungm.cho@ samsung.com2电子邮件地址：rtos21@samsung.com1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.12.00874S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）73外部存储卡也是嵌入式系统。它们有自己的微处理器、内部总线，当然还有闪存。 随着各种移动设备的市场不断扩大，对外部存储卡的需求不断增加。存 储 卡 有 许 多 工 业 标 准 ， 如 SD 卡 ， 记 忆 棒 和 CF 卡 。多 媒 体 卡（MMC）[9]也是存储卡的规格之一。它已被许多供应商采用，包括三星，在PDA，数码相机，摄像机和MP3播放器领域。当三星开始生产MMC卡时，人们认为性能是最重要的问题。然而，很快就变得明显的是，可靠性也是在市场上取得成功的关键。营销部门的一位男士这样表示：“我们可以通过降低价格来销售低性能产品，但如果它们在插入时崩溃，我们就不能销售它们。”在本文中，我们提出了一个案例研究，我们进行了改善验证过程中MMC卡。我们提出了一种新的基于规格的存储卡测试方法，并将其应用于我们的MMC卡。存储卡系统形成嵌入式系统的子类别。它们也是通信系统，因为它们与PDA、手机和数码相机等主机接口。因此，存储卡系统的规范通常由两部分组成：底层硬件需求规范和主机与卡之间的通信协议规范。它们具有许多独特的功能，使其区别于典型的通信系统或嵌入式系统。• 通常，它们在专用硬件上运行。由于硬件和软件是共同设计的，硬件的设计决策对软件的设计有很大的影响，反之亦然。此外，硬件和软件都具有复杂的应用逻辑。这对于嵌入式系统来说并不普遍，在嵌入式系统中，使用现成的实时操作系统来减少软件和硬件之间的直接功能依赖。• 由于嵌入式系统往往会对安全或财务造成很大的危害，因此通常会非常小心地开发它们并投入大量资源。然而，存储卡并不被认为对安全或财务至关重要此外，市场迫切需要快速交付相对可靠的产品。• 与上述原因相关，存储卡系统的体系结构往往分层较差。例如，OSI7层参考模型被接受为分布式网络系统的标准体系结构。因此，提供每一层的供应商的多样性不会造成什么问题，因为他们的角色是S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）7375定义明确。另一方面，MMC的规范只定义了物理层、位和通信协议;不同的主机和卡供应商在硬件、固件和设备驱动程序之间使用不同的功能分离。根据这些特点，我们认为最好设计我们自己的基于规范的测试方法，而不是采用现有的方法。 我们建立了一个周期精确的模型MMC主机，显示完全一般的行为。其仅根据MMC的官方规格建立。它还使我们能够在主机模型中包含测试oracleMMC规范限制MMC卡的允许行为。主机模型也被用作测试预言机，因为它保持MMC卡的状态本文提出了一种方法，并进行了试点项目的结果。本文的贡献可以概括如下。首先，我们建立了一个新的轻量级[6]基于规范的测试方法，适用于存储卡。 我们的方法建立了一个正式的行为模型的环境，并从中派生出一个测试harness。[7]）或安全关键嵌入式系统（例如，[10]）。我们发现，存储卡的显著特征使我们的方法比现有的基于规格的测试方法更具吸引力第二，我们将MMC规范的环境部分正式化。这个规格乍一看似乎微不足道，但发现对主机和卡有几个复杂的要求。我们使用Esterel[1]形式化了MMC主机的周期精确行为模型.在形式化过程中，我们可以准确地理解规范中存在的一些歧义，也发现了规范的一些违规行为。第三，我们描述了我们的MMC卡的测试结果。 测试在商业平台Seamless上完成，Seamless是一种硬件/软件协同仿真工具[11]。由于速度问题和错误的再现性，实际测试是在仿真环境中进行的。由形式化模型产生的测试线束代码与MMC卡的硬件代码（用Ver-ilog编写）和软件代码（用C编写）相结合。我们将展示与蛮力随机测试相比，实验的有效性本文的组织结构如下。在第二节中，我们介绍了我们的工作背景。我们介绍MMC规范和Esterel。我们在第3节中提出了我们的框架和基本原理。在第四节中，我们简要介绍了MMC主机的建模方法测试结果将在第5.最后，对本文进行了总结，并提出了一些讨论和进一步的工作.76S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）732背景2.1MultiMediaCardMMC系统由MMC主机和MMC卡组成。主机是使用外部存储卡的设备，如数码相机、PDA或手机.它们通过三线串行数据总线（时钟、命令和数据线）连接它们之间的通信使用消息来执行，消息由以下令牌之一表示。• 命令是开始操作的令牌。命令从主机发送到MMC卡，并在命令行上串行传输• 响应是从MMC卡发送到主机的令牌，作为对先前接收的命令的应答。它在命令行上串行传输。• 经由数据线将数据MMC卡的主要功能是读取和写入数据。 数据通过两种方式转移：面向流的模式，其中主机应该解释停止数据传输流，以及面向块的模式，其中数据传输根据其大小在传输之前被定义的块来完成。我们考虑块导向模式在这里，因为许多MMC卡，包括一个由三星，只支持块导向传输。除了读和写命令之外，还有其他附加命令，如停止传输命令和设置块计数命令。与大多数工业规范一样，MMC规范主要用英语编写。它还包括许多图表和表格，为理解需求提供了很大帮助。状态图（如图1）用于显示MMC卡中的状态转换，时序图（如图2）用于描述时序要求。 然而，这些图表不足以完全解决模糊性或不完整性，因为它们不是用来定义需求，而是帮助理解需求。例如，有许多图表显示串行总线上令牌之间的时序关系。然而，很明显，所有可能的情况中只有一小部分被涵盖。MMC规范确定了卡在操作期间可以停留的11种状态。在每个状态下，卡接受来自主机的命令令牌，如果需要，发回响应令牌，执行所需的任务，并更改其状态。请注意，并非所有命令在每个状态下都是合法的。为3版权归MultiMediaCard Association所有。4版权归多媒体卡协会所有。S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）7377Fig. 1. 数据传输模式3的状态图示例图二. 读取多个块4例如，在写操作期间发送读命令被认为是非法的。然而，非法命令的后果也在规范中定义。当接收到非法命令时，卡应该忽略该命令，不发送任何响应。命令集分为几类，MMC卡只能支持其中的一部分。我们对SamsungMMC卡支持的15个命令的行为进行了建模。2.2EsterelEsterel[5]是一种支持同步编程范式的命令式文本语言。它通常用于编写并发性和确定性都成为重要问题的反应式系统。不同于常规78S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）73在Java等并发语言中，同步语言通过将并发程序编译成顺序程序，可以同时提供并发性和确定性因此，Esterel在开发反应系统的复杂控制自动机方面是非常有用的。给定一个Esterel程序，Esterel编译器生成一个实现自动机的C代码Esterel的执行模型是时钟驱动的。在每个循环中，自动机的反应然后，该函数处理输入信号，计算下一个要继续的状态，并向环境发出适当的输出信号。一个Esterel程序由许多与信号通信的模块组成。它们在每个周期中存在或不存在。它们也可以承载价值。语言构造分为两类：一类消耗时间，另一类是即时执行的。“瞬时”一词实际上意味着，与周期时间相比，执行在相对较短的时间内完成。第一类包括await，repeat-n-times，圆圈等来第二类包括赋值、C函数调用、发出等。Esterel有许多控制结构。基本的是顺序和并行组成。它也有一个抢占结构（陷阱），以中断程序块，并直接执行中断处理程序。有许多关于Esterel和同步编程的介绍性材料，其中我们推荐最多。3轻量级基于规范的测试：方法考虑到在引言中提到的MMC系统的独特性，我们得出结论，大多数现有的基于规范的测试的研究不能直接应用于验证MMC系统。我们将原因总结如下。• 通常，它们带有相当复杂的工具（例如，[3]）分析形式规格并生成测试用例。由于采用这些工具伴随着高昂的学习成本，它往往是不可接受的普通领域的工程师。此外，这些方法的有效性尚未得到充分证明。• MMC卡使用串行总线与主机连接。要求的形式类似于 因此，通信的基本单位是比特，而不是消息。现有的基于规范的方法大多是针对通信协议设计的，不能处理这种情况。S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）7379系统.我们认为，这个问题是由于MMC系统的架构中缺乏分层，如前所述。• 基于规格说明的测试的研究主要集中在开发测试生成方法上。然而，执行测试被认为是一个单独的问题。这是非常困难的，因为许多测试生成的研究不能完全解决的可行性问题。我们的方法旨在提供我们期望从基于规范的测试中获得的许多好处。它被认为是轻量级的，适用于资源有限的现实世界的问题。我们认为这并不太激进，不会被现场工程师所接受。图三. MMC系统图3是我们方法的概述。我们在Esterel中模拟环境。将其编译成C代码，作为Seamless仿真环境中的宿主模型.随机测试和基于MIMO的测试被用来验证系统在无缝（SUT）。我们展示了我们为设计方法所做的决定。3.1环境建模与大多数基于规范的测试方法相反，我们构建环境的正式行为模型，而不是SUT。在MMC系统的情况建模是使用80S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）73从MMC规范中获取信息，以便对MMC主机进行完全通用和完全不确定的模型。5我们假设MMC系统由环境和SUT组成，它们具有几乎相同的复杂性。假设环境和SUT目前都没有正式建模，我们要对它们应用形式化方法。毕竟，如果我们要从模型检查等形式验证技术中受益，我们需要对它们两者进行建模[4]。然而，考虑到这种情况，我们有两个选择，首先对它们中的哪一个进行建模。传统的形式化方法通常强调SUT模型。因此，基于规范的测试方法也假设SUT模型的存在，并为它们提出测试技术。因此，在文献中有一个默契，即用户需要首先将SUT形式化，以应用基于规范的测试。然而，经过仔细考虑，我们得出了一个结论，首先构建环境模型在许多情况下更合适，因为我们可以直接将它们用作测试工具。我们可以通过从模型生成命令式代码来利用宿主模型的可执行性，这些命令式代码可以与SUT的实际代码一起执行或仿真它还支持形式方法的轻量级应用[6]。由于许多行为建模语言都带有生成命令式代码（通常用C编写）的编译器，因此工程师的学习成本相对较小。此外，采用变得容易，因为生成的代码可以用于现有的测试过程。3.2语言：简体中文作为行为建模语言，我们选择Esterel[1]。它允许非常容易地描述复杂的、并发的、通信的状态机。选择Esterel的理由可归纳如下。• 它可以生成高效的C代码。许多特定语言支持代码生成工具。然而，在许多情况下，代码生成的主要目的是快速原型或模拟。相反，Es-terel应该直接用作实现语言，因此生成的代码非常高效。• 对于一般程序员来说，它很容易学习。虽然同步编程范式[5]可能是一个障碍，但具有一点硬件设计背景的程序员可以理解范式和语言5.当我们用SUT执行宿主模型时，通过随机选择解决了不确定性S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）7381轻易Esterel的命令式语法也很有帮助。• Esterel基于循环的执行模型适合与硬件描述语言结合使用。它还使硬件和软件的详细验证成为发送命令）。• 它是自由分发的。Esterel提供免费但功能强大的编译和调试工具。3.3测试环境：无缝实际测试在仿真环境Seamless上执行，该环境支持硬件和软件的共同验证[11]。缺乏硬件和软件之间功能分离的规范也导致了它们的组合测试。Seamless可以同时执行用C编写的软件代码和用Verilog编写的硬件代码由于SUT是卡，我们应该提供主机模型无缝仿真环境（图。3）。我们使用C代码编译从Esterel程序作为主机模型。3.4测试执行我们在Esterel中构建的主机模型是最大的不确定性，这意味着它生成所有可能的行为，而不与规范相冲突。但是，要解决模型的不确定性，使模型更好地用于检验目的.在我们的MMC主机模型中有几种不确定性。在一个状态中，主机应该确定：1）下一个要发出的命令，2）在收到响应后，在发送下一个命令之前要等待多长时间，3）要发送的数据令牌的数量，等等。它们对应于从一个状态的输出转换。我们使用两种方法来解决不确定性。第一种是使用预先定义的场景。已报告的三星MMC卡的一些错误被用作场景。二是随机模拟。我们提供Esterel代码与C代码，随机选择一个过渡在测试过程中，我们使用分支覆盖分析来衡量测试的完整性。我们在一个状态中记录所选的转换，并在测试完成后报告它们的覆盖结果请注意，我们不能提供100%的分支覆盖率，因为区间的范围和块的数量是无限的。由于发出具有不同数据值或不同延迟的命令会表现出不同的行为，82S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）73这些命令应该被认为是不同的转换。作为比较，我们使用预定义的区间集和块数进行测试。4MMC主机建模MMC主机模型使用Esterel和C代码构建。Esterel代码扮演控制自动机的角色，C代码提供数据操作和随机测试选择机制。4.1埃斯特雷尔码我们通过将功能仔细划分为模块并设计它们之间的通信来管理MMC规范的复杂性。大多数复杂性在于命令之间的交互规范。例如，主机可以在读取或写入数据期间发出许多命令，包括停止传输、取消选择卡、进入非活动状态、进入空闲状态等[9]。 因此，这些命令的模块应该相互作用，以正确处理这些情况。这套模块分为三组。下文将对此进行解释4.1.1主模块Esterel程序有一个唯一的主模块。它定义了系统的接口、配置和全局状态变化。图4显示了主模块的主体。它被一个循环包围，这意味着系统永远不会终止自己。循环体分为两部分。当控制处于第一部分时，卡正常运行，即没有任何违反规范的情况。一些模块通常由run命令实例化（第9-11行），但其他模块在另一个嵌套循环中实例化，abort-when构造（第14-16行）。 需要这种区别来处理CMD 0的软复位。模块CMD 00可以发出软复位信号，并强制模块重新启动其他命令。因此，模块CMD 00本身应该在abort-when构造之外一旦检测到违反规范，就会发出ViolationFound信号。第一个陷阱块（第3-18行）终止，控制转移到循环体的第二部分。现在我们发现了一个违规，我们应该通过发出CMD 0来重置卡以继续测试。S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）73831回路2暂停;3陷阱Reset_after_Violation in4every Violation_Found do5暂停;6退出Reset_after_Violation7结束每8||9运行CMD 00||运行||运行Dataline_Moniter||10运行CMD_REQ||运行Response_Receiver||11运行Data_Receiver||运行Data_Data12||13循环中止14运行CMD 01||运行CMD 02||运行CMD 03||运行CMD07||15运行CMD 09||运行CMD 10||运行CMD 12||运行CMD13||16运行CMD 17||运行CMD 18||运行CMD 23||运行CMD24_2517当Soft_Reset结束18结束陷阱;%Reset_after_Violation1920%发送CMD 0进行重置21陷阱CMD0_INIT22回路23运行CMD_REQ24||25[26暂停;27int maximum（0）; int maximum（0）;暂停;28等待48tick;29退出CMD0_INIT30]31循环结束32结束陷阱%CMD0_INIT33end%Loop-end见图4。主模块部分，MMC主机4.1.2接口模块MMC有两条串行通信线，CMD线用于命令和响应，DATA线用于数据传输。接口模块管理这些线路。他们扮演着包装的角色。解包）令牌从（分别位，通知其它模块令牌的到达/发送等。与无缝环境的接口也由这些模块处理。84S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）73例如，模块cmd snd负责在命令行上放置命令令牌。它调用Seamless提供的API函数，以模拟在接口线上写入一些数据图4中的第9-11行显示了这些模块的实例化4.1.3命令模块MMC规范定义了许多命令。在我们的MMC主机模型中，每个MMC命令都由一个模块表示，该模块在处理该命令期间管理通信的控制当发出命令令牌时，负责全局调度的模块（图4的第9行）发出指示该命令开始的信号mand.然后，相应的模块注意到它并开始适当的处理。作为一个例子，我们展示了一个适度复杂的模块。在附录A中，我们给出了处理CMD 18（读取多个块）的Esterel代码，以显示模块之间的交互示例。图2中CMD 18的时序图有助于理解CMD 18的行为。CMD18用于从MMC卡读取多个数据块。在发出CMD 18之前，应通过其他命令设置要读取的块数和块的长度。在接收CMD 18时，卡开始通过DATA线发送数据块。传输可以通过多种方式终止，例如接收到所有指定数量的块，发出停止传输命令或发出卡重置命令。CMD 18只能在传输状态（TRAN）下执行。当卡在状态TRAN接收CMD 18时，它将其状态改变为发送数据状态（DATA）。在完成传输之后，它返回到状态TRAN。请参阅图1，图中显示了数据传输模式的状态图附录A中CMD 18的模块中，6行10-52为主体。循环结构意味着每当CMD18被发布时，这个主体就应该开始。第11-16行扮演等待CMD 18的角色每当发出一个如果是，则通过退出陷阱（第14行）退出每个循环。当在TRAN状态下发出命令时（第18行），执行第19-50行。它由两个线程组成，分别处理CMD行（第20-33行）和DATA行（第36-48行）。我们使用两个线程，因为读进程可以通过几种方式终止。第二个线程（第36-48行）用于处理正常传输。它接收预定数量的数据块（第38-42行），并发出一个信号状态改变（TRAN），以指示传输结束。6声明信号和变量的行被省略。S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）7385然而，在所有块被传输之前，还有其他方法来结束传输。第28-31行表示信号状态改变（TRAN）可以终止传输的方式。注意，信号状态改变（TRAN）也可以由其他模块发出。CMD 12（停止传输）任务）还发出该信号以指示中止正在进行的传送。因此，第28-31行实际上处理两种情况：正常传输终止和停止命令终止。另一方面，第一个线程在收到信号结束响应时宣布状态变为DATA状态（第20-21行）。信号结束响应由负责将CMD线上的位组装成响应令牌的模块发出。以这种方式，模块与卡和其他模块接口4.2C代码像一般的Esterel程序一样，我们的主机程序需要C函数来进行数据操作。我们解释几个重要的功能。• 函数selectnext用于选择下一个要执行的命令，并决定主机在收到上一个命令的响应后，在发出命令之前要等待多少个周期。在基于场景的模式下，选择是由预定义的场景完成的，它是一个列表命令和延迟的组合在随机执行模式中，随机地做出决定。然而，不同的权重被赋予命令以反映现实。例如，复位命令CMD 0被赋予低权重，以便测试足够长的命令序列。• 函数更新覆盖率具有计算分支覆盖率的作用。覆盖率被用来衡量测试的完整性。每当发出命令时，都会调用它。• 定义了许多函数来处理与Seam-less的实际接口（参见图3。）5实验使用我们上面描述的主机模型，我们在无缝环境中测试MMC卡。正如许多形式方法的倡导者所断言的那样，建模过程本身被揭示为在非正式规范中清除歧义的有效手段。例如，图3具有触发条件为“操作完成”和“传输完成”的转换。然而，确切地说，86S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）73该等术语的定义并未在说明书中直接给出。在建模过程中，我们必须通过仔细阅读规范并与领域工程师讨论来定义这些触发条件的确切含义建模完成后，我们对被确定为兼容性问题的场景进行了实验。它们是通过对具有物理MMC主机的MMC卡进行实际测试而发现的识别的场景被建模为MMC命令序列，其中延迟与每个命令相关联。（0， 8000），（1， 200），（2， 200），（3， 200），（7，64），（24， 8）例如，上述场景包括6个MMC命令。列表中的每个元素都是命令和延迟的一对;在主机收到之前发送给卡的CMD3我们收到了一组三个兼容性问题的命令序列的形式从域工程师。然而，它们我们能够通过测试各种延迟来填补缺失的这表明基于仿真的测试是强大的，因为它可以实现MMC卡的周期精确测试。我们亦发现其他被识别为违反法定规格的个案例如，当我们在写操作期间发送非法命令时，数据线上的CRC位在某些条件下会变得异常。我们在随机测试中发现了四个异常情况。当我们报告我们的发现时，领域工程师的反应通常是愤怒的表情，而不是惊讶。他们问我们为什么要考虑这些奇怪的情况。当然，我们提供的好答案是，已经发现的兼容性问题的大多数原因看起来也很荒谬，除非它们是真实的。在大多数情况下，我们无法理解为什么主人的行为如此奇怪。但是，应该支持主机的任何不违反官方规范的行为。因此，防止未来错误的正确方法是尽可能地符合具体6结论在本文中，我们介绍了一个轻量级的基于规格的测试方法的存储卡系统。我们建议从MMC的官方规范中构建通用MMC主机的周期精确行为模型，并将其用于联合仿真环境，而不是使用许多真实的MMC主机设备进行测试我们能够在模拟器上重现错误场景，发现这有助于调试错误。测试方法使用S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）7387正式模型还发现了一些以前未知的违规行为，这些违规行为没有得到很好的处理。我们的方法在理论上不那么优雅，也不那么新颖。然而，我们相信它可以直接使许多与我们面临类似问题的工程师它可以集成到现有的测试过程中，几乎没有负担。使用形式化建模语言是一种简单而有效的方法来精确地实现测试工具。Esterel的学习成本被认为是可以接受的，特别是与其他重型建模语言（如UML）的兼容性。我们的一个工程师，他有硕士学位。电子工程学位，只有C编程经验，可以在一周内学会语言及其背后的范式。Esterel的可视化仿真和调试环境有助于快速建立主机模型。然而，我们也发现了一些困难，在进行该项目如下。• 虽然Esterel的仿真环境xes在单机调试方面表现出色，但它不能很好地与其他工具（如Seamless）集成。例如，要使时间进度是可能的，只有通过点击'tick'按钮在模拟器中。如果有模拟点击的API，xes可以与Seamless环境结合使用。我们认为添加API• 同时仿真硬件和软件所花费的时间比我们预期的要多得多。例如，MMC卡模型（用Verilog编写）在上电后大约需要10分钟才能开始正常工作，通过存储和恢复仿真状态可以部分解决该问题。我们听说即将推出的Seamless版本将通过将Verilog代码翻译成C来解决这个问题。我们相信这将大大缓解速度问题。存在用于验证嵌入式系统的专用商业工具。其中两个已经达到了明显的工业接受水平：Verisity的Specman [15]和Synopsys的Vera [12]。我们有机会将我们的方法与Specman的方法进行比较。它使用他们专有的建模语言e，以及一组用于建模和执行验证的工具。约束求解器使建模人员能够编写带有实际数据值约束的参数化测试场景。覆盖率分析器在执行一组测试之后报告完整性程度。在我们的框架中，这两种工具都有一些原始的形式，但都是以一种相当特别的方式。虽然使用这些专用工具在许多情况下似乎富有成效，但我们88S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）73认为开放的，而不是专有的语言，如Esterel有自己的好处。首先，我们不需要依赖于特定的工具供应商。此外，我们可以从Esterel免费提供的其他分析工具中受益，例如模型检查器Xeve[2]。有一些方向值得进一步研究。• 现在我们有了MMC主机的正式模型，我们可以进行正式的验证，例如模型检查。最大的挑战可能是建立MMC卡的模型。这将比构建主模型困难得多，因为模型应该反映具体产品的足够细节。然而，如果Seamless的下一个版本提供了将Verilog代码抽象为C代码的功能，那么建模任务将变得非常容易。• 将我们的方法的测试结果与其他现有的基于规范的测试方法的测试结果进行比较将是有趣的。为了做这个实验，我们也需要建立MMC卡的模型。但是，在这种情况下，模型将使用来自规范的信息来构建我们不认为这是困难的，因为主机和卡的行为之间存在二元性• 我们在Esterel中构建主机模型的方法可以结合到SystemC[13]框架中。SystemC正在迅速成为SoC系统的系统级设计的事实上的标准语言。SystemC设计的测试平台通常也是用SystemC编写的。然而，我们的经验似乎表明，由于其强大的控制结构，Esterel比SystemC更合适。我们计划将我们的方法应用到系统级设计的MMC卡时，设计将可用。• 在第5节描述的实验中，我们发现没有标准语言来指定嵌入式系统（如存储卡）的测试用例因此，工程师应该从头开始编写他们的测试平台，使用通用语言，如Verilog或C。这种情况对于通信系统是不同的，其中TTCN[14]被认为是描述测试用例的标准语言。使用TTCN的验证工程师可以专注于测试用例的逻辑正确性，而不必关注无关的细节。我们坚信，嵌入式系统的测试语言将减轻该领域验证工程师的负担S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）7389确认作者要感谢Mentor Graphics，特别是Seok Man Jung和Soo Yong Lee为我们使用无缝CVE提供了宝贵的支持引用[1] Berry，G.：Esterel语言入门，版本v5.91。ftp://ftp-sop.inria.fr/esterel/pub/papers/primer.pdf[2] Bouali，A.：Xeve：一个esterel验证环境，在第10届计算机辅助验证国际会议上，第1427卷。LNCS，1998年。[3] 布斯凯湖Ouabdesselam，F.，Richmond，J.- L.，Zuanon，N.：Lutess：一个规范驱动的同步软件测试环境。第21届软件工程国际会议，ACM出版社，1999年5月，267[4] Burch，J.R.，克拉克，E.M.，McMillan，K.L.，Dill，D.L.，和Hwang，L.J.：符号模型检查：1020个状态及以上。第四届计算机科学逻辑年会论文集，1990年[5] Halbwachs，N.：反应系统的同步编程（一九九三年）[6] 杰克逊，D。Wing，J：轻量级形式化方法，IEEE计算机，1996年4月[7] 贾加德桑湖J.，Porter，A.，Puchol，C.，Ramming，J.C.， Votta，L.G.：反应式软件的基于规范的测试：工具与实验。软件工程国际会议论文集，1997年[8] Malaiya，Y.K.，Li，N.，Bieman，J.，Karcich河，Skibbe，R.：测试覆盖率和可靠性之间的关系。第五届软件可靠性工程国际研讨会论文集（1994年）[9] 多媒体卡系统规范，3.1。MMCA技术委员会，http://www.mmca.org/tech/tech.html[10] Paleska，J.：安全关键系统的测试自动化：工业应用和未来发展。欧洲形式方法会议FME 96（1996年）[11] 无缝硬件/软件协同验证，http://www.mentor.com/seamless。[12] Synopsys，http://www.synopsys.com/[13] SystemC，http://www.systemc.org。[14] IS O/I EC9646- 3：1998，第3部分：T r eeandTabularCombinedNotatin。[15] Verisity，http://www.verisity.com/[16] 张，L.，Luo，X.，Chen，M.：考虑到测试配置文件的随机和分区测试的比较。测试与评估杂志，2013年，第31期。第2条（2003年）90S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）73读取多个块1模块18： %% CMD 18： READ_MULTIPLE_BLOCK2%%信号定义：由于空间限制而3function CMD07_is_mine（integer）： boolean;4函数get_number_blocks（）：integer;56varcmd： integer，7nn：整数8在9陷阱E10回路11陷阱T（以%为单位）等待CMD 1812每个end_cmd都13cmd：=？end_cmd;14如果cmd = 18，则退出测试结束15端16端捕集器;17陷阱停止18如果（？state_changed）= TRAN，则%法律命令19[%此线程处理总线的 CMD线20wait_end_response;21emit state_changed（DATA）; % 现在，主机正在读取数据22回路23等待24case end_cmd do25如果（？end_cmd = 7和（不是CMD07_is_mine（？end_cmd_arg）26还是？end_cmd = 15然后退出停止27endif28case state_changed do29如果？state_changed = TRAN，则传输结束百分比30退出已停止31endif32结束等待33末端回路3435|| % this thread deals with DATA line36int n：= int n（）;37陷阱LoopTin loop38中止39wait（NAC * 10）tick;40E出口41when start_data;42wait_end_data;43nn：= nn- 1;44如果nn = 0，则退出LoopT end，如果45末端回路46端捕集器;47暂停;48发射状态改变（TRAN）四十九]50endif51末端陷阱停止%S.M. 赵振英Lee/Electronic Notes in Theoretical Computer Science 111（2005）739152末端回路53手柄E do54持续违规_发现55末端陷阱56末端变量57端模块