Abstract
In this paper we attempt to demonstrate that on-the-fly techniques, developed in the context of verification, can help in deriving test suites. Test purposes are used in practice to select test cases according to some properties of the specification. We define a consistency pre-order linking test purposes and specifications. We give a set of rules to check this consistency and to derive a complete test case with preamble, postamble, verdicts and timers. The algorithm, which implements the construction rules, is based on a depth first traversal of a synchronous product between the test purpose and the specification. We shortly relate our experience on an industrial protocol with TGV, a first prototype of the algorithm implemented as a component of the C ADP toolbox.
This work has been partially supported by an industrial contract with Verilog in a study for the french DGA (Direction Générale pour l'Armement)
Chapter PDF
Similar content being viewed by others
References
B. Algayres, Y. Lejeune, F. Hugonnet, and F. Hantz. The AVALON project: A VALidatiON Environment For SDL/MSC Descriptions. In 6th SDL Forum, Darmstadt, 1993.
E. Brinksma. A theory for the derivation of tests. In S. Aggarval and K. Sabnani, editors, Protocol Specification, Testing and Verification VIII, IFIP, pages 63–74. Elsevier Science Publishers, B.V., North-Holland, 1988.
CCITT/SGx/WP3-1, Specification and Description Language, SDL. CCITT Recommendation Z.100, 1988.
M. Clatin, R. Groz, M. Phalippou, and R. Thummel. Two approaches linking a test generation tool with verification techniques. In A. Cavalli and S. Budkowski, editors, 8th Int. Workshop on Protocols Test Systems, Evry, France, pages 159–174, September 1995.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In E.M. Clarke and R.P. Kurshan, editors, Computer Aided Verification, 2nd International Workshop, CAV'90, New Brunswick, NJ, USA. Springer Verlag, LNCS 531, 1990.
J.-C. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, and J. Sifakis. A Tool Box for the Verification of Lotos Programs. In 14th International Conference on Software Engineering, Melbourne, Australia, May 1992.
J.-C. Fernandez, C. Jard, T. Jéron, and G. Viho. An experiment in automatic generation of test suites for protocoles with verification technology. under revision for SCP, 1996.
J.-C. Fernandez and L. Mounier. On the fly verification of behavioral equivalences and preorders. In K.G. Larsen and A. Skou, editors, Computer Aided Verification, 3rd International Workshop, CAV'91, Aalborg, Denmark, pages 181–190. Springer Verlag, LNCS 575, June 1991.
J.-C. Fernandez, L. Mounier, C. Jard, and T. Jéron. On-the-fly verification of finite transition systems. Formal Methods in System Design, 1:251–273, 1992. Kluwer Academic Publishers.
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.
C. Jard and T. Jéron. On-line model-checking for finite linear temporal logic specifications. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, pages 275–285. Springer-Verlag, LNCS 407, June 1989.
C. Jard and T. Jéron. Bounded memory algorithms for verification on the fly. In K.G. Larsen and A. Skou, editors, Computer Aided Verification, 3rd International Workshop, CAV'91, Aalborg, Denmark, pages 192–202. Springer Verlag, LNCS 575, June 1991.
M. Phalippou. Relations d'implantations et Hypothèses de Test sur des automates à entrées et sorties. Thèse de doctorat, Université de Bordeaux, France, 1994.
M. Phalippou. Test sequence using Estelle or SDL structure information. In FORTE'94, Berne, October 1994.
J. Tretmans. Testing Labelled Transition Systems with Inputs and Outputs. In A. Cavalli and S. Budkowski, editors, 8th Int. Workshop on Protocols Test Systems, Evry, France, pages 461–476, September 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fernandez, J.C., Jard, C., Jéron, T., Viho, C. (1996). Using on-the-fly verification techniques for the generation of test suites. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_82
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_82
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive