Software Testing via Model Checking

摘要

Testing is a necessary, but costly process for user-centric quality control. Moreover, testing is not comprehensive enough to completely detect faults. Many formal methods have been proposed to avoid the drawbacks of testing, e.g., model checking that can be automatically carried out. This paper presents an approach that (ⅰ) generates test cases from the specification and (ⅱ) transfers the specification-oriented testing process to model checking. Thus, the approach combines the advantages of testing and model checking assuming the availability of (ⅰ) a model that specifies the expected, desirable system behavior as required by the user and (ⅱ) a second model that describes the system behavior as observed. The first model is complemented in also specifying the undesirable system properties. The approach analyzes both these specification models to generate test cases that are then converted into temporal logic formulae to be model checked on the second model.