An approach for test selection for EFSMs using a theorem prover

Mahadevan Subramaniam, Ling Xiao, Bo Guo, Zoltan Pap

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

This paper describes an automatic approach for selecting tests from a test suite to validate the changes made to an extended finite state machine (EFSM). EFSMs supporting variables over commonly used data types including booleans, numbers, arrays, queues, and records, and communicating with the environment using parameterized messages are considered. Changes to the EFSM add/delete/replace one or more transitions. Tests are described using a sequence of input and output messages with parameter values. We introduce a class of fully-observable tests. The description of a fully-observable test contains all the information to accurately determine the transitions executed by the test. Interaction among the EFSM transitions captured in terms of a compatibility relation is used along with a given test description to automatically identify fully-observable tests. A procedure is described for selecting a test for a given change based on accurately predicting if the test executes the change transition. We then describe how several tests can be simultaneously selected by grouping them based on overlap of their descriptions. The proposed approach has been implemented using a theorem prover and applied to several examples including protocols and web services with encouraging results.

Original languageEnglish (US)
Title of host publicationTesting of Software and Communication Systems - 21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009, Proceedings
Pages146-162
Number of pages17
DOIs
StatePublished - Dec 1 2009
Event21st IFIP International Conference on Testing of Communicating Systems, TESTCOM 2009 and 9th International Workshop on Formal Approaches to Testing of Software, FATES 2009 - Eindhoven, Netherlands
Duration: Nov 2 2009Nov 4 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5826 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st IFIP International Conference on Testing of Communicating Systems, TESTCOM 2009 and 9th International Workshop on Formal Approaches to Testing of Software, FATES 2009
CountryNetherlands
CityEindhoven
Period11/2/0911/4/09

Fingerprint

Finite automata
Theorem
Web services
State Machine
Network protocols
Grouping
Compatibility
Web Services
Queue
Overlap

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Subramaniam, M., Xiao, L., Guo, B., & Pap, Z. (2009). An approach for test selection for EFSMs using a theorem prover. In Testing of Software and Communication Systems - 21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009, Proceedings (pp. 146-162). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5826 LNCS). https://doi.org/10.1007/978-3-642-05031-2_10

An approach for test selection for EFSMs using a theorem prover. / Subramaniam, Mahadevan; Xiao, Ling; Guo, Bo; Pap, Zoltan.

Testing of Software and Communication Systems - 21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009, Proceedings. 2009. p. 146-162 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5826 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Subramaniam, M, Xiao, L, Guo, B & Pap, Z 2009, An approach for test selection for EFSMs using a theorem prover. in Testing of Software and Communication Systems - 21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5826 LNCS, pp. 146-162, 21st IFIP International Conference on Testing of Communicating Systems, TESTCOM 2009 and 9th International Workshop on Formal Approaches to Testing of Software, FATES 2009, Eindhoven, Netherlands, 11/2/09. https://doi.org/10.1007/978-3-642-05031-2_10
Subramaniam M, Xiao L, Guo B, Pap Z. An approach for test selection for EFSMs using a theorem prover. In Testing of Software and Communication Systems - 21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009, Proceedings. 2009. p. 146-162. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-05031-2_10
Subramaniam, Mahadevan ; Xiao, Ling ; Guo, Bo ; Pap, Zoltan. / An approach for test selection for EFSMs using a theorem prover. Testing of Software and Communication Systems - 21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009, Proceedings. 2009. pp. 146-162 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{01befb6ce6c2442faee85bd4c3ce1141,
title = "An approach for test selection for EFSMs using a theorem prover",
abstract = "This paper describes an automatic approach for selecting tests from a test suite to validate the changes made to an extended finite state machine (EFSM). EFSMs supporting variables over commonly used data types including booleans, numbers, arrays, queues, and records, and communicating with the environment using parameterized messages are considered. Changes to the EFSM add/delete/replace one or more transitions. Tests are described using a sequence of input and output messages with parameter values. We introduce a class of fully-observable tests. The description of a fully-observable test contains all the information to accurately determine the transitions executed by the test. Interaction among the EFSM transitions captured in terms of a compatibility relation is used along with a given test description to automatically identify fully-observable tests. A procedure is described for selecting a test for a given change based on accurately predicting if the test executes the change transition. We then describe how several tests can be simultaneously selected by grouping them based on overlap of their descriptions. The proposed approach has been implemented using a theorem prover and applied to several examples including protocols and web services with encouraging results.",
author = "Mahadevan Subramaniam and Ling Xiao and Bo Guo and Zoltan Pap",
year = "2009",
month = "12",
day = "1",
doi = "10.1007/978-3-642-05031-2_10",
language = "English (US)",
isbn = "3642050301",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "146--162",
booktitle = "Testing of Software and Communication Systems - 21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009, Proceedings",

}

TY - GEN

T1 - An approach for test selection for EFSMs using a theorem prover

AU - Subramaniam, Mahadevan

AU - Xiao, Ling

AU - Guo, Bo

AU - Pap, Zoltan

PY - 2009/12/1

Y1 - 2009/12/1

N2 - This paper describes an automatic approach for selecting tests from a test suite to validate the changes made to an extended finite state machine (EFSM). EFSMs supporting variables over commonly used data types including booleans, numbers, arrays, queues, and records, and communicating with the environment using parameterized messages are considered. Changes to the EFSM add/delete/replace one or more transitions. Tests are described using a sequence of input and output messages with parameter values. We introduce a class of fully-observable tests. The description of a fully-observable test contains all the information to accurately determine the transitions executed by the test. Interaction among the EFSM transitions captured in terms of a compatibility relation is used along with a given test description to automatically identify fully-observable tests. A procedure is described for selecting a test for a given change based on accurately predicting if the test executes the change transition. We then describe how several tests can be simultaneously selected by grouping them based on overlap of their descriptions. The proposed approach has been implemented using a theorem prover and applied to several examples including protocols and web services with encouraging results.

AB - This paper describes an automatic approach for selecting tests from a test suite to validate the changes made to an extended finite state machine (EFSM). EFSMs supporting variables over commonly used data types including booleans, numbers, arrays, queues, and records, and communicating with the environment using parameterized messages are considered. Changes to the EFSM add/delete/replace one or more transitions. Tests are described using a sequence of input and output messages with parameter values. We introduce a class of fully-observable tests. The description of a fully-observable test contains all the information to accurately determine the transitions executed by the test. Interaction among the EFSM transitions captured in terms of a compatibility relation is used along with a given test description to automatically identify fully-observable tests. A procedure is described for selecting a test for a given change based on accurately predicting if the test executes the change transition. We then describe how several tests can be simultaneously selected by grouping them based on overlap of their descriptions. The proposed approach has been implemented using a theorem prover and applied to several examples including protocols and web services with encouraging results.

UR - http://www.scopus.com/inward/record.url?scp=70549096178&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70549096178&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-05031-2_10

DO - 10.1007/978-3-642-05031-2_10

M3 - Conference contribution

AN - SCOPUS:70549096178

SN - 3642050301

SN - 9783642050305

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

SP - 146

EP - 162

BT - Testing of Software and Communication Systems - 21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009, Proceedings

ER -