An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems (Extended Version)

Philip S. Kurtin, Marco J.G. Bekooij

    Research output: Book/ReportReportAcademic

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

    Compared to the journal version of this paper, we further present several additions in this extended version, such as an inclusion abstraction-refinement theory for the same component model, the definition of the expression of several timed dataflow models in our component model, as well as various formalizations of previously informal definitions and proofs.
    Original languageEnglish
    Place of PublicationEnschede, The Netherlands
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages43
    Publication statusPublished - 24 Oct 2017

    Publication series

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

    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

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

    Cite this