A Comparison of the BTT and TTF Test-Generation Methods

  • Bruno Legeard
  • Fabien Peureux
  • Mark Utting
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


This paper compares two methods of generating tests from formal specifications. The Test Template Framework (TTF) method is a framework and set of heuristics for manually generating test sets from a Z specification. The B Testing Tools (BTT) method uses constraint logic programming techniques to generate test sequences from a B specification. We give a concise description of each method, then compare them on an industrial case study, which is a subset of the GSM 11.11 smart card specification.


Current Directory State Machine Formal Method Smart Card Constraint Logic Programming 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    John D. Gannon, Paul R. McMullin, and Richard G. Hamlet. Data-abstraction implementation, specification, and testing. ACM TOPLAS, 3(3):211–223, 1981.CrossRefGoogle Scholar
  2. 2.
    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, number 670 in LNCS, pages 268–284. Springer-Verlag, April 1993.CrossRefGoogle Scholar
  3. 3.
    Michael R. Donat. Automating formal specification-based testing. In Michel Bidoit and Max Dauchet, editors, TAPSOFT’ 97: Theory and Practice of Software Development, volume 1214 of LNCS, pages 833–847. Springer, 1997.CrossRefGoogle Scholar
  4. 4.
    Susan Stepney. Testing as abstraction. In J. P. Bowen and M. G. Hinchey, editors, ZUM’95: 9th International Conference of Z Users, Limerick, 1995, volume 967 of Lecture Notes in Computer Science, pages 137–151. Springer-Verlag, 1995.Google Scholar
  5. 5.
    Hans-Martin Hoercher and Jan Peleska. Using formal specifications to support software testing. Software Quality Journal, 4(4):309–327, 1995.CrossRefGoogle Scholar
  6. 6.
    C. Péraire, S. Barbey, and D. Buchs. Test selection for object-oriented software based on formal specifications. In David Gries and Willem-Paul de Roever, editors, Programming Concepts and Methods: PROCOMET’ 98, IFIP TC2/WG2.2, 2.3 International Conference, June 1998, Shelter Island, New York, pages 385–403. Chapman and Hall, 1998.Google Scholar
  7. 7.
    R. M. Hierons. Testing from a z specification. Journal of Software Testing, Verification and Reliability, 7:19–33, 1997.CrossRefGoogle Scholar
  8. 8.
    Igor Burdonov, Alexander Kossatchev, Alexander Petrenko, and Dmitri Galter. KVEST: Automated generation of test suites from formal specifications. In Wing et al. [28], pages 605–621. LNCS 1708 (Volume 1).Google Scholar
  9. 9.
    S. Behnia and H. Waeselynck. Test criteria definition for B models. In Wing et al. [28], pages 509–529. LNCS 1708 (Volume 1).Google Scholar
  10. 10.
    Philip Stocks. Applying formal methods to software testing. PhD thesis, The Department of Computer Science, The University of Queensland, 1993. Available from
  11. 11.
    P. A. Stocks and D. A. Carrington. A framework for specification-based testing. IEEE Transactions in Software Engineering, 22(11):777–793, November 1996.CrossRefGoogle Scholar
  12. 12.
    D. Carrington and P. Stocks. A tale of two paradigms: Formal methods and software testing. In Proceedings of the 8th Z User Meeting, pages 51–68. Springer-Verlag, 1994.Google Scholar
  13. 13.
    L. Py, B. Legeard, and B. Tatibouet. Évaluation de spécifications formelles en programmation logique avec contraintes ensemblistes — application á l’animation de spécification formelles B. In AFADL’2000, Grenoble, 26–28 Jan 2000, pages 21–35, 2000.Google Scholar
  14. 14.
    Bruno Legeard and Fabien Peureux. Generation of functional test sequences from B formal specification — presentation and industrial case-study. Submitted to Automated Software Engineering 2001, 2001.Google Scholar
  15. 15.
    L. Murray, D. Carrington, I. MacColl, J. McDonald, and P. Strooper. Formal derivation of finite state machines for class testing. In J. P. Bowen, A. Fett, and M. G. Hinchey, editors, ZUM’98: The Z Formal Specification Notation, volume 1493 of LNCS, pages 42–49. Springer-Verlag, 1998.CrossRefGoogle Scholar
  16. 16.
    P. Stocks and D. Carrington. Test templates: A specification-based testing framework. In Proceedings of the 15th International Conference on Software Engineering, pages 405–414. IEEE Computer Society Press, 1993.Google Scholar
  17. 17.
    L. Murray, D. Carrington, I. MacColl, and P. Strooper. Extending test templates with inheritance. In Proceedings of 1997 Australian Software Engineering Conference (ASWEC’97), pages 80–87. IEEE Computer Society, 1997. Also SVRC Technical Report 97-18.Google Scholar
  18. 18.
    I. MacColl and D. Carrington. Extending the TTF for specification-based testing of interactive systems. In Australasian Computer Science Conference (ACSC99), pages 372–381. Springer-Verlag, 1999.Google Scholar
  19. 19.
    L. Murray, D. Carrington, I. MacColl, and P. Strooper. Tinman-a test derivation and management tool for specification-based class testing. In Technology of Object-Oriented Languages and Systems (TOOLS 32), pages 222–233. IEEE Computer Society, 1999. Available as SVRC Technical Report 99-07.Google Scholar
  20. 20.
    Christophe Meudec. Automatic Generation of Software Test Cases from Formal Specifications. PhD thesis, Faculty of Science, Queen’s University of Belfast, 1997.Google Scholar
  21. 21.
    F. Bouquet, B. Legeard, and F. Peureux. Constraint logic programming with sets for animation of B formal specifications. In Proceedings of 1st International Conference on Computational Logic (CL’2000). Workshop on Constraint Logic Programming and Software Engineering, LPSE’2000, London, July 2000, pages 62–81, 2000.Google Scholar
  22. 22.
    Fabrice Bouquet, Bruno Legeard, Fabien Peureux, and Paurent Py. Un systéme de résolution de contraintes ensemblistes pour l’évaluation de spécifications B. In Programmation en logique avec contraintes. JFPLC’00. Marseilles, June 2000, pages 125–144, 2000.Google Scholar
  23. 23.
    B. Legeard and F. Peureux. Generation of functional test sequences from B formal specifications-presentation and industrial case-study. In 16 th IEEE International conference on Automated Software Engineering (ASE’2001), 2001.Google Scholar
  24. 24.
    B. Legeard, F. Peureux, and J. Vincent. Automatic generation of functional of test patternes from a formalized smart card model — application to the GSM 11-11 specification. Rapport de fin de contrat (Confidentielle) Tome 1: 79 pages, Tome 2: 418 pages, Convention de recherche Schlumberger R&D Smart Card/LIFC, TFC01-01, Juillet 2000.Google Scholar
  25. 25.
    J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
  26. 26.
    I. MacColl and D. Carrington. Extending the test template framework. In Proceedings of the Third Northern Formal Methods Workshop, Ilkley, UK, Sept. 1998, 1998.Google Scholar
  27. 27.
    I. MacColl, D. Carrington, and P. Stocks. An experiment in specification-based testing. In Proceedings of the 19th Australian Computer Science Conference (ACSC’96), pages 159–168, 1996. Also SVRC Technical Report 96-05.Google Scholar
  28. 28.
    Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors. FM’99 — Formal Methods. Springer-Verlag, 1999. LNCS 1708 (Volume 1).zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Bruno Legeard
    • 1
  • Fabien Peureux
    • 1
  • Mark Utting
    • 2
  1. 1.Laboratoire d’Informatique de Franche-ComteFrance
  2. 2.Visiting from: The University of WaikatoHamiltonNew Zealand

Personalised recommendations