Testing of Ada Abstract Data Types using Formal Specifications

The purpose of this paper is to present an experiment with formal methods for the black-box testing of reusable abstract data types (ADTs). We propose to test a family of software components by re-engineering a formal specification from an existing Ada implementation, using algebraic specifications. From this well-defined basis, we generate test sets automatically, by constructing an exhaustive set of formulae that prove the property preservations of a program with respect to its specifications, and by reducing this set to a finite size by applying reduction hypotheses. Once the selection of a finite test set has been performed, we show how to build the oracle, the decision procedure for the success or the failure of a test set. Finally, we discuss the advantages of test sets generated from the formal specification over those defined by a programmer, based on his intuitive understanding of the behavior of the ADT.


Editor(s):
Toussaint, Marcel
Published in:
Eurospace Ada-Europe'94 Symposium Proceedings, Copenhagen, Danemark, September 26-30 1994, 887, 76-89
Year:
1994
Publisher:
Springer Verlag
Keywords:
Note:
Also available as Technical Report EPFL-DI No 94/75
Laboratories:




 Record created 2005-09-20, last modified 2018-01-27

External link:
Download fulltext
n/a
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)