Abstraction and refinement of mathematical functions toward SMT-based test-case generation
Abstraction and refinement of mathematical functions toward SMT-based test-case generation
复制标题
针对基于 SMT 的测试用例生成的数学函数的抽象和细化
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Akihiro Yamamoto
中科院分区：
文献类型：
--
作者：
Takuro Kutsuna;Yoshinao Ishii;Akihiro Yamamoto
我们提出了一种新的软件测试用例生成方法，其中包括数学函数，如三角函数、对数函数、用非线性内插实现的查找表函数等。在有界模型检测方案中，使用可满足性模理论(SMT)求解器迭代地生成测试用例。在该方法中，对数学函数进行了抽象，使得推导出的公式可以很容易地用SMT求解器来处理。抽象是基于前面的反例进行自适应提炼的。我们还提出了一种通过抽样和机器学习来估计数学函数抽象程度的通用方法。虽然本文提出的方法主要针对测试用例的生成，但在抽象为正确的过近似的假设下，该方法也适用于普通的有界模型检测。以汽车行业的嵌入式控制软件为例，对所提出的方法进行了评估。实验结果表明了该方法的有效性。
We propose a novel approach for generating test cases of software that includes mathematical functions, such as trigonometric functions, logarithmic functions, functions implemented as look-up tables with non-linear interpolation, and so on. A satisfiability modulo theories (SMT) solver is iteratively used to generate test cases in the scheme of bounded model checking. In the proposed method, mathematical functions are abstracted so that the derived formula can be easily treated using an SMT solver. The abstraction is refined adaptively based on the previous counterexamples. We also propose a general method to estimate an abstraction of a mathematical function by means of sampling and machine learning. Although the method proposed in this paper addresses mainly the topic of test-case generation, it is also applicable to ordinary bounded model checking under the assumption that the abstraction should be a correct over-approximation. We evaluated the proposed method by applying it to an example of embedded control software taken from the automotive industry. The experimental results show the usefulness of the proposed method.