In: LNCS 2043: Reliable Software Technologies - Ada-Europe 2001, pages 35-pp. 6th Ada-Europe International Conference, Leuven, Belgium, May 14-18, 2001, Proceedings / D. Craeynest and A. Strohmeier (Eds.) --- Springer Verlag, 2001.
Abstract: Deriving test cases from specifications is now recognised as a major application of formal methods to software development. Several methods have been proposed for various formalisms: behavioural descriptions such as transition systems, model-based specifications, algebraic specifications, etc. This article presents a general framework for test data selection from formal specifications. A notion of "exhaustive test set" is derived from the semantics of the formal notation and from the definition of a correct implementation. Then a finite test set is selected via some "selection hypotheses", This approach has been illustrated by its application to algebraic specifications, object-oriented Petri nets (CO-OPN2), LUSTRE, and full LOTOS.