Timed Automata for Modelling Caches and Pipelines

Franck Cassez
(Macquarie University, Sydney, Australia) 		Pablo González de Aledo Marugán
(University of Cantabria, Santander, Spain)

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.

In Rob van Glabbeek, Jan Friso Groote and Peter Höfner: Proceedings Workshop on Models for Formal Analysis of Real Systems (MARS 2015), Suva, Fiji, November 23, 2015, Electronic Proceedings in Theoretical Computer Science 196, pp. 37–45.
Published: 8th November 2015.
ArXived at: http://dx.doi.org/10.4204/EPTCS.196.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org