Testing multi input-output real-time systems

L. Brandan Briones, Hendrik Brinksma

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

    20 Citations (Scopus)
    118 Downloads (Pure)


    In formal testing, the assumption of input enabling is typically made. This assumption requires all inputs to be enabled anytime. In addition, the useful concept of quiescence is sometimes applied. Briefly, a system is in a quiescent state when it cannot produce outputs. In this paper, we relax the input enabling assumption, and allow some input sets to be enabled while others remain disabled. Moreover, we also relax the general bound M used in timed systems to detect quiescence, and allow different bounds for different sets of outputs. By considering the tiocoM theory, an enriched theory for timed testing with repetitive quiescence, and allowing the partition of input sets and output sets, we introduce the mtiocoM relation. A test derivation procedure which is nondeterministic and parameterized is further developed, and shown to be sound and complete wrt mtiocoM .
    Original languageUndefined
    Title of host publicationFormal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005
    EditorsK.K. Lau, R. Banach
    Place of PublicationBerlin
    Number of pages16
    ISBN (Print)3 540 29797 9
    Publication statusPublished - Nov 2005
    Event7th International Conference on Formal Engineering Methods, ICFEM 2005 - Manchester, United Kingdom
    Duration: 1 Nov 20054 Nov 2005
    Conference number: 7

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference7th International Conference on Formal Engineering Methods, ICFEM 2005
    Abbreviated titleICFEM
    Country/TerritoryUnited Kingdom


    • EWI-1631
    • IR-54947
    • METIS-229701

    Cite this