Generating tests from EFSM models using guided model checking and iterated search refinement

Abstract

We present a way to generate test sequences from EFSM models using a guided model checker: Uppaal Cora. The approach allows to specify various structural test coverage criteria of EFSMs, for example, selected states/transitions, all transitions, all transition pairs, etc. We describe a method to construct Uppaal models to achieve test sequences satisfying these criteria and experiment with the search options of Uppaal to achieve test sequences that are suboptimal in terms of length. We apply a bitstate hashing space reduction based iterated search refinement method to shorten the length of test sequences with respect to the length gained using depth first search. The test generation method and different search strategies are compared by applying them on a stopwatch and INRES protocol based case study. The outcome shows the feasibility of applying guided model checking in conjunction with iterated search refinement for generating suboptimal test sequences. © 2006 Springer-Verlag Berlin/Heidelberg.