自动检测无法达到的覆盖目标和生成“极端情况”场景的测试

理论计算机科学电子笔记116（2005）199-211www.elsevier.com/locate/entcs通过回溯模型检查器反例A. Fantechi1，2Dipartimento di Sistemi eInformaticaUniversit`adegliStudidiFirenze Firenze，ItalyS. Gnesi1，3ISTI-CNR意大利比萨A. Maggiore马焦雷1，4AltraVeri fica Ltd，英国摘要自动检测无法达到的覆盖目标和生成“极端情况”场景的测试对于使基于测试和模拟的验证更加有效至关重要。在本文中，我们解决的问题，覆盖性分析和测试用例生成模块化和组件为基础的系统。我们提出了一种技术，给定一个未覆盖的分支在一个组件中，要么建立该分支不能被覆盖或产生一个测试用例，在系统级，覆盖该分支。该技术是基于使用模型检查器返回的反例，并利用组合性来处理实际应用中典型的大状态空间关键词：可覆盖性分析，测试，模块化，基于组件的系统，组合性1这项工作得到了意大利大学和研究部在COFIN 2001项目2 电子邮件地址：fantechi@dsi.unifi.it3 电子邮件地址：gnesi@isti.cnr.it4电子邮件：adriana@altrave ri fic a. COM1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.077200A. Fantechi等人理论计算机科学电子笔记116（2005）1991介绍代码覆盖率指标，如语句覆盖率和分支覆盖率，主要用于软件和硬件设计的基于测试和模拟的验证，以衡量验证的进度，并确定需要进一步测试的设计区域。代码覆盖度量报告在仿真期间未执行的设计区域。这些也将包括代码的部分是无法访问的。基于模拟的验证的一个共同目标是实现100%的合理分支覆盖率。手动识别代码中无法访问的部分或为“corner-case”场景生成测试用例通过自动和可靠地确定覆盖目标（如控制流程中分支的覆盖）是否可实现，验证过程变得更加有效。这个过程是可覆盖性分析的主题[13]。一个典型的情况是，当无法达到的目标是组件运行的环境对组件施加的约束的结果时，就会出现无法覆盖的目标在本文中，我们提出了一种方法的覆盖性分析和测试用例生成未覆盖的分支在系统级的基础上使用的反例返回的模型检查器，利用组合性，以应付大的状态空间典型的实际应用。反例是基于模型检验的形式验证的最有用的结果之一[3]，并已被广泛用于诊断系统模型中检测到的问题。这里使用了一个更丰富的反例概念，即“反例自动机”的概念本文的结构如下。第2节一般性地介绍了所提出的技术。第3节介绍了我们的建议中使用的框架（形式主义，逻辑和工具），并通过一个例子描述了法 然后在4中讨论该方法的复杂性。2拟议方法2.1基本原理我们提出的方法来检查覆盖性，并从系统的未覆盖分支导出测试用例是基于以下原则。• 我们假设系统可以被建模为有限状态标记转换系统（LTS）[12]，并且测试过程能够通过适当的工具提供覆盖度量和关于非状态的信息。A. Fantechi等人理论计算机科学电子笔记116（2005）199201覆盖的树枝• 从每一个未覆盖的分支开始，我们建立一个时序逻辑公式来表达“未覆盖的分支永远无法到达”的属性• 我们将模型检查器应用于对系统建模的LTS，以检查模型上给定的时态逻辑公式：如果返回TRUE，则无法覆盖分支。• 否则，我们要求模型检查器提供一个反例，这是一个执行未覆盖分支的路径：这个路径包含执行它所需的输入信息-也就是所寻找的测试用例。2.2组合性然而，这个看似简单的过程由于实际应用具有非常大的状态空间而变得复杂，因此模型检查很快变得不可行。我们提出的方法利用组合性来解决这个问题，如下所示。• 我们假设系统是由一系列模块组成的（见图1），并且我们要处理的未覆盖分支可以定位在内部模块S0中。请注意，这个假设比乍看起来的限制要少：实际上，一个组件与通过将更多的组件分组在单个模块中，可以根据该说明将更复杂的结构分割成模块（这就是为什么在下文中我们称之为• 我们将第2.1节中描述的过程应用于模块S0，获得一条路径，该路径显示模块需要哪些输入来执行未覆盖的我们假设S0的输入作为输出来自前一个模块S1。• 从S1的输出序列中，我们详细阐述了一个时序逻辑公式φ1，它表达了这样的性质：• 我们在模块S1的模型上应用模型检查器来检查公式φ1：再次，这应该返回（如果不是，再次，S1的输出序列是不可行的，因此S0中的未覆盖分支不可达）。• 我们要求模型检查器给出一个反例。 这个反例是S1的一条路径，它给出了执行S0中未覆盖分支的输出序列。此路径还包含有关执行它所需的输入的信息。202A. Fantechi等人理论计算机科学电子笔记116（2005）199• 系统被构造成一个模块链，每个模块为下一个模块产生输入，并接收前一个模块的输出，我们可以对遇到的每个模块重复上述过程在Sn上产生的最终反例实际上是模块Sn的接口的所寻找的测试用例，当作为输入给Sn时，它会导致中间反例作为输入给下一个模块，这最终导致S0中的未覆盖分支被执行。SnSN-1...S2S1S0Fig. 1. 模块链2.3应对错误的反例可能的情况是，由上述方法针对给定模块返回的单个反例迹不对应于链中的前一模块的任何可行路径。这并不意味着不存在覆盖未覆盖分支的测试用例。实际上，模型检查器已经产生了一个反例跟踪，该跟踪在前一个模块提供的输入序列下不可执行。因此，我们不需要提取一个反例，而是提取所有可能的反例迹：实际上，可能的反例迹的数量可能是无限的。因此，我们对可能的反例的有限表示感兴趣，这将我们引向“反例自动机”的概念一个LTSA和一个公式φ的反例自动机是一个自动机，它识别A上φ作为下一步，我们需要从反例自动机中提取一个公式，表示在下文中，我们也将该公式称为在这一点上，我们可以通过模型检查下一个模块来满足这个反例公式，以获得一个新的反例自动机，然后为下一个模块获得一个新的反例公式，依此类推，重复这个过程，直到我们到达系统的边界，即最后一个模块，任何线性反例都提供了一个测试用例，这是所需的测试用例。这个案例是用来直接测试整个A. Fantechi等人理论计算机科学电子笔记116（2005）199203模块链，它将覆盖最初未覆盖的分支。2.4整个测试用例生成过程总体方法可以通过以下过程来描述，其细节将在下一节中通过运行示例并参考特定的建模形式主义和验证环境来讨论。我们假设一个链结构，如图1所示：Gi是Si和Si+1之间的公共动作集。φi是在第i因此，φ0测试用例生成的过程如下。过程testcasegen（φ0，S0）如果MC（φ0，S0）=真，则“不可行路径”，否则AC0：=AC（φ0，S0）φ1：=FCG0（AC0）对于i：= 1，n，如果MC（φi，Si）=真，则“不可行路径”，否则ACi：=AC（φi，Si）/Gi−1ACi−1ifi/=nthenφi+1：=FCGi（ACi）“ACi的任何路径都是系统的测试用例其中，以下为辅助操作员：• MC，该模型检查LTS上的公式，给出布尔结果• AC，它从公式和LTS计算反例自动机• FC，在一组通信动作上索引，其相对于给定的一组动作计算LTS的特征公式• A/GB，一个索引同步操作符，用于过滤虚假的反例。204A. Fantechi等人理论计算机科学电子笔记116（2005）199？？？BBB？一？B？C？C？B？e？？CC？D？D？？ee？一？D？？？一一一3JACK方法的可行性在下文中，为了展示该方法的可行性，我们通过将其应用于一个运行示例来描述该方法的步骤，该示例是采用集成验证环境JACK [1]5中包含的编辑工具和显式模型检查器AMC开发的。因此，我们从JACK继承了描述模型的形式主义（Labelled转换系统）和可以描述属性的逻辑，即ACTL（基于时间的计算树逻辑）[7]，它是分支时间时态逻辑CTL [3]的基于动作的版本。3.1标签转换系统我们使用标记转换系统（LTS）和LTS网络的图形符号，这些符号在JACK中继承自Autograph [14]。LTS的示例如图2所示。LTS的初始状态由双圆表示，并且标签与表示LTS的转变的边缘相关联。图二. 示例自动机的图形化规范（Mod0）为了表达两个LTS之间的同步通信，我们使用网络的图形符号（图3）。用方框5有关环境的详细信息，请访问http://fmt.isti.cnr.it/fmt-tools.htmA. Fantechi等人理论计算机科学电子笔记116（2005）199205说是一个网络，边境口岸是它的连接点。盒子实际上是LTS的抽象。如果两个网络在同一级别绘制，则它们可以通过链接相应端口执行的操作进行同步。在这种情况下，在链接的端口上执行的动作不再是可观察的，并且当它们被执行时，静默τ？F图三. 的示例网络3.2逻辑在下文中，我们使用ACTL逻辑的子集（基于时间的计算树逻辑）[7]，其是分支时间时序逻辑CTL [3]的基于动作的版本。这类配方：“未覆盖的分支永远无法到达”和“不存在具有由反例自动机识别的动作序列的路径”可以在该ACTL子集中定义。限制这些类型的公式允许反例本身的概念和反例自动机以更准确和有效的方式定义。我们可以观察到，我们感兴趣的所有公式都是这样的：φφ，其中φ是否定算子，φ是存在公式。因此，我们将使用的计算公式：：=φ：：=φ|φ|EX{ act }φ| EGφ| EFφ| E[ φ { act } U { act } φ ]|E [φ{act}U{act}φ]φ公式形成ACTL的正存在片段的子集，包括命题析取和蕴涵，EX存在下一个算子（我们参考[7]中关于前面算子的形式定义。由于我们只在公式的开头使用否定，反例实际上是可以看出，所有类型的公式，当不满足于LTS时，！！一一？gMod1！！BB！C？？HH！！DD？一？？bbMod0？C？？DD？？ee206A. Fantechi等人理论计算机科学电子笔记116（2005）199？h？？GG！！BB！！一一！！一一！C！！BB？？FF？？FF！！BB！！！CCC！！DD！D！e允许线性反例;相应地，φ公式，当满足LTS时，允许线性见证。3.3测试用例生成示例我们通过一个简单的例子来展示整个测试用例生成过程，这个例子是由两个模块组成的系统，如图3中的网络所示。模块Mod0和Mod1分别由图2和图4中的LTS定义。见图4。 模块Mod1我们假设一个测试活动还没有覆盖到由动作标记的分支？e，（之后？a和？b）在Mod0中。我们通过在未覆盖的分支之后添加一个转换来修改Mod 0的LTS，标记为fresh action！k（图5，左侧）属性：k}真应用模型检查器AMC在Mod0上验证此公式，我们得到了预期的否定答案。然后我们为公式EFEX{！k}为真。 一个LTSA和一个公式phi是一个自动机，它可以识别所有有限线性的语言。A上的phi的见证人。从模型检查器产生的状态的标记中提取见证自动机的算法，工作在A. Fantechi等人理论计算机科学电子笔记116（2005）199207图五.在Mod0中标记未覆盖的分支。 −反例自动机AC0标记由显式模型检查器在φ的成功检查期间计算，并且通过访问由φ的子公式标记的A的状态空间的部分来继续;访问由公式本身的结构分析驱动，因此当到达公式的叶子时，它被终止（注意，对于所使用的逻辑，叶子总是真正的子公式）。如果需要，如果φ中的动作序列与A中的循环匹配，则A被展开。访问是通过递归的深度优先搜索来实现的。因此，我们得到的自动机AC0是公式的反例自动机：k}为真，如图5所示。我们现在需要提供一个公式来表达“不存在具有由反例自动机识别的动作序列的路径”。这可以通过给出自动机的特征公式来实现[2，15]，即完全描述自动机本身的公式。实际上，我们只需要特征公式的存在部分，我们采用[9]中所示的方法，利用隐不动点的概念给出ACTL特征公式，它不需要显式的不动点算子。回到我们的运行示例，从自动机AC0我们导出公式FCG，其中G=（a，b，c，d，e）：<<！a>>！b>>（！e>>true）|(EG（EX{！c} true =>（EX{！{\fnSimHei\bord1\shad1\pos（200，288）} d>>！e|！c>>true）其中<>用作以下的简写：E[true{！第一幕！第二&幕&∼208A. Fantechi等人理论计算机科学电子笔记116（2005）199？？FF！！BB？？GG！！一一！B！C！！！DDD！eFF！动作n}U{act}φ]在第二步中，我们将模型检查器应用于Mod1 LTS和公式：~！a>>！b>>（！e>>true）|(EG（EX{！c} true =>（EX{！{\fnSimHei\bord1\shad1\pos（200，288）} d>>！e|！c>>true）然后我们得到反例自动机AC1（图6）。见图6。反例自动机AC1反例自动机AC1显示了一个循环！B、？f行动，这将对应于一个周期？b在Mod 0上，这是不可行的;只有一个？b动作实际上由Mod0在该点执行。这意味着AC1产生了应该避免的错误反例这种现象是由于这样一个事实，即在ACTL中，如果不使用状态公式，就不可能在路径上断言一个复杂的公式，每个公式都应该单独量化。因此，不可能表达“存在一条具有复杂行为的路径”类型的谓词，而只能表达“存在一条路径，它在简单行为之后达到一种状态，从该状态存在一条路径......"。这意味着当计算特征公式时，我们引入了虚假的迹线。为了消除这种错误的反例，我们应该只考虑AC1的路径对应于AC0的路径。该操作实质上是AC0和AC1之间对公共动作的同步操作。我们将使用符号AC1/GAC0来进行这个操作，其中G是公共动作的集合，在我们的例子中是（a，b，c，d，e）。实际上，在这个操作之后，我们仍然需要删除所有没有以final状态结束的终止分支。如果在示例中完成了这一操作，则该操作将生成图7中表示的自动机。所得到的反例减少到路径？g;！a;！b;！c;！d;！e. ，从中我们提取的输入序列形成的只有？g，这是我们要找的测试注意，在第一步产生一个线性反例A. Fantechi等人理论计算机科学电子笔记116（2005）199209∗∗∗∗？G！一！B！C！D！eFF见图7。自动机AC1/GAC0而不是反例自动机AC0，可以产生在年底的路径：？g;！a;！b;！这实际上是最短的反例，但在Mod1 LTS中是不可行的。这个过程可以重复，只要我们有模块连接在链条;对于每个中间模块，应该计算反例自动机和公式，并且应该在下一个模块上检查后者。对于最后一个模块，反例自动机，一旦错误的反例被过滤掉，就定义一组测试用例，每个测试用例覆盖最初未覆盖的分支。4程序的复杂性以下元素加起来增加了该过程的计算复杂性：• 模型检验（MC）与状态空间大小乘以公式长度（即运算符的最大嵌套• 特征公式（FC）的长度与子的大小成线性关系.线性以及特征公式生成的复杂性;• 自动机同步（/G）的复杂性至多为自动机大小的乘积，这里它适用于两个连续的反例自动机;• 反例自动机（AC）往往很小，因为它们会生成新的测试用例：如果我们假设该方法仅在“最简单”的测试用例已经被执行并且只有“角落案例”的测试用例还有待发现时才被应用• 无论如何，模型复杂性都是从组合角度进行攻击的因此，复杂度的阶数是n m c，其中n是链中模块的数量，m是模块的（平均）状态空间，c是反例自动机的（平均）状态空间。注意，这可能比n m m好得多，因为反例自动机的维数通常很低，特别是对于210A. Fantechi等人理论计算机科学电子笔记116（2005）199可以使用两个连续模块的显式同步来定义上述过程的替代方案。我们声称，这两个，使用的特征公式加模型检查的过程具有最小的复杂性，实现基于显式状态空间枚举。5结论和进一步工作我们已经使用一个运行的例子详细介绍了所提出的方法，以及特定的形式主义和验证工具。尽管如此，我们认为，这一办法具有普遍的有效性。工作正在进行中的方法都使用显式模型检查（如本文所示）和基于BDD的符号模型检查的实现，但仍然集中在LTS和基于动作的时态逻辑。然而，似乎合理的是，该方法与基于状态的形式主义（KripkeStructures）和基于状态的时态逻辑（如CTL）一起工作。这需要验证：反例、见证和反例自动机的定义实际上对所使用的逻辑和模型的假设高度敏感。与我们的工作相关的一个结果是为Kripke结构和CTL定义了更有表现力的树状反例;这些反例被用作指导精化技术的支持[5]。与我们的方法的主要区别是，树形反例是在其整体上证明公式是无效的。我们的反例自动机给出了所有线性反例的集合，每个线性反例都可以单独作为传统的反例。树型反例的最新发展是证明类反例[11]，用于提取模型上公式不满足的证明。与我们的方法更接近的是[6，10]的多个反例生成，它生成给定长度的所有反例，表示为用二进制变量的可能值注释的单个反例迹。引用[1] A. Bouali ，S. Gnesi ， S. 拉 罗萨JACK 环 境的 集成 项目 。 EATCS 公 告，n 。 54 ，October，1994，pp.207-223.[2] M.C. Browne ， E.M. Clarke ， O. Grumberg ： Characterizing Finite Kripke Structures inPropositional Temporal Logic，Theoretical Computer Science，59（1，2），1988，pp.115-131[3] E.M. Clarke，E.A. Emerson，A.P. Sistla.使用时序逻辑规范的有限状态并发系统的自动验证。ACM Transaction on Programming Languages and Systems，vol.8，n.2，1986，pp.244-263。[4] E. Clarke，O. Grumberg，K. McMillan，X.赵，符号模型检验中的反例和证明的有效生成，第32届设计自动化会议，DACA. Fantechi等人理论计算机科学电子笔记116（2005）199211[5] E.M. Clarke，S. Jha，Y. Lu，H.维斯模型检验中的树型反例。第17届IEEE计算机科学逻辑研讨会（LICS'2002），pp。十九比二十九[6] F. Copty，A.伊伦岛Weissberg，N.克洛普湾卡姆希在正式验证环境中的有效验证，CHARME'01，LNCS 2144，pp。275-292，Springer-Verlag，2001。[7] R. De Nicola，F.W.凡德拉格转换系统的动作与基于状态的逻辑。 Proc. Ecole de Printempson Semantics of Concurrency ， Lecture Notes in Computer Science vol. 469 ， Springer ，Berlin，1990，pp.407-419[8] A. Fantechi，S.格内西湾里斯托里反例和见证自动机ISTI技术报告，2004年。[9] A. Fantechi，S.格内西湾里斯托里在基于动作的逻辑中建模过渡系统。IEI技术报告，1996年。[10] M. Glusman，G.Kamhi，S.马多尔海姆河Fraer，M.Vardi，Multiple-CounterexampleGuided Iterative Abstraction Refinement：An Industrial Evaluation。TACAS 2003，LNCS2619，pp. 176-191，Springer Verlag，2003。[11] A. Gur Finkel，M.你好证明类反例，TACAS 2003，LNCS 2619，pp. 160-175，SpringerVerlag，2003.[12] R.米尔纳通信和并发。Prentice-Hall International，Englewood Cli Clens，1989年。[13] G. Ratzaby，S.乌尔河吴明，基于符号模型检验的可覆盖性分析，北京：计算机科学出版社，2001。[14] 罗伊河德·西蒙1990年，《计算机辅助验证研讨会论文集》，LNCS 531，65-75[15] B.陈志文，“特征公式”，第16届国际计算机科学大会论文集，计算机科学讲义，第372卷，第723 -732页，1989年。