Generating trace-sets for model-based testing

  • Lindström B
  • Pettersson P
  • Offutt J
  • 9


    Mendeley users who have this article in their library.
  • 4


    Citations of this article.


Model-checkers are powerful tools that can find individual traces through models to satisfy desired properties. These traces provide solutions to a number of problems. Instead of individual traces, software testing needs sets of traces that satisfy coverage criteria. Finding a trace set in a large model is difficult because model checkers generate single traces and use a lot of memory. Space and time requirements of modelchecking algorithms grow exponentially with respect to the number of variables and parallel automata of the model being analyzed. We present a method that generates a set of traces by iteratively invoking a model checker. The method mitigates the memory consumption problem by dynamically building partitions along the traces. This method was applied to a testability case study, and it generated the complete trace set, while ordinary model-checking could only generate 26%.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Get full text


Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free