Generation of fault detecting tests from formal specifications by model checking

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 and combinatorial coverage criteria and show an empirical cross coverage among faults.