Toward testing from finite state machines with symbolic inputs and outputs

After 60 or so years of development, the theory of checking experiments for FSM still continues to attract a lot of attention of research community. One of the reasons is that it offers test generation techniques which under well-defined assumptions guarantee complete fault coverage for a given fault model of a specification FSM. Checking experiments have already been extended to remove assumptions that the specification Mealy machine need to be reduced, deterministic, and completely specified, while keeping the input, output and state sets finite. In our recent work, we investigated possibilities of removing the assumption about the finiteness of the input set, introducing the model FSM with symbolic inputs. In this paper, we report the results that further lift the theory of checking experiments for Mealy machines with symbolic inputs and symbolic outputs. The former are predicates defined over input variables and the latter are output variable valuations computed by assignments on input variables. Both types of variables can have large or even infinite domains. Inclusion of assignments in the model complicates even output fault detection, as different assignments may produce the same output valuations for some input valuations. We address this issue by using a transition cover composed of symbolic inputs on which the assignments produce different outputs. The enhanced transition cover is then used in checking experiments, which detect assignment/output faults and more general transition faults under certain assumptions.