Symbolic Test Selection Based on Approximate Analysis

  • Bertrand Jeannet
  • Thierry Jéron
  • Vlad Rusu
  • Elena Zinovieva
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


This paper addresses the problem of generating symbolic test cases for testing the conformance of a black-box implementation with respect to a specification, in the context of reactive systems. The challenge we consider is the selection of test cases according to a test purpose, which is here a set of scenarios of interest that one wants to observe during test execution. Because of the interactions that occur between the test case and the implementation, test execution can be seen as a game involving two players, in which the test case attempts to satisfy the test purpose.

Efficient solutions to this problem have been proposed in the context of finite-state models, based on the use of fixpoint computations. We extend them in the context of infinite-state symbolic models, by showing how approximate fixpoint computations can be used in a conservative way. The second contribution we provide is the formalization of a quality criterium for test cases, and a result relating the quality of a generated test case to the approximations used in the selection algorithm.


Test Generation Test Purpose Test Selection Label Transition System Approximate Analysis 
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.


  1. 1.
    ISO/IEC 9646. Conformance Testing Methodology and Framework (1992)Google Scholar
  2. 2.
    Belinfante, A., Feenstra, J., de Vries, R.G., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: A simple experiment. In: 12th Int. Workshop on Testing of Communicating Systems. Kluwer Academic Publishers, Dordrecht (1999)Google Scholar
  3. 3.
    Benjamin, M., Geist, D., Hartman, A., Mas, G., Smeets, R., Wolfsthal, Y.: A feasibility study in formal coverage driven test generation. In: DAC 1999 (1999)Google Scholar
  4. 4.
    Cousot, P., Cousot, R.: Abstract intrepretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symposium on Principles of Programming Languages, Los Angeles, CA (1977)Google Scholar
  5. 5.
    Frantzen, L., Tretmans, J., Willemse, T.: Test generation based on symbolic specifications. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 1–15. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Grabowski, J., Hogrefe, D., Nahm, R.: Test Case Generation with Test Purpose Specification by MSCs. In: 6th SDL Forum, Darmstadt (Germany). North-Holland, Amsterdam (1993)Google Scholar
  7. 7.
    Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2) (1997)Google Scholar
  8. 8.
    Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 327. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    Jard, C., Jéron, T.: TGV: theory, principles and algorithms. International Journal on Software Tools for Technology Transfer 6 (2004)Google Scholar
  10. 10.
    Jeannet, B.: Dynamic partitioning in linear relation analysis. application to the verification of reactive systems. Formal Methods in System Design 23(1) (2003)Google Scholar
  11. 11.
    Jeannet, B., Jéron, T., Rusu, V., Zinovieva, E.: Symbolic test selection using approximate analysis. Technical Report 1649, INRIA (2004), Available at
  12. 12.
    Jéron, T., Morel, P.: Test generation derived from model-checking. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 108–121. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  13. 13.
    Lee, D., Yannakakis, M.: Principles and Methods of Testing Finite State Machines - A Survey. Proceedings of the IEEE 84(8) (1996)Google Scholar
  14. 14.
    Rusu, V., du Bousquet, L., Jéron, T.: An approach to symbolic test generation. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, p. 338. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    Rusu, V., Marchand, H., Jéron, T.: Verification and symbolic test generation for safety properties. Technical Report 5285, INRIA (2004), Available at
  16. 16.
    Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Software—Concepts and Tools 17(3) (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Bertrand Jeannet
    • 1
  • Thierry Jéron
    • 1
  • Vlad Rusu
    • 1
  • Elena Zinovieva
    • 1
  1. 1.IRISA/INRIARennesFrance

Personalised recommendations