State verification

Abstract

State verification is the problem of verifying that a Mealy machine, placed in a black box, is in a specified state s. The state diagram of the machine is assumed to be known. The only way of doing this, short of opening the box, is to feed input to the machine, and study the output. Therefore, state verification for state s is only possible if there is an input sequence x such that the output produced by the machine when it is in state s and is given input x is unique, i.e., there is no other state that would produce the same output on input x. Such an input sequence is called a unique input-output, or UIO sequence. Thus the problem of state verification reduces to that of computing UIO sequences for the states to be verified. Unfortunately, not all states of all Mealy machines have UIO sequences. However, they are frequent enough in many practical test settings to be a valuable tool in conformance testing of Mealy machines; see Chapter 4. Specifically, UIO sequences are more common than distinguishing sequences, either adaptive or preset; see Chapter 2. Computing UIO sequences is a hard problem. In fact, even determining whether a given state has a UIO sequence is PSPACE-complete [LY94]. Thus there is most probably no polynomial time algorithm for computing the sequences. Also, some states have UIO sequences, but none of polynomial length [LY94], which is a problem in testing applications. Still, some algorithms have been proposed and tried in practice. They have exponential worst case complexity, but use heuristics that allow efficient computations for many relevant problem instances. The most elaborate algorithm is that of Naik [Nai97]. It tries to compute sequences for some states quickly, and then use them to infer sequences for other states. Guo et al. suggest a genetic algorithm, where a fitness function is used to evaluate candidate sequences, which are then paired using crossover and mutated, for a certain number of generations [GHHD04]. The research field is still open for new algorithmic ideas and better analysis of performance on interesting subclasses of Mealy machines. © Springer-Verlag Berlin Heidelberg 2005.