Testing multi input-output real-time systems (Extended Version)

L. Brandan Briones, Hendrik Brinksma

    Research output: Book/ReportReportProfessional

    10 Downloads (Pure)

    Abstract

    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
    Place of PublicationEnschede
    PublisherFormal Methods and Tools (FMT)
    Number of pages20
    Publication statusPublished - Sep 2005

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
    No.TR-CTIT-05-40
    ISSN (Print)1381-3625

    Keywords

    • EWI-5729
    • METIS-248101
    • IR-57037

    Cite this

    Brandan Briones, L., & Brinksma, H. (2005). Testing multi input-output real-time systems (Extended Version). (CTIT Technical Report Series; No. TR-CTIT-05-40). Enschede: Formal Methods and Tools (FMT).