Testing from Formal Specifications, a Generic Approach

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.

• Type: Conference
• Year: 2001
• Where: ADAEUROPE
• Authors: Marie-Claude Gaudel
• Keywords: ADAEUROPE 2001, Algebraic Specifications, Software Engineering, Test Data Selection, Test Set