Model-based testing from input output symbolic transition systems enriched by program calls and contracts

Imen Boudhiba; Christophe Gaston; Pascale Le Gall; Virgile Prevosto

doi:10.1007/978-3-319-25945-1_3

Model-based testing from input output symbolic transition systems enriched by program calls and contracts

Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prevosto

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

Abstract

An Input Output Symbolic Transition System (IOSTS) specifies all expected sequences of input and output messages of a reactive system. Symbolic execution over this IOSTS then allows to generate a set of test cases that can exercise the various possible behaviors of the system it represents. In this paper, we extend the IOSTS framework with explicit program calls, possibly equipped with contracts specifying what the program is supposed to do. This approach bridges the gap between a model-based approach in which user-defined programs are abstracted away and a code-based approach in which small pieces of code are separately considered regardless of the way they are combined. First, we extend symbolic execution techniques for IOSTS with programs, in order to re-use classical test case generation algorithms. Second, we explore how constraints coming from IOSTS symbolic execution can be used to infer contracts for programs used in the IOSTS.

Original language	English
Title of host publication	Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Proceedings
Editors	Nina Yevtushenko, Khaled El-Fakih, Gerassimos Barlas
Publisher	Springer Verlag
Pages	35-51
Number of pages	17
ISBN (Print)	9783319259444
DOIs	https://doi.org/10.1007/978-3-319-25945-1_3
Publication status	Published - 1 Jan 2015
Externally published	Yes
Event	27th IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2015 - Sharjah and Dubai, United Arab Emirates Duration: 23 Nov 2015 → 25 Nov 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9447
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	27th IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2015
Country/Territory	United Arab Emirates
City	Sharjah and Dubai
Period	23/11/15 → 25/11/15

Keywords

Feasibility
Input output symbolic transition systems
Model-based testing
Program contracts
Symbolic execution

Access to Document

10.1007/978-3-319-25945-1_3

Cite this

Boudhiba, I., Gaston, C., Gall, P. L., & Prevosto, V. (2015). Model-based testing from input output symbolic transition systems enriched by program calls and contracts. In N. Yevtushenko, K. El-Fakih, & G. Barlas (Eds.), Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Proceedings (pp. 35-51). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9447). Springer Verlag. https://doi.org/10.1007/978-3-319-25945-1_3

Boudhiba, Imen ; Gaston, Christophe ; Gall, Pascale Le et al. / Model-based testing from input output symbolic transition systems enriched by program calls and contracts. Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Proceedings. editor / Nina Yevtushenko ; Khaled El-Fakih ; Gerassimos Barlas. Springer Verlag, 2015. pp. 35-51 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e5d1ecfa30e5406380696ae50dcfe34f,

title = "Model-based testing from input output symbolic transition systems enriched by program calls and contracts",

abstract = "An Input Output Symbolic Transition System (IOSTS) specifies all expected sequences of input and output messages of a reactive system. Symbolic execution over this IOSTS then allows to generate a set of test cases that can exercise the various possible behaviors of the system it represents. In this paper, we extend the IOSTS framework with explicit program calls, possibly equipped with contracts specifying what the program is supposed to do. This approach bridges the gap between a model-based approach in which user-defined programs are abstracted away and a code-based approach in which small pieces of code are separately considered regardless of the way they are combined. First, we extend symbolic execution techniques for IOSTS with programs, in order to re-use classical test case generation algorithms. Second, we explore how constraints coming from IOSTS symbolic execution can be used to infer contracts for programs used in the IOSTS.",

keywords = "Feasibility, Input output symbolic transition systems, Model-based testing, Program contracts, Symbolic execution",

author = "Imen Boudhiba and Christophe Gaston and Gall, \{Pascale Le\} and Virgile Prevosto",

note = "Publisher Copyright: {\textcopyright} IFIP International Federation for Information Processing 2015.; 27th IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2015 ; Conference date: 23-11-2015 Through 25-11-2015",

year = "2015",

month = jan,

day = "1",

doi = "10.1007/978-3-319-25945-1\_3",

language = "English",

isbn = "9783319259444",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "35--51",

editor = "Nina Yevtushenko and Khaled El-Fakih and Gerassimos Barlas",

booktitle = "Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Proceedings",

}

Boudhiba, I, Gaston, C, Gall, PL & Prevosto, V 2015, Model-based testing from input output symbolic transition systems enriched by program calls and contracts. in N Yevtushenko, K El-Fakih & G Barlas (eds), Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9447, Springer Verlag, pp. 35-51, 27th IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2015, Sharjah and Dubai, United Arab Emirates, 23/11/15. https://doi.org/10.1007/978-3-319-25945-1_3

Model-based testing from input output symbolic transition systems enriched by program calls and contracts. / Boudhiba, Imen; Gaston, Christophe; Gall, Pascale Le et al.
Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Proceedings. ed. / Nina Yevtushenko; Khaled El-Fakih; Gerassimos Barlas. Springer Verlag, 2015. p. 35-51 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9447).

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

TY - GEN

T1 - Model-based testing from input output symbolic transition systems enriched by program calls and contracts

AU - Boudhiba, Imen

AU - Gaston, Christophe

AU - Gall, Pascale Le

AU - Prevosto, Virgile

N1 - Publisher Copyright: © IFIP International Federation for Information Processing 2015.

PY - 2015/1/1

Y1 - 2015/1/1

N2 - An Input Output Symbolic Transition System (IOSTS) specifies all expected sequences of input and output messages of a reactive system. Symbolic execution over this IOSTS then allows to generate a set of test cases that can exercise the various possible behaviors of the system it represents. In this paper, we extend the IOSTS framework with explicit program calls, possibly equipped with contracts specifying what the program is supposed to do. This approach bridges the gap between a model-based approach in which user-defined programs are abstracted away and a code-based approach in which small pieces of code are separately considered regardless of the way they are combined. First, we extend symbolic execution techniques for IOSTS with programs, in order to re-use classical test case generation algorithms. Second, we explore how constraints coming from IOSTS symbolic execution can be used to infer contracts for programs used in the IOSTS.

AB - An Input Output Symbolic Transition System (IOSTS) specifies all expected sequences of input and output messages of a reactive system. Symbolic execution over this IOSTS then allows to generate a set of test cases that can exercise the various possible behaviors of the system it represents. In this paper, we extend the IOSTS framework with explicit program calls, possibly equipped with contracts specifying what the program is supposed to do. This approach bridges the gap between a model-based approach in which user-defined programs are abstracted away and a code-based approach in which small pieces of code are separately considered regardless of the way they are combined. First, we extend symbolic execution techniques for IOSTS with programs, in order to re-use classical test case generation algorithms. Second, we explore how constraints coming from IOSTS symbolic execution can be used to infer contracts for programs used in the IOSTS.

KW - Feasibility

KW - Input output symbolic transition systems

KW - Model-based testing

KW - Program contracts

KW - Symbolic execution

U2 - 10.1007/978-3-319-25945-1_3

DO - 10.1007/978-3-319-25945-1_3

M3 - Conference contribution

AN - SCOPUS:84952815142

SN - 9783319259444

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 35

EP - 51

BT - Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Proceedings

A2 - Yevtushenko, Nina

A2 - El-Fakih, Khaled

A2 - Barlas, Gerassimos

PB - Springer Verlag

T2 - 27th IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2015

Y2 - 23 November 2015 through 25 November 2015

ER -

Boudhiba I, Gaston C, Gall PL, Prevosto V. Model-based testing from input output symbolic transition systems enriched by program calls and contracts. In Yevtushenko N, El-Fakih K, Barlas G, editors, Testing Software and Systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Proceedings. Springer Verlag. 2015. p. 35-51. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-25945-1_3

Model-based testing from input output symbolic transition systems enriched by program calls and contracts

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this