University of Minnesota
Software Engineering Center

You are here

Robert Weber

Recent Publications

Specification Test Coverage Adequacy Criteria = Specification Test Generation Inadequacy Criteria?

The successful analysis technique model checking can be employed as a test-case generation technique to generate tests from formal models. When using a model checker for test case generation, we leverage the witness (or counter-example) generation capability of model-checkers for constructing test cases. Test criteria are expressed as temporal properties and the witness traces generated for these properties are instantiated to create complete test sequences, satisfying the criteria.