Learning-based Software Testing using Symbolic Constraint Solving Methods

Sammanfattning: Software testing remains one of the most important but expensive approaches to ensure high-quality software today. In order to reduce the cost of testing, over the last several decades, various techniques such as formal verification and inductive learning have been used for test automation in previous research. In this thesis, we present a specification-based black-box testing approach, learning-based testing (LBT), which is suitable for a wide range of systems, e.g. procedural and reactive systems. In the LBT architecture, given the requirement specification of a system under test (SUT), a large number of high-quality test cases can be iteratively generated, executed and evaluated by means of combining inductive learning with constraint solving. We apply LBT to two types of systems, namely procedural and reactive systems. We specify a procedural system in Hoare logic and model it as a set of piecewise polynomials that can be locally and incrementally inferred. To automate test case generation (TCG), we use a quantifier elimination method, the Hoon-Collins cylindric algebraic decomposition (CAD), which is applied on only one local model (a bounded polynomial) at a time. On the other hand, a reactive system is specified in temporal logic formulas, and modeled as an extended Mealy automaton over abstract data types (EMA) that can be incrementally learned as a complete term rewriting system (TRS) using the congruence generator extension (CGE) algorithm. We consider TCG for a reactive system as a bounded model checking problem, which can be further reformulated into a disunification problem and solved by narrowing. The performance of the LBT frameworks is empirically evaluated against random testing for both procedural and reactive systems (executable models and programs). The results show that LBT is significantly more efficient than random testing in fault detection, i.e. less test cases and potentially less time are required than for random testing.