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.
|Title of host publication||Formal Modeling and Analysis of Timed Systems |
|Subtitle of host publication||6th International Conference, FORMATS '08, Saint Malo, France, September 15-17, 2008. Proceedings|
|Editors||F. Cassez, C. Jard|
|Place of Publication||Berlin|
|Number of pages||15|
|Publication status||Published - 2008|
|Name||Lecture Notes in Computer Science (LNCS)|