On conformance testing for timed systems
conference paper
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.
Topics
TNO Identifier
953992
ISSN
03029743
ISBN
354085777X
Publisher
Springer
Source title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008, 15 September 2008 through 17 September 2008
Pages
250-264
Files
To receive the publication files, please send an e-mail request to TNO Repository.