Abstract
We propose an approach to test whether a system conforms to its specification given in terms of an Input/Output Symbolic Transition System (IOSTS). IOSTSs use data types to enrich transitions with data-based messages and guards depending on state variables. We use symbolic execution techniques both to extract IOSTS behaviours to be tested in the role of test purposes and to ground an algorithm of test case generation. Thus, contrarily to some already existing approaches, our test purposes are directly expressed as symbolic execution paths of the specification. They are finite symbolic subtrees of its symbolic execution. Finally, we give coverage criteria and demonstrate our approach on a running example.
Chapter PDF
Similar content being viewed by others
Keywords
References
Omega 1.2. The Omega Project: Algorithms and Frameworks for Analyzing and Transforming Scientific Programs (1994)
Clarke, L.-A.: A system to generate test data and symbolically execute programs. IEEE Transactions on software engineering 2(3), 215–222 (1976)
Frantzen, L., Tretmans, J., Willemse, T.A.C.: Test generation based on symbolic specifications. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 1–15. Springer, Heidelberg (2005)
Jard, C., Jéron, T.: TGV: theory, principles and algorithms, a tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Software Tools for Technology Transfer (STTT) 6 (October 2004)
Jeannet, B., Jéron, T., Rusu, V., Zinovieva, E.: Symbolic test selection based on approximate analysis. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 349–364. Springer, Heidelberg (2005)
King, J.-C.: A new approach to program testing. In: Proceedings of the international conference on Reliable software, Los Angeles, California, April 1975, vol. 21-23, pp. 228–233 (1975)
Lugato, D., Rapin, N., Gallois, J.-P.: Verification and tests generation for SDL industrial specifications with the AGATHA toolset. In: Petterson, P., Yovine, S. (eds.) Proceedings of the Workshop on Real-Time Tools affiliated to CONCUR 2001, Department of Information Technology UPPSALA UNIVERSITY Box 337, SE-751 05 Sweden (August 2001), ISSN 1404-3203
Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetic. Comptes rendus du premier Congres des Math. des Pays Slaves, 92–101 (1929)
Ramamoorthy, C.-V., Ho, S.-F., Chen, W.-T.: On the automated generation of program test data. IEEE Transactions on software engineering 2(4), 293–300 (1976)
Rapin, N., Gaston, C., Lapitre, A., Gallois, J.-P.: Behavioural unfolding of formal specifications based on communicating automata. In: Proceedings of first Workshop on Automated technology for verification and analysis, Taiwan (2003)
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, pp. 338–357. Springer, Heidelberg (2000)
Tretmans, J.: Conformance Testing with Labelled Transition Systems: Implementation Relations and Test Generation. Computer Networks and ISDN Systems 29, 49–79 (1996)
Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Software—Concepts and Tools 17(3), 103–120 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Gaston, C., Le Gall, P., Rapin, N., Touil, A. (2006). Symbolic Execution Techniques for Test Purpose Definition. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds) Testing of Communicating Systems. TestCom 2006. Lecture Notes in Computer Science, vol 3964. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11754008_1
Download citation
DOI: https://doi.org/10.1007/11754008_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34184-0
Online ISBN: 978-3-540-34185-7
eBook Packages: Computer ScienceComputer Science (R0)