英语原文共 6 页，剩余内容已隐藏，支付完成后下载完整资料

基于符号执行的机器学习自动生成测试用例模型

摘要 - 我们在本文中提出了一种基于符号执行技术的模型，旨在生成软件测试用例。为了使模型自动执行，我们使用一种使用机器学习算法构建的模型的确定性有限自动机（DFA），该算法将复杂模型视为黑盒子组件，其行为被推断。由于以这种方式获得的DFA可能是非常相似的，因此，允许在原始模型上不被允许的自动搜索，使用由不可行路径构成的反例来细化抽象。使用DFA状态和转换的系统覆盖来实现对比的计算，产生在模型上重复的测试序列，为离线测试提供测试用例或旨在抽象细化。

关键词：符号执行 约束求解 机器学习 抽象细化

1. 绪论

在以模型为基础的测试的背景下，各种方法都涉及和使用到基于状态转换的系统的图形的形式化，例如有限状态机或（IO）LTS。相反，其他方法将文本描述视为广义替代的模型，例如B或更简单的前/后置条件形式。 在许多情况下，文本模型首先变成一个图形，然后使用专用算法（如过渡巡视），或者使用条件限制符号执行的测试目的进行探索。

在本文中，我们专注于B机器的测试生成。我们的主要目标是改进现有的两种基于独立算法的主要测试用例生成方法。一方面，Leirios测试发生器使用一种结构覆盖标准，旨在覆盖系统的运行，采用经典的Wi-Fi盒测试生成技术。然后，它对模型状态进行即时的探索，以构建测试用例，因此生成的测试用例较短。另一方面，ProTest在有限状态机上使用状态检测算法代表系统可达到的状态，通过自动化模型计算并列举所有状态。我们的目标是提出一种方法，结合LTG的模型覆盖标准与状态检测算法这两种世界上最好的技术，通过增加测试前代码中的多样性来提高可以产生的测试质量。

当对大型系统进行处理时，这个枚举是会耗费大量的时间，而且需要象征性技术或近似处理，才能是被检测的代码数量减少到易处理的范围。以模型为基础的符号执行救赎使得可以通过用符号变量替换操作参数来探索潜在的大状态空间，这些变量创建符号状态，测试将自动执行。虽然对于给定的操作序列来说是有效的，但由于符号状态包含的检测需要复杂的约束求解机制，因此可能会大大减慢计算速度，因此几乎不能用于构建状态机。

系统的抽象画被广泛用来消除不重要的细节来得到简单的模型。然而，抽象系统的引入损失精度，并可能会产生虚假的执行（可以在抽象系统运行而不能在原系统上运行）。为了获得更好和更精细的抽象化系统，引入了Counter Example Guided Abaction Refinement的范例：从一个抽象系统和一个反例，一个无法执行的路径由更精细的抽象系统产生。这种方法在许多情况下得到成功应用，如符号模型检测和重写分析。

机器学习通常用于从黑盒子组件中提取FSM。 基本思想是通过使用其可能的输入数据来查询系统的运行状态，并推断确定性有限自动机（DFA）。 在这些算法中，生成的机器可能不正确w.r.t. 系统的行为，并且需要通过考虑由oracle提供的能够确定两台机器的等价性（即，假定oracle知道SUT）的反例来改进。 这种技术已经在组件的黑盒测试的背景下进行了实验。

我们在本文中提出，通过将这些机器学习方法与以模型为基础的符号执行相结合来适应这些机器学习方法。 我们的目的是推断一个提供B模型抽象的DFA，从中可以使用经典的图形覆盖算法来计算测试用例。 该方法的基本思想是基于生成的模型生成序列。 所有成功的测试序列（即在模型上动画化时都是可行的）提供基于模型的测试用例，而失败的测试序列将提供将用于优化DFA的反例。

本文的结构如下。 首先，我们在第二部分介绍这项工作意义，即B抽象机器。 我们在第三节介绍使用约束逻辑编程的符号执行原理。 然后，我们在第四节介绍我们研究机器学习算法，介绍测试用例/反例的计算及其对DFA完善的开发。 我们在第五节给出一些实验数据。最后，我们在第六节总结并介绍以后的工作。

1. B机器概述摘要

我们在本节介绍我们所研究的意义，即B抽象机，我们介绍一个运行例子。

A.B方法

B方法致力于正式的软件开发，从高级规范到可执行代码。规范基于三种形式主义：数据是使用集合理论指定的，属性是一阶谓词，行为部分由广义替代来指定。

B方法从编写一个名为抽象机的形式规范开始，给出了系统的功能视图。 然后将机器加入固定属性，表示在系统执行的每个状态下必须保持的属性。 这意味着（i）初始化必须建立不变量，（ii）操作必须保留不变量（意味着如果在操作之前满足不变量，则在执行操作之后也必须满足）。 操作是以基于基本任务为基础的广义替代方法编写的，构成更广义和更具体的结构，例如代表条件替代（IF ... THEN ... ELSE ... END）或非 确定性建筑（选择，任何）。

B方法已经应用于许多工业应用，特别是在铁路领域（例如巴黎地铁第14行，称为METEOR）以及Java应用的环境和背景下。

在这项工作中，我们不考虑B细化，我们只关注抽象机器。 请注意，这不是一个限制，因为机器的细化可以简化为单个B机器。

B.运行示例

我们在这里介绍一个简单的进程调度程序的B抽象机的简单示例。 在这个例子中， 1，进程尝试访问关键部分。 因此，系统管理准备激活的进程的等待队列。 四个操作可以分别创建（新）或删除（删除）进程，使进程请求访问关键部分（就绪），或删除活动进程，以便可以激活（交换）空闲进程。 数据模型由三个变量表示，这些变量表示不请求关键部分（等待）的现有进程集合，一旦发布（准备就绪）和活动进程（活动 - 最多包含）就准备好访问关键部分 一个元素）。

当B模型是自动执行时，用户选择哪一个他想要执行的操作。 根据系统的当前状态和参数值，可以获得不同的结果状态。 我们现在对符号执行的原理进行阐述。

1. 符号执行使用CLP

符号执行通过给出抽象操作参数的可能性来改进原模型。 一旦参数被抽象化，它被替换为由特设的约束求解器处理的符号变量。 抽象出所有的参数值，将每个操作视为现在描述的一组“行为”。

1. 行为定义

我们使用的BZ-Testing-Tools的Prolog引擎，将B机器的操作分解为一个个行为。 每个行为被定义为表示其激活条件的预测，以及指示状态变量的演变和操作的返回参数的实例化的替代。 这些行为被计算为所考虑的B操作的控制流程图中的路径。 它们分为两部分：激活条件和替代。

将操作分解为行为，在执行操作后，根据结果状态给出等效类。

B.使用符号执行

当对B模型进行符号执行时，操作参数被抽象化，因此，通过它们的行为来考虑操作。 每个参数被一个符号变量替换，其值由约束求解器管理。

所有与抽象参数相关的状态变量（例如分配在替换中的状态变量），也成为链接到相应参数的符号变量。 包含至少一个符号状态变量的系统状态被称为符号状态。

符号执行过程通过探索系统操作的连续行为而起作用。 当两个操作必须连接时，这个过程将作为对每个操作的连续行为的可能组合的探索。

在实践中，选择要激活的行为以可见的方式完成，并且使用回溯机制来探索行为链的可能组合的列举。 对于B模型，我们使用CLPS-BZ ，一种使用SICStus Prolog编写的集合理论约束求解器，它能够处理B机器中存在的数据结构的大部分子集（集合，关系，函数，整数， 原子等）。

一旦序列被象征性地播放，可以通过一个简单的标注过程来实现保留符号参数，其中包括解决约束系统并产生符号变量的实例化。 这使得可以产生一个实例化的测试用例。

产生的系统约束的一致性定义了操作顺序的可行性; 据说，后者被认为是可行的，当且仅当存在根据其相关约束向变量分配正确值的至少一个解决方案时。

1. 使用抽象算法

我们现在提出使用学习算法来生成DFA，从中计算测试。 我们回想机器学习的概念，并使用基于符号执行呈现其适应性。

1. 机器学习算法

机器学习算法的目的是推断有限机器机器在状态和转换方面提供了所考虑的系统的行为方式的描述。 机器学习算法基本上由三个主要实体组成。

第一个实体是学习者。 他打算从他收到的信息中构建DFA。 第二个实体是向学习者提供信息的实体。 它可能是一个老师给出可能的系统执行的正确和错误的样本。 学习者也可以直接与系统进行交互，以便询问会员查询，并观察系统是否接受或拒绝提议的执行。 一旦产生了令人满意的DFA，学习者就会询问oracle是否推算的机器与实际的系统相当。 oracle通过“是”或“否”来回答，并提供可以考虑的反例，以便改进DFA并重新开始该过程。

这个算法的最着名的实现之一是由D. Angluin 提出，提出推论的Mealy机器基于以下原则：学习者将执行收集到观察表中，存储已经给予系统的前缀及其相应的输出。 当两个前缀响应于所有可能的输入（由系统字母表给出）产生相同的输出时，则在执行这两个前缀之后达到的状态被合并到相同的状态。

这个过程的主要问题是存在一个能够检查推断的DFA和实际系统的等价性的全能的oracle。 当两个比较系统被称为有限状态机时，Vasilevski和Chow提出了一种解决方案。 基本思想是从一台机器上计算测试序列。 如果其他的通过测试，那么两台机器被宣布为等同的。

该算法的变体是基于通过考虑减少观察表或通过研究树而不是集合来改变观测值的表示。 后一种解决方案已经在我们的方法中进行了选择。

B.使用歧视树构建DFA

我们使用的学习算法的想法是使用符号执行来探索模型执行。 首先，每个状态都是由一组可以从该点激活的行为来识别的。 因此，当一个状态从同一组行为被激活为已经访问的状态时，对模型执行的探索就停止（对于当前的执行部分）。

该算法返回由其根节点标识的树，以及必须完成的一组合并操作，以获取DFA。 每个形式为s1 →s意味着状态s1必须与状态s合并。 该算法跟踪探索必须继续的一组访问状态。 符号动画程序是：获得能够从给定（可能符号）状态s激活的一组行为的可激活行为，并激活计算由激活所产生的状态的行为（s，b） 来自状态的行为b。

虽然算法应该终止，但实际上，在处理大型系统的情况下，它是深度有限的，以增加其收敛。 请注意，使用Prolog的内部回溯机制，使用深度优先算法来完成对模型执行的探索。

一旦树已经建成，就进行探索，以构建相应的自动机。

C.用原始B模型检查等价物

与Vasilevski和Chow 相似，我们建议从我们获得的DFA构建测试，并在原始B模型上重播它们。 对于每个测试，如果测试通过，则将其保留以后被具体化以在SUT上运行。 如果测试失败，即如果在某个（断点）点，该序列是不可行的，那么它代表一个反例。

用于从DFA导出测试的技术是基于图的探索，使用众所周知的技术，如随机散步，贪心算法或过渡旅游（例如使用中文邮递员算法）。

在模型上重现测试，使用符号动画激活序列的连续行为。 一旦动画结束，测试用例被实例化，即符号参数被分配给一个值。

D.处理反例

不可行的所有序列表示反例，即由推断的DFA接受但不是由原始系统接受的迹线。 在机器学习的情况中，这些反例在观察树中被处理。

基本上，修改程序的工作原理如下。 如果跟踪不可行，那么它必然包含已被错误合并的节点。 反例的处理在于首先，识别“断点” - 不应该被合并的节点。 然后，跟踪将添加到树中，从该断点直到序列的最后一个可激活的行为。 因此，每个步骤将表示不会与其他现有节点合并的新状态，但必须对后续节点进行计算。 断点被定义为监视观察树上的跟踪执行时遇到的第一个合并状态。

一旦处理了所有的反例，评估将重新启动，直到找不到反例。 在实践中，如果可行行为序列是可接受的（用户定义的）长度，则反例可以被认为是测试用例。 例如，由最后一步失败的100个步骤组成的测试用例可以保留为测试用例。 在这种情况下，DFA上没有进行反例处理。 可以相对于DFA的大小选择此限制。

1. 成果

在对一个名为Demoney的电子钱包进行实际案例研究之前，我们首先将我们的技术应用于本文中介绍的调度程序的示例。

该技术在计划程序示例中的应用产生了第一个抽象，从中可以使用中文邮递员算法计算出可行的测试。 这个抽象的第一个细化不会改善这个结果，创建新的状态，但仍然导致168个步骤的不可行的跟踪，15个步骤后失败。 这里没有报告的第二个细化，由23个状态和61个转换组成，产生了一个不可行的痕迹，其中包括步骤39步骤后的262个步骤。 Demoney案例研究的结果更好，因为只有一个跟踪在五个不可行，在47个步骤后失败，可以被认为是可接受的测试用例。

虽然有些结果很有趣，但是不可行的测试也会产生。 这可能是由于两个原因。 第一，状态委员会的标准可能太粗糙，将查看所得抽象时的状态合并在一起是不相等的。 第二，探索算法可能未被应用。 事实上，中国的邮递员算法通常会产生长时间的测试用例，这些测试用例在原始模型上直观上更有可能失败。

我们主要关心我们的排斥的正确性，决定加强我们在原始算法中采用的合并标准。 而不是计算给定状态下的可激活行为，我们计算连续行为的可激活对。 结果见表二。 不出所料，计算时间增加，构成抽象的状态和转换次数也增加。 然而，计算的抽象是“正确的”，因为使用中文邮递员算法在其上产生的测试都可以在原始B模型上重放，从而避免细化步骤。

不幸的是，在Demoney案例研究中，抽象并不表示原始规范的所有行为。 请注意，其中绝大多数-41-是同一操作的错误行为。 目前正在研究技术的改进以弥补失踪行为。

为了评估我们的测试用例的相关性，我们对Scheduler示例进行了突变分析。 我们手动创建了一组15个突

剩余内容已隐藏，支付完成后下载完整资料

资料编号：[137615]，资料为PDF文档或Word文档，PDF文档可免费转换为Word