Automatic amortised worst-case execution time analysis

Our research focuses on formally bounded WCET analysis, where we aim to provide ab-solute guarantees on execution time bounds. In this paper, we describe how amortisation can be used to improve the quality of the results that are obtained from a fully-automatic and formally guaranteed WCET analysis, by delivering analy-sis results that are parameterised on specific in-put patterns and which take account of relations between these patterns. We have implemented our approach to give a tool that is capable of predicting execution costs for a typical embedded system development platform, a Renesas board with a Renesas M32C/85U processor. We show that not only is the amortised approach applica-ble in theory, but that it can be applied auto-matically to yield good WCET results.