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

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 χM\! that adds timing without the TA overhead: given an LTS, χ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 ioco if and only if its lifted version conforms under timed tiocoM (2) applying χM\! before or after the standard 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.