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

Philip S. Kurtin; Marco J.G. Bekooij

doi:10.1145/3126507

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

Philip S. Kurtin, Marco J.G. Bekooij

Research output: Contribution to journal › Article › Academic › peer-review

6 Citations (Scopus)

67 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 language	English
Article number	173
Pages (from-to)	173:1-173:20
Number of pages	20
Journal	ACM transactions on embedded computing systems
Volume	16
Issue number	5s
DOIs	https://doi.org/10.1145/3126507
Publication status	Published - 1 Sept 2017
Event	17th International Conference on Embedded Software, EMSOFT 2017 - Seoul, Korea, Republic of Duration: 16 Oct 2017 → 18 Oct 2017 Conference number: 17

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
2023 OA procedure

Access to Document

10.1145/3126507

ArticleFinal published version, 755 KBLicence: Taverne

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, 2023 OA procedure",

author = "Kurtin, {Philip S.} and Bekooij, {Marco J.G.}",

year = "2017",

month = sep,

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",

number = "5s",

note = "17th International Conference on Embedded Software, EMSOFT 2017, EMSOFT ; Conference date: 16-10-2017 Through 18-10-2017",

}

TY - JOUR

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

AU - Kurtin, Philip S.

AU - Bekooij, Marco J.G.

N1 - Conference code: 17

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

KW - 2023 OA procedure

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

U2 - 10.1145/3126507

DO - 10.1145/3126507

M3 - Article

SN - 1539-9087

VL - 16

SP - 173:1-173:20

JO - ACM transactions on embedded computing systems

JF - ACM transactions on embedded computing systems

IS - 5s

M1 - 173

T2 - 17th International Conference on Embedded Software, EMSOFT 2017

Y2 - 16 October 2017 through 18 October 2017

ER -

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

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

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

Cite this