Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

TGV: theory, principles and algorithms

A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems

  • Special section on high-level test of complex systems
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

This paper presents the TGV tool, which allows for the automatic synthesis of conformance test cases from a formal specification of a (non-deterministic) reactive system. TGV was developed by Irisa Rennes and Verimag Grenoble, with the support of the Vasy team of Inria Rhônes-Alpes. The paper describes the main elements of the underlying testing theory, which is based on a model of transitions system which distinguishes inputs, outputs and internal actions, and is based on the concept of conformance relation. The principles of the test synthesis process, as well as the main algorithms, are explained. We then describe the main characteristics of the TGV tool and refer to some industrial experiments that have been conducted to validate the approach. As a conclusion, we describe some ongoing work on test synthesis.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abramsky S (1987) Observational equivalence as a testing equivalence. Theor Comput Sci 53(3):225–241

    Article  MathSciNet  Google Scholar 

  2. Benjamin M, Geist D, Hartman A, Mas G, Smeets R, Wolfsthal Y (1999) A feasibility study in formal coverage driven test generation. In: 36th Design Automation conference, DAC99, June 1999

  3. Bernot G, Gaudel MC, Marre B (1991) Software testing based on formal specification: a theory and a tool. Softw Eng J 6:387–405

    Article  Google Scholar 

  4. Bozga M, Fernandez J-C, Ghirvu L, Jard C, Jéron T, Kerbrat A, Morel P, Mounier L (2000) Verification and test generation for the SSCOP protocol. J Sci Comput Programm 36(1):27–52

    Article  Google Scholar 

  5. Bozga M, Graf S, Mounier L (2002) IF-2.0: A validation environment for component-based real-time systems. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 343–348

  6. Clarke D, Jéron T, Rusu V, Zinovieva E (2002) STG: a symbolic test generation tool. In: International conference on tools and algorithms for construction and analysis of systems (TACAS2002), Grenoble, France, April 2002. Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York

  7. Clarke E, Emerson EA (1981) Synthesis of synchronisation skeletons for branching time temporal logic. In: Workshop in logic of programs, (Yorktown Heights, NY). Lecture notes in computer science, vol 131. Springer, Berlin Heidelberg New York

  8. De Nicola R, Henessy M (1984) Testing equivalences for processes. Theor Comput Sci 34:83–133

    Article  Google Scholar 

  9. De Vries RG, Tretmans J (2000) On-the-fly conformance testing using Spin. Int J Softw Tools Technol Transf 2(4):382–393

    Article  Google Scholar 

  10. De Vries RG, Tretmans J (2001) Torwards formal test purposes. In: Brinskma E, Tretmans J (eds) Workshop FATES’01: Formal Approaches of Testing of Software. BRICS Notes Series NS-01-4

  11. Doldi L, Encontre V, Fernandez J-C, Jéron T, Le Bricquir S, Texier N, Phalippou M (1996) Assessment of automatic generation methods of conformance test suites in an industrial context. In: Baumgarten B, Burkhardt A, Giessler H-J (eds) IFIP TC6 9th international workshop on testing of communicating systems, September 1996. Chapman & Hall, London

  12. du Bousquet L, Ramangalahy S, Simon SVC, Belinfante A, De Vries RG (2000) Formal test automation: the conference protocol with TGV/TorX. In: Ural H, Probert R, v. Bochmann G (eds) IFIP 13th international conference on testing of communicating systems (TestCom 2000). Kluwer, Dordrecht

  13. Engels A, Feijs L, Mauw S (1997) Test generation for intelligent networks using model-checking. In: Third Workshop TACAS, Enschede, The Netherlands, Lecture notes in computer science, vol 1217. Springer, Berlin Heidelberg New York

  14. Fernandez J-C, Garavel H, Kerbrat A, Mateescu R, Mounier L, Sighireanu M (1996) CADP: A protocol validation and verification toolbox. In: Alur R, Henzinger TA (eds) Proc. CAV’96 New Brunswick, NJ, August 1996. Lecture notes in computer science, vol 1102. Springer, Berlin Heidelberg New York

  15. Fernandez J-C, Jard C, Jéron T, Viho G (1997) An experiment in automatic generation of conformance test suites for protocols with verification technology. Sci Comput Programm 29:123–146. Egalement disponible en rapport de recherche Irisa no 1035 et Inria no 2923

    Article  Google Scholar 

  16. Gaudel M-C, James PR (1999) Testing algebraic data types and processes : a unifying theory. Formal Aspects Comput 10(5–6):436–451

  17. Groz R, Jéron T, Kerbrat A (1999) Automated test generation from SDL specifications. In: Dssouli R, von Bochmann G, Lahav Y (eds) SDL’99 The Next Millenium, 9th SDL Forum, Montréal, Québec, June 1999, pp 135–152. Elsevier, Amsterdam

  18. Ho W-M, Jézéquel J-M, Le Guennec A, Pennaneac’h F (1999) UMLAUT: an extendible UML transformation framework. In: Proc. Automated Software Engineering (ASE’99), Florida, October 1999

  19. ISO (1992) Information Technology – Open Systems Interconnection Conformance Testing Methodology and Framework. International Standard ISO/IEC 9646-1/2/3. Part 1: General Concept – Part 2: Abstract Test Suite Specification – Part 3: The Tree and Tabular Combined Notation (TTCN)

  20. ITU (1996) ISO/IEC JTC1/SC21 WG7, Information Retrieval, Transfer and Management for OSI; Framework: Formal Methods in Conformance Testing. Committee Draft CD 13245-1, ITU-T proposed recommendation Z 500

  21. Jard C (2002) Principles of test synthesis using true-concurrency models. In: König H, Schiferdecker I (eds) Proc. Testcom’2002, Berlin, March 2002

  22. Jard C (2003) Synthesis of distributed testers from true-concurrency models of reactive systems. Int J Inf Softw Technol 45:791–888

    Article  Google Scholar 

  23. Jard C, Jéron T, Kahlouche H, Viho C (1998) Towards automatic distribution of testers for distributed conformance testing. In: FORTE/PSTV’98, Paris, France, November 1998. Chapman & Hall, London

  24. Jard C, Jéron T, Morel P (2000) Verification of test suites. In: TestCom 2000, IFIP TC 6 / WG 6.1, The IFIP 13th international conference on testing of communicating systems, Ottawa, Ontario, Canada, August 2000. Kluwer, Dordrecht

  25. Jéron T, Morel P (1997) Abstraction, τ-réduction et déterminisation à la volée: application à la génération de test. In: CFIP’97, Congrès Francophone sur l’Ingéniérie des Protocoles, Liège, Belgique. Hermes, September

  26. Jéron T, Morel P (1999) Test generation derived from model-checking. In: Halbwachs N, Peled D (eds) CAV’99, Trento, Italy, July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York, pp 108–122

  27. Kahlouche H, Viho C, Zendri M (1998) An industrial experiment in automatic generation of executable test suites for a cache coherency protocol. In: Petrenko A, Yevtushenko N (eds) IFIP TC6 11th international workshop on testing of communicating systems, September. Chapman & Hall, London

  28. Kahlouche H, Viho C, Zendri M (1999) Hardware testing using a communication protocol conformance testing tool. In: Cleaveland WR (ed) Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), March 1999. Lecture notes in computer science, vol 1579. Springer, Berlin Heidelberg New York, pp 315–329

  29. Lee D, Yannakakis M (1996) Principles and methods of testing finite state machines – a survey. Proc IEEE 84(8):1090–1123

    Article  Google Scholar 

  30. Peled D (1994) Combining partial order reductions with on-the-fly model-checking. In: Dill DL (ed) CAV Workshop. Lecture notes in computer science, vol 818. Springer, Berlin Heidelberg New York

  31. Petrenko A (2000) Fault model-driven test derivation from finite state models: annotated bibliography. In: Cassez F, Jard C, Rozoy B, Ryan M (eds) MOVEP’2k MOdelling and VErification of Parallel processes, Nantes, France. Lecture notes in computer science, vol 2067. Springer, Berlin Heidelberg New York, pp 196–205

  32. Phalippou M (1994) Test sequence generation using Estelle or SDL structure information. In: FORTE’94, Berne, October

  33. Rusu V, du Bousquet L, Jéron T (2000) An approach to symbolic test generation. In: Integrated Formal Methods (IFM’00), Dagstuhl, Germany, November 2000. Lecture notes in computer science, vol 1945. Springer, Berlin Heidelberg New York, pp 338–357

  34. Tarjan R (1972) Depth-first search and linear graph algorithms. SIAM J Comput 1:146–160

    Article  MathSciNet  Google Scholar 

  35. Tretmans J (1996) Test generation with inputs, outputs and repetitive quiescence. Softw Concepts Tools 17:103–120

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRISA/ENS Cachan-Bretagne, Campus de Ker Lann, 35170, Bruz Cedex, France

    Claude Jard

  2. IRISA/INRIA, Campus de Beaulieu, 35042, Rennes Cedex, France

    Thierry Jéron

Authors
  1. Claude Jard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thierry Jéron
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Claude Jard.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Jard, C., Jéron, T. TGV: theory, principles and algorithms. Int J Softw Tools Technol Transfer 7, 297–315 (2005). https://doi.org/10.1007/s10009-004-0153-x

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-004-0153-x

Keywords

Search

Navigation