Vlad Rusu, Lydie du Bousquet, and Thierry JÚron. An approach to symbolic test
generation. In International Conference on Integrating Formal Methods
(IFM'00), Dagstuhl (Germany), pp 338-357, 2000. LNCS 1945.
Test generation is a program-synthesis problem: starting from the formal
specification of a system under test, and from a test purpose describing
a set of behaviours to be tested, compute a reactive program that observes an
implementation of the system to detect non-conformant behaviour, while
trying to control it towards satisfying the test purpose. In this paper
we describe an approach for generating symbolic test cases,
in the form of input-output automata with variables and parameters.
Full postscript text.