An approach for the verification and synthesis of complete test generation algorithms for finite state machines

Complete test suites are of special interest in the field of model-based testing, as they guarantee high fault detection capabilities under well-specified assumptions. The variety and complexity of strategies generating complete test suites, their implementations, and their completeness proofs impose difficulties upon manual verification. Furthermore, ambiguities or only implicitly specified assumptions in natural language descriptions and proofs easily lead to implementations that do not generate complete test suites.

The present dissertation proposes an alternative approach to the verification and implementation of test strategies that generate complete test suites for testing for language-equivalence on finite state machines, that employs the interactive theorem prover Isabelle.

In the first part of this work, similarities and differences between steps performed by the considered test strategies are identified. From these, a framework is derived as a higher order function capable of representing all considered strategies as concrete applications of it. Several implementations of parameters of this framework are shared between multiple strategies. Additional frameworks are developed to support alternative completeness proofs.

The second part of this work defines finite state machines, their properties and operations, as well as the frameworks in Isabelle/HOL and respectively proves them correct and complete. Completeness proofs over frameworks are decoupled from concrete implementations of their parameters by suitable interfaces. This approach enables the reuse of proofs between similar strategies and thus simplifies completeness proofs for new variations on already handled strategies.

Finally, the definitions in Isabelle are employed to automatically generate provably correct implementations of the considered test strategies. It is shown that these exhibit comparable performance to a manually developed C++ library for certain inputs.