Testing from Formal Specifications, a Generic Approach

  • Marie-Claude Gaudel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2043)


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.


Selection Hypothesis Observable Action Exhaustive Test Conformance Relation Algebraic Specification 
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.
    Goodenough, J. B., Gerhart, S.: Toward a Theory of Test Data Selection. IEEE Transactions on Software Engineering, vol. SE-1,n° 2, (1975) 156–173.MathSciNetGoogle Scholar
  2. 2.
    Howden, W.: Errors, Design Properties, and Functional Program Tests. in Chandraskaran, B., Radicchi, S. (eds.), Computer Program Testing, North-Holland (1981).Google Scholar
  3. 3.
    Chow, T. S.: Testing Software Design Modeled by Finite-State Machines. IEEE Transactions on Software Engineering, vol. SE-4,n° 3, (1978) 178–187.CrossRefGoogle Scholar
  4. 4.
    Gannon, J., McMullin, P., Hamlet, R.: Data Abstraction Implementation, Specification and Testing. ACM Transactions on Programming Languages and Systems, vol. 3,n°3, (1981) 211–223.CrossRefGoogle Scholar
  5. 5.
    Bernot, G., Gaudel, M.-C., Marre B.: Software Testing based on Formal Specifications: a theory and a tool. Software Engineering Journal, vol. 6,n° 6, (1991) 387–405.CrossRefGoogle Scholar
  6. 6.
    Dick, J., Faivre, A.: Automating the Generation and Sequencing of test cases from model-based specifications. FME’93, LNCS n°670, Springer-Verlag (1993) 268–284.Google Scholar
  7. 7.
    Brinksma, E., A Theory for the Derivation of Tests, 8th International Conference on Protocol Specification, Testing and Verification, Atlantic City, North-Holland (1988).Google Scholar
  8. 8.
    Pitt, D.H., Freestone, D.: The Derivation of Conformance Tests from LOTOS specifications, IEEE Transactions on Software Engineering, vol. 16,n°12, (1990) 1337–1343.CrossRefGoogle Scholar
  9. 9.
    Chen, H. Y., Tse, T. H., Chan, F. T., Chen, T. Y.: In Black and White: an Integrated Approach to Class-level Testing of Object-Oriented Programs. ACM transactions on Software Engineering and Methodology, vol. 7,n° 3, (1998) 250–295.CrossRefGoogle Scholar
  10. 10.
    Littlewood, B., Popov, P. T., Strigini, L., Shryane, N.: Modeling the Effects of Combining Diverse Software Fault Detection Techniques. IEEE Transactions on Software Engineering, vol. 26,n° 12, (2000) 1157–1167.CrossRefGoogle Scholar
  11. 11.
    Gaudel, M.-C., James, P. R.: Testing Algebraic Data Types and Processes: a unifying theory. Formal Aspects of Computing, 10(5-6), (1999) 436–451.CrossRefGoogle Scholar
  12. 12.
    James, P. R., Endler M., Gaudel M.-C.: Development of an Atomic Broadcast Protocol using LOTOS. Software Practice and Experience, 29(8), (1999) 699–719.CrossRefGoogle Scholar
  13. 13.
    Bernot, G., Gaudel, M.-C, Marre, B.: A Formal Approach to Software Testing. 2nd International Conference on Algebraic Methodology and Software Technology, AMAST, Iowa City, 1991, Workshops in Computing Series, Springer-Verlag, (1992).Google Scholar
  14. 14.
    Phalippou, M.: Relations d’Implantation et Hypothèses de Test sur des Automates à Entrées et Sorties. Thèse de l’université de Bordeaux 1, (1994).Google Scholar
  15. 15.
    Kreowski, H.-J. ed.: Foundations of Algebraic Specifications. Springer-Verlag, (1999).Google Scholar
  16. 16.
    ISO: LOTOS, a Formal Description Technique based on the Temporal Ordering of Observational Behaviours. Technical report 8807, International Standards Organisation (1989).Google Scholar
  17. 17.
    Marre, B.: Toward Automatic Test Data Selection using Algebraic Specifications and Logic Programming. International Conference on Logic Programming, MIT Press (1991) 202–219.Google Scholar
  18. 18.
    Marre, B.: LOFT, a Tool for Assisting Selection of Test Data Sets from Algebraic Specifications. LNCS n°915, Springer-Verlag (1995) 799–800.Google Scholar
  19. 19.
    Le Gall, P., Arnould, A.: Formal Specifications and Test: Correctness and Oracle. LNCS n°1130, Springer-Verlag (1996) 342–358.Google Scholar
  20. 20.
    Doong, R.-K., Frankl, P. G.: The ASTOOT Approach to Testing Object-Oriented Programs. ACM Transactions on Software Engineering and Methodology, 3(2), (1994) 101–130.CrossRefGoogle Scholar
  21. 21.
    Machado, P. D. L: On Oracles for Interpreting Test Results against Algebraic Specifications. LNCS n° 1548, Springer-Verlag (1998) 502–518.Google Scholar
  22. 22.
    Dauchy, P., Gaudel, M.-C, Marre, B.: Using Algebraic Specifications in Software Testing: a Case Study on the Software of an Automatic Subway. Journal of Systems and Software, 21(3), (1993) 229–244.CrossRefGoogle Scholar
  23. 23.
    Marre, B., Thévenod-Fosse, P., Waeselink, H., Le Gall, P., Crouzet, Y.: An Experimental Evaluation of Formal Testing and Statistical Testing, SAFECOMP’92, Zurich, Oct. 1992.Google Scholar
  24. 24.
    Barbey, S., Buchs, D.: Testing Ada abstract data types using formal specifications, in Ada in Europe, 1st Int. Eurospace-Ada-Europe Symposium. LNCS n°887, Springer-Verlag, (1994) 76–89.Google Scholar
  25. 25.
    Arnold, A., Gaudel, M.-C., Marre, B.: An Experiment on the Validation of a Specification by Heterogeneous Formal Means: the Transit Node. 5th IFIP Working Conference on Dependable Computing for Critical Applications, (1995) 24–34.Google Scholar
  26. 26.
    Hennessy, M.: An Algebraic Theory of Processes. MIT Press (1988).Google Scholar
  27. 27.
    Tretmans, J.: A Formal Approach to Conformance Testing. 6th Int. Workshop on Protocol Test Systems, IFIP Transactions C-19, North-Holland, (1994) 257–276.Google Scholar
  28. 28.
    Birman, K. P.: Building Secure and Reliable Network Applications. Manning Publications (1997)Google Scholar
  29. 29.
    Auerbach, J. S. et al.: High-level Language Support for Programming Distributed Systems. IEEE Int. Conf. on Computer Languages, IEEE, (1992) 320–330.Google Scholar
  30. 30.
    Péraire, C., Barbey, S., Buchs, D.: Test Selection for Object-Oriented Software Based on Formal Specifications. IFIP Working Conference on Programming Concepts and Methods, Shelter Island, USA, Chapman & Hall, (1998) 385–403.Google Scholar
  31. 31.
    Marre, B., Arnould, A.: Test Sequences Generation from LUSTRE Descriptions: GATEL. IEEE Automated Software Engineering Conference, IEEE, (2000) 229–237.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Marie-Claude Gaudel
    • 1
  1. 1.L.R.IUniversité de Paris-Sud et CNRSOrsay-cedexFrance

Personalised recommendations