G∀ST is a fully automatic test system. Given a logical property, stated as a function, it is able to generate appropriate test values, to execute tests with these values, and to evaluate the results of these tests. Many reactive systems, like automata and protocols, however, are specified by a model rather than in logic. There exist tools that are able to test software described by such a modelbased specification, but these tools have limited capabilities to generate test data involving data types. Moreover, in these tools it is hard or even impossible to state properties of these values in logic. In this paper we introduce some extensions of G∀ST to combine the best of logic and model based testing. The integration of model based testing and testing based on logical properties in a single automated system is the contribution of this paper. The system consists only of a small library rather than a huge stand-alone system.
Pieter W. M. Koopman, Rinus Plasmeijer