Abstract
This paper tackles some aspects concerning the exploitation of Abstract State Machines (ASMs) for testing purposes. We define
for ASM specifications a set of adequacy criteria measuring the coverage achieved by a test suite, and determining whether
sufficient testing has been performed. We introduce a method to automatically generate from ASM specifications test sequences
which accomplish a desired coverage. This method exploits the counter example generation of the model checker SMV. We use
ASMs as test oracles to predict the expected outputs of units under test.
[download the pdf file] [DOI]