On conformance testing for timed systems

Conformance testing for labeled transition systems starts with defining when an implementation conforms to its specification. One of the formal theories for model-based testing uses the implementation relation ioco for this purpose. A peculiar aspect of ioco is to consider the absence of outputs as an observable action, named quiescence. Recently a number of real-time extensions of ioco have been proposed in the literature. Quiescence and the observation of arbitrary delays are issues when defining such extensions. We present two new timed implementation relations and show their relation with existing ones. Based on these new definitions and using several examples, we show the subtle differences, and the consequences that small modifications in the definitions can have on the resulting relations. Moreover, we present conditions under which some of these implementation relations coincide. The notion of M-quiescence, i.e., if outputs occur in a system they occur before a delay M, turns out to be important in these conditions.