Using a SAT solver to generate checking sequences

—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.

• Type: Conference
• Year: 2009
• Where: ISCIS
• Authors: Guy-Vincent Jourdan, Hasan Ural, Hüsnü Yenigün, Dong Zhu
• Keywords: Checking Sequence, Finite State Machines, Information Management, Input Sequence, ISCIS 2009