Skip to main content

Automated Black-Box Testing with Abstract VDM Oracle

  • Conference paper
  • First Online:
Book cover Computer Safety, Reliability and Security (SAFECOMP 1999)

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

Included in the following conference series:

Abstract

In this paper the possibilities to automate black-box testing through formal requirement specifications are explored. More precisely, the formal method VDM (Vienna Development Method) serves to demonstrate that abstract requirement models can be used as test oracles for concrete software. The automation of the resulting testing frame-work is based on modern CASE-tools that support a light-weight approach to formal methods. The specification language used is VDMSL, but the results are easily transferred into similar model oriented methods such as B, Z or RAISE.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.-R. Abrial. The B-Book, Assigning programs to meanings. Cambridge University Press, 1996. ISBN 0521 49619 5(hardback).

    Google Scholar 

  2. Lionel Van Aertryck. Une méthode et un outil pour l’aide à la génération de jeux de tests de logiciels. PhD thesis, Université de Rennes, January 1998.

    Google Scholar 

  3. Sten Agerholm, Pierre-Jean Lecoeur, and Etienne Reichert. Formal specification and validation at work: A case study using VDM-SL. In Proceedings of Second Workshop on Formal Methods in Software Practice, Florida, Marts. ACM, 1998.

    Google Scholar 

  4. Bernhard K. Aichernig. Automated requirements testing with abstract oracles. In ISSRE’98: The Ninth International Symposium on Software Reliability Engineering, Paderborn, Germany, pages 21–22, IBM Thomas J. Watson Research Center, P.O.Box 218, Route 134, Yorktown Heights, NY, USA, November 1998. Ram Chillarege. ISBN 3-00-003410-2.

    Google Scholar 

  5. Bernhard K. Aichernig and Peter Gorm Larsen. A proof obligation generator for VDM-SL. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME’97: Industrial Applications and Strengthened Foundations of Formal Methods, volume 1313 of Lecture Notes in Computer Science, 1997.

    Google Scholar 

  6. Bernhard K. Aichernig and Peter Lucas. Softwareentwicklung — eine Ingenieursdisziplin!(?). Telematik, Zeitschrift des Telematik-Ingenieur-Verbandes (TIV), 4(2):2–8, 1998. ISSN 1028-5068.

    Google Scholar 

  7. Boris Beizer. Software Testing Techniques. Van Nostrand Reinhold, New York, 2nd edition, 1990.

    Google Scholar 

  8. R. E. Bloomfield and P. K. D. Froome. The application of formal methods to the assessment of high integrity software. IEEE Transactions on Software Engineering, SE-12(9):988–993, September 1986.

    Google Scholar 

  9. Jeremy Dick and Alain Faivre. Automating the generation and sequencing of test cases from model-based specifications. In J. C. P. Woodcock and P. G. Larsen, editors, FME’93: Industrial-Strength Formal Methods. Springer-Verlag, April 1993.

    Google Scholar 

  10. Michael R. Donat. Automating formal specification-based testing. In Michel Bidoit and Max Dauchet, editors, TAPSOFT’ 97:Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, volume 1214 of Lecture Notes in Computer Science, pages 833–847. Springer-Verlag, April 1997.

    Chapter  Google Scholar 

  11. John Fitzgerald and Peter Gorm Larsen. Modelling Sytems, Practical Tools and Techniques. Cambridge University Press, 1998.

    Google Scholar 

  12. Brigitte Fröhlich and Peter Gorm Larsen. Combining VDM-SL specifications with C++ code. In Marie-Claude Gaudel and Jim Woodcock, editors, FME96, Industrial Benefit and Advances in Formal Methods, Lecture Notes in Computer Science, pages 179–194. Springer, March 1996.

    Google Scholar 

  13. Chris George et al. The Raise Development Method. The BCS Practitioner Series. Prentice Hall, 1995.

    Google Scholar 

  14. Andrew Harry. The value of reference implementations and prototyping in a formal design and testing methodology. Report 208/92, National Physical Laboratory, Queen’s Road, Teddington, Middelsex TW11 0LW, UK, October 1992.

    Google Scholar 

  15. Steffen Helke, Thomas Neustupny, and Thomas Santen. Automating test case generation from Z specifications with Isabelle. In ZUM’97, 1997.

    Google Scholar 

  16. Johann Hörl. Formal specification of a voice communication system used in air traffic control. Master’s thesis, Institute for Software Technology (IST), Technical University Graz, Austria, December 1998.

    Google Scholar 

  17. IFAD. IFAD’s homepage. http://www.ifad.dk/.

  18. Cliff B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, Englewood Cliffs, New Jersey, second edition, 1990.

    MATH  Google Scholar 

  19. Cliff B. Jones. Formal methods light: A rigorous approach to formal methods. IEEE Computer, 29(4):20–21, April 1996.

    Google Scholar 

  20. P. G. Larsen, B. S. Hansen, H. Bruun, N. Plat, H. Toetenel, D. J. Andrews, J. Dawes, G. Parkin, et al. Information technology — Programming languages, their environments and system software interfaces — Vienna Development Method — Specification Language — Part 1: Base language, December 1996. International Standard ISO/IEC 13817-1.

    Google Scholar 

  21. Janusz Laski. Data ow testing in STAD. The Journal of Systems and Software, 12(1):3–14, 1990.

    Article  Google Scholar 

  22. OMG. The common object request broker architecture and specification, revision 2.0. Technical report, OMG, 1996.

    Google Scholar 

  23. Jesper Pedersen. Automatic test case generation and instantiation for VDM-SL specifications. Master’s thesis, Department of Mathematics and Computer Science, Odense University, September 1998.

    Google Scholar 

  24. J. Peleska and M. Siegel. Test automation of safety-critical reactive systems. South African Computer Jounal, 19:53–77, 1997.

    Google Scholar 

  25. J. M. Spivey. The Z Notation. Series in Computer Science. Prentice-Hall, 1989.

    Google Scholar 

  26. Philip Alan Stocks. Applying formal methods to software testing. PhD thesis, The Department of computer science, The University of Queensland, 1993.

    Google Scholar 

  27. Ole Storm. The VDM Toolbox API users guide. Technical report, IFAD, 1998.

    Google Scholar 

  28. H. Treharne, J. Draper, and S. Schneider. Test case preparation using a prototype. In B’98 — Second B-Conference, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Aichernig, B.K. (1999). Automated Black-Box Testing with Abstract VDM Oracle. In: Felici, M., Kanoun, K. (eds) Computer Safety, Reliability and Security. SAFECOMP 1999. Lecture Notes in Computer Science, vol 1698. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48249-0_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-48249-0_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66488-8

  • Online ISBN: 978-3-540-48249-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics