REGRESSION TESTING VIA MODEL CHECKING

摘要

The use of formal methods has long been recognized as improving the quality of software specifications and implementations, early in the process of software development. Regression testing is an important activity during the maintenance phase, aimed at ensuring that modified software still meets the customer's requirements. In this paper, we present a specification-based regression testing technique using model checking, whose objective is to generate test cases for a modified system based on formal specification(s) of the system, instead of based on the evolving source code. The substantial advantage of combining a model checker with regression testing is two-fold. First, each counterexample can be considered as a complete test sequence; therefore, generating test cases can be automatic. Second, more confidence can be gained by deriving regression test cases based on a formal description of the evolving system. We propose a hierarchical approach to guide regression test selection with different levels of test criteria based on users' requirements and constraints.