A symbolic framework for model-based testing

被引:0
作者
Frantzen, L. [1 ]
Tretmans, J. [2 ]
Willemse, T. A. C. [2 ]
机构
[1] CNR, Ist Sci & Tecnol Informaz Alessandro Faedo, I-56100 Pisa, Italy
[2] Radboud Univ Nijmegen, Inst Comp & Informat Sci, NL-6525 ED Nijmegen, Netherlands
来源
FORMAL APPROACHES TO SOFTWARE TESTING AND RUNTIME VERIFICATION | 2006年 / 4262卷
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页码:40 / +
页数:2
相关论文
共 16 条
  • [11] Jeannet B, 2005, LECT NOTES COMPUT SC, V3440, P349
  • [12] KING JC, 1975, P INT C REL SOFTW, P228
  • [13] Principles and methods of testing finite state machines - A survey
    Lee, D
    Yannakakis, M
    [J]. PROCEEDINGS OF THE IEEE, 1996, 84 (08) : 1090 - 1123
  • [14] *OBJ MAN GROUP, PTC030802 OBJ MAN GR
  • [15] Rusu V, 2000, LECT NOTES COMPUT SC, V1945, P338
  • [16] Tretmans J, 1996, SOFTWARE-CONC TOOL, V17, P103