Time for Quiescence: Modelling quiescent behaviour in testing via time-outs in timed automata

TL;DR

This paper introduces a simple method to model quiescence in testing by adding a timing mechanism to labelled transition systems, enabling formal analysis without the complexity of full timed automata.

Contribution

It presents a lifting operator that adds timing to LTSs for quiescence detection, aligning conformance testing with timed automata without extra overhead.

Findings

Conformance under ioco is equivalent to conformance under timed tioco_M after lifting.

Applying the lifting operator before or after test generation yields identical test sets.

Lifted and original test suites produce the same verdicts for all implementations.

Abstract

Model-based testing (MBT) derives test suites from a behavioural specification of the system under test. In practice, engineers favour simple models, such as labelled transition systems (LTSs). However, to deal with quiescence - the absence of observable output - in practice, a time-out needs to be set to conclude observation of quiescence. Timed MBT exists, but it typically relies on the full arsenal of timed automata (TA). We present a lifting operator $\chi^{\scriptstyle M}\!$ that adds timing without the TA overhead: given an LTS, $\chi^{\scriptstyle M}\!$ introduces a single clock for a user chosen time bound $M>0$ to declare quiescence. In the timed automaton, the clock is used to model that outputs should happen before the clock reaches value $M$, while quiescence occurs exactly at time $M$. This way we provide a formal basis for the industrial practice of choosing a time-out to conclude quiescence. Our contributions are threefold: (1) an implementation conforms under $\mathbf{ioco}$ if and only if its lifted version conforms under timed $\mathbf{tioco_M}$ (2) applying $\chi^{\scriptstyle M}\!$ before or after the standard $\mathbf{ioco}$ test-generation algorithm yields the same set of tests, and (3) the lifted TA test suite and the original LTS test suite deliver identical verdicts for every implementation.