Abstract
The starting point for Model-Based Testing is an implementation relation that formally defines when a formal model representing the System Under Test conforms to a formal model constituting its specification. An implementation relation for the formalism of Labelled Transition Systems is ioco. For ioco several test generation algorithms and test tools have been built. In this paper we define a framework for the symbolic implementation relation sioco which lifts ioco to Symbolic Transition Systems. These are transition systems with an explicit notion of data and data-dependent control flow. The introduction of symbolism avoids the state-space explosion during test generation, and it preserves the information present in data definitions and constraints for use during the test selection process. We show the soundness and completeness of the symbolic notions w.r.t. their underlying Labelled Transition Systems’ counterparts.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Belinfante, A., Feenstra, J., de Vries, R.G., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: A simple experiment. In: Csopaki, G., Dibuz, S., Tarnay, K. (eds.) IWTCS 1999, pp. 179–196. Kluwer Academic Publishers, Dordrecht (1999)
Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language Lotos. Computer Networks 14(1), 25–59 (1988)
Broy, M., Jonsson, B., Katoen, J.P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472, pp. 277–279. Springer, Heidelberg (2005)
Brucker, A.D., Wolff, B.: Symbolic test case generation for primitive recursive functions. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 16–32. Springer, Heidelberg (2005)
Ehrig, H., Mahr, B., Cornelius, F., Große-Rhode, M., Zeitz, P.: Mathematisch-strukturelle Grundlagen der Informatik, 2nd edn. Springer, Heidelberg (2001)
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)
Gaston, C., Le Gall, P., Rapin, N., Touil, A.: Symbolic execution techniques for test purpose definition. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 1–18. Springer, Heidelberg (2006)
Goga, N.: Comparing torx, autolink, tgv and uio test algorithms. In: Reed, R., Reed, J. (eds.) SDL 2001. LNCS, vol. 2078, pp. 379–402. Springer, Heidelberg (2001)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)
Jard, C., Jéron, T.: TGV: theory, principles and algorithms. In: IDPT 2002. Society for Design and Process Science (2002)
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, pp. 228–233. ACM Press, New York (1975)
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - A survey. Proceedings of the IEEE 84, 1090–1126 (1996)
Object Management Group. UML 2.0 Superstructure Specification, ptc/03-08-02 edition. Adopted Specification
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.: 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 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Frantzen, L., Tretmans, J., Willemse, T.A.C. (2006). A Symbolic Framework for Model-Based Testing. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds) Formal Approaches to Software Testing and Runtime Verification. FATES RV 2006 2006. Lecture Notes in Computer Science, vol 4262. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11940197_3
Download citation
DOI: https://doi.org/10.1007/11940197_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-49699-1
Online ISBN: 978-3-540-49703-5
eBook Packages: Computer ScienceComputer Science (R0)