Performance Evaluation of Components Using a Granularity-based Interface Between Real-Time Calculus and Timed Automata
Karine Altisen, Yanhong Liu, Matthieu Moy

TL;DR
This paper introduces a granularity-based interface framework that accelerates the analysis of timed automata components in real-time systems by abstracting models at multiple granularities to balance precision and analysis speed.
Contribution
It proposes a novel framework that uses multi-granularity abstraction and RTC theory to reduce analysis time of TA components while maintaining accuracy.
Findings
Framework speeds up analysis of TA components.
Tradeoff between analysis precision and time achieved.
Bounds on output streams derived efficiently.
Abstract
To analyze complex and heterogeneous real-time embedded systems, recent works have proposed interface techniques between real-time calculus (RTC) and timed automata (TA), in order to take advantage of the strengths of each technique for analyzing various components. But the time to analyze a state-based component modeled by TA may be prohibitively high, due to the state space explosion problem. In this paper, we propose a framework of granularity-based interfacing to speed up the analysis of a TA modeled component. First, we abstract fine models to work with event streams at coarse granularity. We perform analysis of the component at multiple coarse granularities and then based on RTC theory, we derive lower and upper bounds on arrival patterns of the fine output streams using the causality closure algorithm. Our framework can help to achieve tradeoffs between precision and analysis…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsReal-Time Systems Scheduling · Formal Methods in Verification · Software System Performance and Reliability
