An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems

Philip S. Kurtin, Marco J.G. Bekooij

    Research output: Contribution to journalArticleAcademicpeer-review

    5 Citations (Scopus)
    30 Downloads (Pure)


    Component-based and model-based reasonings are key concepts to address the increasing complexity of real-time systems. Bounding abstraction theories allow to create efficiently analyzable models that can be used to give temporal or functional guarantees on non-deterministic and non-monotone implementations. Likewise, bounding refinement theories allow to create implementations that adhere to temporal or functional properties of specification models. For systems in which jitter plays a major role, both best-case and worst-case bounding models are needed.

    In this paper we present a bounding abstraction-refinement theory for real-time systems. Compared to the state-of-the-art TETB refinement theory, our theory is less restrictive with respect to the automatic lifting of properties from component to graph level and does not only support temporal worst-case refinement, but evenhandedly temporal and functional, best-case and worst-case abstraction and refinement.
    Original languageEnglish
    Article number173
    Pages (from-to)173:1-173:20
    Number of pages20
    JournalACM transactions on embedded computing systems
    Issue number5s
    Publication statusPublished - 1 Sept 2017
    Event17th International Conference on Embedded Software, EMSOFT 2017 - Seoul, Korea, Republic of
    Duration: 16 Oct 201718 Oct 2017
    Conference number: 17


    • Denotational & asynchronous component model
    • Bounding abstraction & refinement
    • Worst-case & best-case modeling
    • Real-time system analysis & design
    • Temporal & functional analysis
    • Discrete-event streams
    • The-earlier-the-better
    • Timed dataflow
    • 2023 OA procedure


    Dive into the research topics of 'An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems'. Together they form a unique fingerprint.

    Cite this