Title: Using a SAT Solver to Generate Checking Sequences

Abstract:
Methods for software testing based on Finite State Machines (FSMs) have
been researched since the early 60’s. Many of these methods are about
generating a checking sequence from a given FSM which is an input sequence
that determines whether an implementation of the FSM is faulty or correct.
In this paper, we consider one of these methods, which constructs a
checking sequence by reducing the problem of generating a checking
sequence to finding a Chinese rural postman tour on a graph induced by the
FSM; we re-formulate the constraints used in this method as a set of
Boolean formulas; and use a SAT solver to generate a checking sequence of
minimal length.