Researches on Automatic Techniques for Specification-Based Testing and Fault Localization

The existing specification-based techniques (SBT) has difficulty in generating an appropriate test suite without the knowledge of code structure to trigger different kinds of unintended behaviours hidden in programs. Symbolic execution, a powerful technique for automating software testing, instead takes advantage of internal code design to detect many types of errors like out of memory and assertion violations. However, it can encounter severe path explosion problem during the exhausted test data generation. Besides, by only using assertions, it may ignore some faulty paths due to not going deep into checking the functional correctness of a path. To address these problems, this research proposes a specification-based incremental testing method with symbolic execution, called SIT-SE, to provide a much more rigorous way to automatically check the functional correctness of all the discovered program paths within limited time. In this method, we introduce theorems instead of assertions for checking path correctness, and describe a Branch Sequence Coverage (BSC) algorithm together with checking levels for guiding a moderate path exploration. The proposed method carefully treats the relationship between a path condition and the specification in a theorem to reduce the monotonous path exploration, whereas traditional symbolic testing methods use assertions that are not sufficient to judge the correctness of a path during the long tedious path exploration. Moreover, we present a strategy of fault localization called TRIACFL with the support of the SIT-SE to give useful hints to pinpoint the faults in a small set of statements. To enrich our methodology of testing used in practice, we also describe a test data generation method that integrates formal specification with a genetic algorithm as supplementary to the SIT-SE for dealing with exceptional cases where some code is not available to testers. We conduct two experiments with the proposed methods, and the results demonstrate that these methods together facilitate an effective automatic bug detection.There are three main contributions in our work. Firstly, we propose a method, SIT-SE, to provide a systematic way to automatically verify the correctness of all the representative program paths by integrating symbolic execution and formal specification. Secondly, we present a fault localization method with the SIT-SE, namely TRIACFL, to provide useful clues for the locations of real faults within a small scale of statements in programs. Thirdly, a test data generation method using the formal specification and a genetic algorithm (GA), is proposed to cope with the situations where the SIT-SE is not applicable.博士(理学)法政大学 (Hosei University