Cooperative Testing of Timed Systems

This paper deals with targeted testing of timed systems whose models may have 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 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 of the SUT implementation. Specifically, we show that in case the checking yields a negative result, we can still test the SUT implementation against the test purpose as long as the SUT implementation 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 timed systems.