Fault model-driven testing from FSM with symbolic inputs

Test generation based on one-by-one analysis of potential implementations in fault models is challenging; it is indeed impossible or inefficient to enumerate each and every implementation, even when a fault model defines a finite but a significant number of implementations. We propose an approach for fault model and constraint solving-based testing from a particular type of extended finite state machines called a symbolic input finite state machine (SIFSM). Transitions in SIFSMs are labeled with symbolic inputs, which are predicates on input variables having possibly infinite domains. Its implementations, mutants, are also represented by SIFSMs. The generated tests are complete in a given fault domain which is a set of mutants specified with a so-called mutation machine. We define a well-formed mutation SIFSM for describing various types of faults. Given a mutation SIFSM, we develop methods for evaluating the adequacy of a test suite and generating complete tests. Experimental results with the prototype tool we have developed indicate that the approach is applicable to industrial-like systems.