Timed Automata for Modelling Caches and Pipelines
Franck Cassez (Macquarie University, Sydney, Australia), Pablo, Gonz\'alez de Aledo Marug\'an (University of Cantabria, Santander, Spain)
TL;DR
This paper presents a method to model caches and pipelines in binary programs using timed automata to accurately compute worst-case execution times with model-checking.
Contribution
It introduces a timed automaton approach specifically designed for modeling cache and pipeline effects in WCET analysis.
Findings
Provides tight WCET bounds for benchmark programs
Demonstrates effectiveness of timed automata in WCET analysis
Improves accuracy over previous static analysis methods
Abstract
In this paper, we focus on modelling the timing aspects of binary programs running on architectures featuring caches and pipelines. The objective is to obtain a timed automaton model to compute tight bounds for the worst-case execution time (WCET) of the programs using model-checking techniques.
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.