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 -