Model based generation of high coverage test suites for embedded systems

In this paper an algorithm for the model-based generation of high coverage test suites for embedded systems using a combination of model checking and optimization techniques is described. The algorithm is able to compute high coverage test suites starting from a formal model of the System Under Test. The novelty of the proposed method resides in the formulation of an incremental test synthesis strategy combining bounded model checking with an optimization-based formulation of the test case generation problem.