Database of Research Tools Developed Using CADP

TorX Architecture for Test Derivation and Execution

Organisation: University of Twente
Eindhoven University of Technology
Philips Research Laboratories

Functionality: Automatic test generation and execution

Tools used: OPEN/CAESAR

Period: 1999

Description: Conformance testing is important for developing reactive systems, since it offers increased confidence in the correctness of the system by means of experimenting with the system implementation. Using formal methods allows to define a precise notion of correctness and to automate the conformance testing process. The Côte-de-Resyste project (a Dutch joint venture of the Universities of Eindhoven and Twente and the industrial partners Philips Research and KPN Research) aims, among other goals, at comparing existing automated test methods and developing open testing tools together with the underlying formal theory.

The TorX environment, developed within the Côte-de-Resyste project, is a tool architecture allowing on-the-fly testing, batch test derivation and batch test execution for different specification formalisms. The main characteristics of TorX are flexibility and openness. Flexibility is obtained by requiring a modular architecture with well-defined interfaces between the components, allowing to replace a component by an improved version or by a component implementing another specification language or implementation relation. Openness is achieved by choosing, when possible, existing (industry standard) interfaces to link the components, thus enabling the integration in TorX of "third party" components that implement these interfaces.

TorX consists of several components (modules): Explorer, Primer, Driver, Adapter, and TTCN storage. The Explorer is an essential component, dependent of the specification language, which offers functions to explore the transition-graph of a specification. The interface used between the Explorer and Primer modules is that provided by OPEN/CAESAR, which offers all the functionalities needed. This allows to obtain an Explorer for LOTOS simply by plugging the CAESAR compiler in the TorX architecture. The TorX environment currently allows automatic test derivation and execution for the LOTOS, PROMELA, and SDL languages. The use of TorX is illustrated by testing a conference protocol described in these specification languages.

Conclusions: The experiments performed with the TorX architecture showed the feasibility of automatic test generation and execution for multiple input languages and/or implementation relations. Both on-the-fly and batch testing are supported. Further work concerns experimenting TorX on other case-studies and considering a larger number of test purposes per case-study. Also, more advanced batch test derivation techniques are needed in order to reduce human intervention for test deriving.

Publications: [Belinfante-Feenstra-Vries-Tretmans-Goga-Feijs-Mauw-Heerink-99] Axel Belinfante, Jan Feenstra, René de Vries, Jan Tretmans, Nicolae Goga, Loe Feijs, Sjouke Mauw, and Lex Heerink. "Formal Test Automation: a Simple Experiment". In G. Csopaki, S. Dibuz, and K. Tarnay, editors, Proceedings of the 12th International Workshop on Testing of Communicating Systems IWTCS'99, pages 179-196, Kluwer Academic Publishers, 1999.

[Tretmans-Belinfante-99] Jan Tretmans and Axel Belinfante. "Automatic testing with formal methods". In Proceedings of the 7th European International Conference on Software Testing, Analysis and Review EuroSTAR'99 (Barcelona, Spain), November 1999.
Axel Belinfante
Tele-Informatics and Open Systems Group (TIOS)
Department of Informatics
P.O. Box 217
NL-7500 AE Enschede
The Netherlands
Tel: +31 53 4893774
Fax: +31 53 4893247

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Thu Jul 17 15:47:33 2014.

Back to the CADP research tools page