A Decompositional Approach to Automatic Test Case Generation Based on Formal Specifications

Automatic functional testing is a potentially effective technique for software reliability, but it has been a challenge due to the difficulties in automatically deriving adequate test cases and test oracle from informal or semi-formal specifications that are often used in practice. This paper puts forward a new decompositional approach to automatic test case generation on the basis of model-based formal specifications. The approach offers a functional scenario-based test strategy, a set of test case generation criteria, a set of automatic test case generation algorithms, and a well-defined test oracle for automatic test result analysis. A small experiment on the application of the approach is presented, and the result shows that the approach can achieve a higher statement coverage of programs than random testing.