Abstract
We present a technique which generates from Abstract State Machines specifications a set of test sequences capable to uncover
specific fault classes. The notion of test goal is introduced as a state predicate denoting the detection condition for a
particular fault. Tests are generated by forcing a model checker to produce counter examples which cover the test goals. We
introduce a technique for the evaluation of the fault detection capability of a test set. We report some experimental results
which validate the method, compare the fault adequacy criteria with some classical structural coverage criteria and show an
empirical cross coverage among faults.
[download the pdf file] [DOI]