On conformance testing for timed systems

J. Schmaltz, J. Tretmans

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    40 Citations (Scopus)

    Abstract

    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.
    Original languageEnglish
    Title of host publicationFormal Modeling and Analysis of Timed Systems
    Subtitle of host publication6th International Conference, FORMATS '08, Saint Malo, France, September 15-17, 2008. Proceedings
    EditorsF. Cassez, C. Jard
    Place of PublicationBerlin
    PublisherSpringer
    Chapter18
    Pages250-264
    Number of pages15
    ISBN (Electronic)978-3-540-85778-5
    ISBN (Print)978-3-540-85777-8
    DOIs
    Publication statusPublished - 2008

    Publication series

    NameLecture Notes in Computer Science (LNCS)
    Volume5215
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-9743

    Fingerprint

    Dive into the research topics of 'On conformance testing for timed systems'. Together they form a unique fingerprint.

    Cite this