Property Oriented Test Case Generation

  • Jean-Claude Fernandez
  • Laurent Mounier
  • Cyril Pachon
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2931)


In this paper we propose an approach to automatically produce test cases allowing to check the satisfiability of a linear property on a given implementation. Linear properties can be expressed by formulas of temporal logic. An observer is built from each formula. An observer is a finite automaton on infinite sequences. Of course, testing the satisfiability of an infinite sequence is not possible. Thus, we introduce the notion of bounded properties. Test cases are generated from a (possibly partial) specification of the IUT and the property to validate is expressed by a parameterised automaton on infinite words. This approach is formally defined, and a practical test generation algorithm is sketched.


Label Transition System Execution Sequence Liveness Property Test Execution Test Graph 
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.
    Belinfante, A., Feenstra, J., de Vries, R., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal Test Automation: a Simple Experiment. In: Csopaki, G., Dibuz, S., Tarnay, K. (eds.) 12th International Workshop on Testing of Communicating Systems. Kluwer Academic Publishers, Dordrecht (1999)Google Scholar
  2. 2.
    Bozga, M., Fernandez, J.-C., Ghirvu, L.: Using static analysis to improve automatic test generation. Tools and Algorithms for Construction and Analysis of Systems, pp. 235–250 (2000)Google Scholar
  3. 3.
    Brinksma, E.: A theory for the derivation of tests. In: Aggarval, S., Sabnani, K. (eds.) Protocol Specification, Testing and Verification VIII, IFIP, pp. 63–74. Elsevier Science Publishers, B.V., North-Holland (1988)Google Scholar
  4. 4.
    Büchi, J.: On a decision method in restricted second order arithmetic. In: van Leeuwan, J., Nagel, E. (eds.) Logic, Methodology and Philosophy of Sciences. Stantford Univ. Press, Stantford (1962)Google Scholar
  5. 5.
    Fernandez, J.-C., Jard, C., Jéron, T., Viho, C.: Using on-the-fly verification techniques for the generation of test suites. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)Google Scholar
  6. 6.
    Groz, R., Jeron, T., Kerbrat, A.: Automated test generation from SDL specifications. In: Dssouli, R., von Bochmann, G., Lahav, Y. (eds.) SDL 1999 The Next Millenium, 9th SDL Forum, Montreal, Quebec, Juin 1999, pp. 135–152. Elsevier, Amsterdam (1999)Google Scholar
  7. 7.
    OSI-Open Systems Interconnection, Information Technology - Open Systems Interconnection Conformance Testing Methodology and Framework - Part 1: General Concept - part 2: Abstract Test Suite Specification - part 3: The Tree and Tabular Combined Notation (TTCN). International Standard ISO/IEC 9646-1/2/3 (1992)Google Scholar
  8. 8.
    Marre, B., Arnould, A.: Test sequences generation from lustre descriptions: Gatel. In: Fifteenth IEEE Int. Conf. on Automated Software Engineering (ASE 2000), September 2000, pp. 229–237. IEEE Computer Society Press, Grenoble (2000)CrossRefGoogle Scholar
  9. 9.
    Mukund, M.: Finite-state automata on infinite input. Technical report (1996)Google Scholar
  10. 10.
    Parissis, I., Vassy, J.: Test des proprietes de surete. In: Actes du colloque Modelisation de Systemes Reactifs (MSR 2001), Hermes, pp. 563–578 (2001)Google Scholar
  11. 11.
    Phalippou, M.: Relations d’implantations et Hypothèses de Test sur des automates à entrées et sorties. Thèse de doctorat. Université de Bordeaux, France (1994)Google Scholar
  12. 12.
    Phalippou, M.: Test sequence using Estelle or SDL structure information. In: FORTE 1994, Berne (October 1994)Google Scholar
  13. 13.
    Thevenod-Fosse, P.: Unit and integration testing of lustre programs: a case study from the nuclear industry. In: 9th European Workshop on Dependable Computing (EWDC-9), Gdansk, Pologne, Mai 14-16, pp. 121–124 (1998)Google Scholar
  14. 14.
    Rabin, M.: Automata o, Infinite Object and Church Problem. Regional Conference series in mathematics, vol. 13. American Mathematical Society, Providence (1972)Google Scholar
  15. 15.
    Raymond, P., Weber, D., Nicollin, X., Halbwach, N.: Automatic testing of reactive systems. In: 19th IEEE Real-Time Systems Symposium, Madrid, Spain (December 1998)Google Scholar
  16. 16.
    Safra, S.: On the complexity of ω-automata, checking. pp. 319–327 (1988)Google Scholar
  17. 17.
    Schmitt, M., Koch, B., Grabowski, J., Hogrefe, D.: Autolink - A Tool for Automatic and Semi-Automatic Test Generation from SDL Specifications. Technical Report A-98-05, Medical University of Lübeck (1998)Google Scholar
  18. 18.
    Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Computation 2(1) (June 1972)Google Scholar
  19. 19.
    Tretmans, J.: Test Generation with Inputs, Outputs, and Quiescence. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 127–146. Springer, Heidelberg (1996)Google Scholar
  20. 20.
    Wolper, P., Vardi, M., Sistla, A.: Reasoning about infinite computation paths. In: 24th IEEE Symposium of Foundations of Computer Science (1983)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Jean-Claude Fernandez
    • 1
  • Laurent Mounier
    • 1
  • Cyril Pachon
    • 1
  1. 1.Verimag, Centre EquationGieresFrance

Personalised recommendations