Abstraction and refinement of mathematical functions toward SMT-based test-case generation

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.