Cooperative Testing of Uncontrollable Timed Systems

Alexandre David, Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen

Research output: Contribution to journalConference article in JournalResearchpeer-review

5 Citations (Scopus)
231 Downloads (Pure)

Abstract

Abstract. This paper deals with targeted testing of timed systems with uncontrollable behavior. The testing activity is viewed as a game between the tester and the system under test (SUT) towards a given test purpose. The SUT is modeled as Timed Game Automaton and the test purpose is specified in Timed CTL formula. We can employ a timed game solver UPPAAL-TIGA to check if the test purpose is ture w.r.t. the model, and if yes, to generate a winning strategy and use it for black-box conformance testing. Specifically, we show that in case the checking yields a negative result, we can still test the SUT against the test purpose as long as the SUT reacts to our moves in a cooperative style. We present an operational framework of cooperative winning strategy generation, test case derivation and execution. The test method is proved to be sound and complete. Preliminary experimental results indicate that this approach is applicable to non-trivial uncontrollable timed systems.
Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Volume220
Issue number1
Number of pages14
ISSN1571-0661
DOIs
Publication statusPublished - Dec 2008
EventFourth Workshop on Model-Based Testing (MBT'08) - Budapest, Hungary
Duration: 30 Mar 200830 Mar 2008

Conference

ConferenceFourth Workshop on Model-Based Testing (MBT'08)
CountryHungary
CityBudapest
Period30/03/200830/03/2008

Fingerprint

Testing
Acoustic waves
Game
Black-box Testing
Conformance Testing
Test Generation
Automata
Experimental Results

Cite this

@inproceedings{d66d7740a26f11dc8188000ea68e967b,
title = "Cooperative Testing of Uncontrollable Timed Systems",
abstract = "Abstract. This paper deals with targeted testing of timed systems with uncontrollable behavior. The testing activity is viewed as a game between the tester and the system under test (SUT) towards a given test purpose. The SUT is modeled as Timed Game Automaton and the test purpose is specified in Timed CTL formula. We can employ a timed game solver UPPAAL-TIGA to check if the test purpose is ture w.r.t. the model, and if yes, to generate a winning strategy and use it for black-box conformance testing. Specifically, we show that in case the checking yields a negative result, we can still test the SUT against the test purpose as long as the SUT reacts to our moves in a cooperative style. We present an operational framework of cooperative winning strategy generation, test case derivation and execution. The test method is proved to be sound and complete. Preliminary experimental results indicate that this approach is applicable to non-trivial uncontrollable timed systems.",
author = "Alexandre David and Larsen, {Kim Guldstrand} and Shuhao Li and Brian Nielsen",
year = "2008",
month = "12",
doi = "10.1016/j.entcs.2008.11.007",
language = "English",
volume = "220",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "1",

}

Cooperative Testing of Uncontrollable Timed Systems. / David, Alexandre; Larsen, Kim Guldstrand; Li, Shuhao; Nielsen, Brian.

In: Electronic Notes in Theoretical Computer Science, Vol. 220, No. 1, 12.2008.

Research output: Contribution to journalConference article in JournalResearchpeer-review

TY - GEN

T1 - Cooperative Testing of Uncontrollable Timed Systems

AU - David, Alexandre

AU - Larsen, Kim Guldstrand

AU - Li, Shuhao

AU - Nielsen, Brian

PY - 2008/12

Y1 - 2008/12

N2 - Abstract. This paper deals with targeted testing of timed systems with uncontrollable behavior. The testing activity is viewed as a game between the tester and the system under test (SUT) towards a given test purpose. The SUT is modeled as Timed Game Automaton and the test purpose is specified in Timed CTL formula. We can employ a timed game solver UPPAAL-TIGA to check if the test purpose is ture w.r.t. the model, and if yes, to generate a winning strategy and use it for black-box conformance testing. Specifically, we show that in case the checking yields a negative result, we can still test the SUT against the test purpose as long as the SUT reacts to our moves in a cooperative style. We present an operational framework of cooperative winning strategy generation, test case derivation and execution. The test method is proved to be sound and complete. Preliminary experimental results indicate that this approach is applicable to non-trivial uncontrollable timed systems.

AB - Abstract. This paper deals with targeted testing of timed systems with uncontrollable behavior. The testing activity is viewed as a game between the tester and the system under test (SUT) towards a given test purpose. The SUT is modeled as Timed Game Automaton and the test purpose is specified in Timed CTL formula. We can employ a timed game solver UPPAAL-TIGA to check if the test purpose is ture w.r.t. the model, and if yes, to generate a winning strategy and use it for black-box conformance testing. Specifically, we show that in case the checking yields a negative result, we can still test the SUT against the test purpose as long as the SUT reacts to our moves in a cooperative style. We present an operational framework of cooperative winning strategy generation, test case derivation and execution. The test method is proved to be sound and complete. Preliminary experimental results indicate that this approach is applicable to non-trivial uncontrollable timed systems.

U2 - 10.1016/j.entcs.2008.11.007

DO - 10.1016/j.entcs.2008.11.007

M3 - Conference article in Journal

VL - 220

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 1

ER -