Structural abstract method for design of checking tests for automata

A method is proposed for design of a checking test whereby properties of the abstract specification and of the structural automaton implementation are used. The method does not require complete search of the faults and leads to shorter tests than those obtained by conventional abstract methods.