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

Philip Sebastian Kurtin, Marco Jan Gerrit Bekooij

    Research output: Contribution to journalArticleAcademicpeer-review

    3 Citations (Scopus)
    1 Downloads (Pure)

    Abstract

    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
    Volume16
    Issue number5s
    DOIs
    Publication statusPublished - 1 Sep 2017
    Event17th International Conference on Embedded Software, EMSOFT 2017 - Seoul, Korea, Republic of
    Duration: 16 Oct 201718 Oct 2017
    Conference number: 17

    Fingerprint

    Real time systems
    Jitter
    Specifications

    Keywords

    • 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

    Cite this

    @article{17e622d57a664da29ba13201924d2ed4,
    title = "An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems",
    abstract = "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.",
    keywords = "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",
    author = "Kurtin, {Philip Sebastian} and Bekooij, {Marco Jan Gerrit}",
    year = "2017",
    month = "9",
    day = "1",
    doi = "10.1145/3126507",
    language = "English",
    volume = "16",
    pages = "173:1--173:20",
    journal = "ACM transactions on embedded computing systems",
    issn = "1539-9087",
    publisher = "Association for Computing Machinery (ACM)",
    number = "5s",

    }

    An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems. / Kurtin, Philip Sebastian; Bekooij, Marco Jan Gerrit.

    In: ACM transactions on embedded computing systems, Vol. 16, No. 5s, 173, 01.09.2017, p. 173:1-173:20.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

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

    AU - Kurtin, Philip Sebastian

    AU - Bekooij, Marco Jan Gerrit

    PY - 2017/9/1

    Y1 - 2017/9/1

    N2 - 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.

    AB - 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.

    KW - Denotational & Asynchronous Component Model

    KW - Bounding Abstraction & Refinement

    KW - Worst-Case & Best-Case Modeling

    KW - Real-Time System Analysis & Design

    KW - Temporal & Functional Analysis

    KW - Discrete-Event Streams

    KW - The-Earlier-the-Better

    KW - Timed Dataflow

    UR - http://www.scopus.com/inward/record.url?scp=85030680392&partnerID=8YFLogxK

    U2 - 10.1145/3126507

    DO - 10.1145/3126507

    M3 - Article

    VL - 16

    SP - 173:1-173:20

    JO - ACM transactions on embedded computing systems

    JF - ACM transactions on embedded computing systems

    SN - 1539-9087

    IS - 5s

    M1 - 173

    ER -