Model Checkers in Software Testing.

摘要

The primary focus of formal methods is static analysis of specifications and code, but there is also a long tradition of exploiting formal methods for testing. This paper continues this tradition by exploring the role of model checkers in software testing. Model checkers were originally developed to check that state machines conformed to specifications expressed in a temporal logic. We show how to apply the powerful computation engines in model checkers to the problems of test generation and test evaluation in model checkers to the problems of test generation and test evaluation for a variety of test coverage criteria defined on model-based specifications.