Skip to main content
SpringerLink
Log in

Testing Ada abstract data types using formal specifications

  • Conference paper
  • First Online:
Ada in Europe (Ada-Europe 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 887))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Stéphane Barbey and Alfred Strohmeier. The problematics of testing object-oriented software. In M. Ross, C.A. Brebbia, G. Staples, and J. Stapleton, editors, SQM '94 Second Conference on Software Quality Management, volume 2, pages 411–426, Edinburgh, Scotland, UK, July 26–28 1994.

    Google Scholar 

  2. Gilles Bernot. Testing against formal specifications: A theoritical view. In TAP-SOFT '91, number 494 in Lecture Notes in Computer Sciences. Springer Verlag, April 1991.

    Google Scholar 

  3. Gilles Bernot, Marie-Claude Gaudel, and Bruno Marre. Software testing based on formal specifications: a theory and a tool. IEE Software Engineering Journal, 6(6):387–405, November 1991.

    Google Scholar 

  4. Didier Buchs, Jacques Flumet, and Pascal Racloz. SANDS: Structured algebraic net development system. In Buy Ugo, editor, 14th International Conference on Application and Theory of Petri Nets, Tool presentation abstracts, pages 25–29. Chicago, USA, June 1993.

    Google Scholar 

  5. Didier Buchs and Nicolas Guelfi. A concurrent object-oriented Petri nets approach for system specification. In M. Silva, editor, 12th International Conference on Application and Theory of Petri Nets, pages 432–454, Aahrus, Denmark, June 1991.

    Google Scholar 

  6. Pierre Dauchy, Marie-Claude Gaudel, and Bruno Marre. Using algebraic specifications in software testing: A case study on the software of an automatic subway. Journal of Systems and Software, 21(3):229–244, June 1993. North Holland, Elsevier Science Publishing Company.

    Google Scholar 

  7. Hartmut Ehrig and Bernd Mahr. Fundamentals of algebraic specification 1: equations and initial semantics. EATCS Monographs on Theoritical Computer Science. Springer-Verlag, March 1985.

    Google Scholar 

  8. Claude Genillard, Norbert Ebel, and Alfred Strohmeier. Rationale for the design of reusable abstract data types implented in Ada. ACM Ada Letters, 9(2):62–71, March 1989.

    Google Scholar 

  9. J. Liddiard. Achieving testability when using Ada packaging and data hiding methods. Ada User, 14(1):27–32, March 1993.

    Google Scholar 

  10. Bruno Marre. Sélection automatique de jeux de tests à partir de spécifications algébriques en utilisant la programmation logique. PhD thesis, LRI, Université de Paris XI, Orsay, France, January 1991.

    Google Scholar 

  11. Bertrand Meyer. Reusable Software: the base object-oriented component library. The Object-Oriented Series. Prentice-Hall, 1994.

    Google Scholar 

  12. I. Spence and C. Meudec. Generation of software tests from specifications. In M. Ross, C.A. Brebbia, G. Staples, and J. Stapleton, editors, SQM '94 Second Conference on Software Quality Management, volume 2, pages 517–530, Edinburgh, Scotland, UK, July 26–28 1994.

    Google Scholar 

  13. Alfred Strohmeier, editor. Ada Software Components. EPFL, 2nd edition, 1992.

    Google Scholar 

  14. Alfred Strohmeier. Use of a software component library in student projects. In A. Finkelstein and B. Nuseibeh, editors, ACM/IEEE International Workshop on Software Education (ICSE), pages 319–326, Sorrento, Italia, 1994.

    Google Scholar 

  15. Elaine J. Weyuker. The oracle assumption of program testing. In 13th International Conference on System Sciences, pages 44–49, Hawaii, USA, 1980.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Swiss Federal Institute of Technology in Lausanne Software Engineering Laboratory, EPFL-DI-LGL, CH-1015, Lausanne, Switzerland

    Stéphane Barbey & Didier Buchs

Authors
  1. Stéphane Barbey
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Didier Buchs
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Marcel Toussaint

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barbey, S., Buchs, D. (1994). Testing Ada abstract data types using formal specifications. In: Toussaint, M. (eds) Ada in Europe. Ada-Europe 1994. Lecture Notes in Computer Science, vol 887. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58822-1_90

Download citation

  • DOI: https://doi.org/10.1007/3-540-58822-1_90

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58822-1

  • Online ISBN: 978-3-540-49110-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation