A symbolic framework for model-based testing

L. Frantzen; J. Tretmans; T.A.C. Willemse

doi:10.1007/11940197_3

A symbolic framework for model-based testing

L. Frantzen, J. Tretmans, T.A.C. Willemse

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

68 Citations (Scopus)

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.

Original language	English
Title of host publication	Formal Approaches to Testing and Runtime Verification
Subtitle of host publication	First Combined International Workshops FATES 2006 and RV 2006, Seattle WA, USA, August 15-16, 2006, Revised Selected Papers
Editors	K. Havelund, M. Núñez, G. Rosu, B. Wolff
Place of Publication	Berlin
Publisher	Springer
Chapter	3
Pages	40-54
Number of pages	15
ISBN (Electronic)	978-3-540-49703-5
ISBN (Print)	3-540-49699-8, 978-3-540-49699-1
DOIs	https://doi.org/10.1007/11940197_3
Publication status	Published - 2006

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Volume	4262
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/11940197_3

Cite this

Frantzen, L., Tretmans, J., & Willemse, T. A. C. (2006). A symbolic framework for model-based testing. In K. Havelund, M. Núñez, G. Rosu, & B. Wolff (Eds.), Formal Approaches to Testing and Runtime Verification : First Combined International Workshops FATES 2006 and RV 2006, Seattle WA, USA, August 15-16, 2006, Revised Selected Papers (pp. 40-54). (Lecture Notes in Computer Science (LNCS); Vol. 4262). Springer. https://doi.org/10.1007/11940197_3

Frantzen, L. ; Tretmans, J. ; Willemse, T.A.C. / A symbolic framework for model-based testing. Formal Approaches to Testing and Runtime Verification : First Combined International Workshops FATES 2006 and RV 2006, Seattle WA, USA, August 15-16, 2006, Revised Selected Papers. editor / K. Havelund ; M. Núñez ; G. Rosu ; B. Wolff. Berlin : Springer, 2006. pp. 40-54 (Lecture Notes in Computer Science (LNCS)).

@inproceedings{d736c2a8694c4a98b480bf890bf72b28,

title = "A symbolic framework for model-based testing",

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{\textquoteright} counterparts.",

author = "L. Frantzen and J. Tretmans and T.A.C. Willemse",

year = "2006",

doi = "10.1007/11940197_3",

language = "English",

isbn = "3-540-49699-8",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "40--54",

editor = "K. Havelund and M. N{\'u}{\~n}ez and G. Rosu and B. Wolff",

booktitle = "Formal Approaches to Testing and Runtime Verification",

address = "Germany",

}

Frantzen, L, Tretmans, J & Willemse, TAC 2006, A symbolic framework for model-based testing. in K Havelund, M Núñez, G Rosu & B Wolff (eds), Formal Approaches to Testing and Runtime Verification : First Combined International Workshops FATES 2006 and RV 2006, Seattle WA, USA, August 15-16, 2006, Revised Selected Papers. Lecture Notes in Computer Science (LNCS), vol. 4262, Springer, Berlin, pp. 40-54. https://doi.org/10.1007/11940197_3

A symbolic framework for model-based testing. / Frantzen, L.; Tretmans, J.; Willemse, T.A.C.
Formal Approaches to Testing and Runtime Verification : First Combined International Workshops FATES 2006 and RV 2006, Seattle WA, USA, August 15-16, 2006, Revised Selected Papers. ed. / K. Havelund; M. Núñez; G. Rosu; B. Wolff. Berlin: Springer, 2006. p. 40-54 (Lecture Notes in Computer Science (LNCS); Vol. 4262).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A symbolic framework for model-based testing

AU - Frantzen, L.

AU - Tretmans, J.

AU - Willemse, T.A.C.

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

U2 - 10.1007/11940197_3

DO - 10.1007/11940197_3

M3 - Conference contribution

SN - 3-540-49699-8

SN - 978-3-540-49699-1

T3 - Lecture Notes in Computer Science (LNCS)

SP - 40

EP - 54

BT - Formal Approaches to Testing and Runtime Verification

A2 - Havelund, K.

A2 - Núñez, M.

A2 - Rosu, G.

A2 - Wolff, B.

PB - Springer

CY - Berlin

ER -

Frantzen L, Tretmans J, Willemse TAC. A symbolic framework for model-based testing. In Havelund K, Núñez M, Rosu G, Wolff B, editors, Formal Approaches to Testing and Runtime Verification : First Combined International Workshops FATES 2006 and RV 2006, Seattle WA, USA, August 15-16, 2006, Revised Selected Papers. Berlin: Springer. 2006. p. 40-54. (Lecture Notes in Computer Science (LNCS)). doi: 10.1007/11940197_3

A symbolic framework for model-based testing

Abstract

Publication series

Access to Document

Fingerprint

Cite this