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

50 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

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

Kurtin, P. S., & Bekooij, M. J. G. (2017). An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems (Extended Version). (CTIT Technical Report Series; No. TR-CTIT-17-06). Enschede, The Netherlands: Centre for Telematics and Information Technology (CTIT).
Kurtin, Philip S. ; Bekooij, Marco J.G. / An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems (Extended Version). Enschede, The Netherlands : Centre for Telematics and Information Technology (CTIT), 2017. 43 p. (CTIT Technical Report Series; TR-CTIT-17-06).
@book{feedd997f91842d790f377cd9fc0520e,
title = "An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems (Extended Version)",
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.",
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 S.} and Bekooij, {Marco J.G.}",
year = "2017",
month = "10",
day = "24",
language = "English",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-17-06",
address = "Netherlands",

}

Kurtin, PS & Bekooij, MJG 2017, An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems (Extended Version). CTIT Technical Report Series, no. TR-CTIT-17-06, Centre for Telematics and Information Technology (CTIT), Enschede, The Netherlands.

An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems (Extended Version). / Kurtin, Philip S.; Bekooij, Marco J.G.

Enschede, The Netherlands : Centre for Telematics and Information Technology (CTIT), 2017. 43 p. (CTIT Technical Report Series; No. TR-CTIT-17-06).

Research output: Book/ReportReportAcademic

TY - BOOK

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

AU - Kurtin, Philip S.

AU - Bekooij, Marco J.G.

PY - 2017/10/24

Y1 - 2017/10/24

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

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

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

M3 - Report

T3 - CTIT Technical Report Series

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

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede, The Netherlands

ER -

Kurtin PS, Bekooij MJG. An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems (Extended Version). Enschede, The Netherlands: Centre for Telematics and Information Technology (CTIT), 2017. 43 p. (CTIT Technical Report Series; TR-CTIT-17-06).