Coverage for Model Checking: When model checking is incomplete and no errors are reported, we would like to gain information about what aspects of the program’s behavior have been checked. To do this, we can use some standard (and some not-so-standard) test coverage criteria. Test coverage provides a measure of how well the testing framework actually checks the application software and how can we know when to stop testing. The situation with a model checker is similar. We want to know what parts of the state space were covered.
There are different coverage levels that we can measure (Cornett 1996):
- Function Coverage
- Statement Coverage
- Decision Coverage
- Condition Coverage
- Multiple Condition Coverage
- Condition/Decision Coverage
- Modified Condition/Decision Coverage
- Path Coverage
- Branch Coverage