Towards Semantics-Based WCET Analysis

From FSL
Jump to: navigation, search

Towards Semantics-Based WCET Analysis
Mihail Asavoae and Dorel Lucanu and Grigore Rosu
WCET'11. 2011
Abstract. This paper proposes the use of formal semantics as a basis for worst-case execution time (WCET) analysis. Specifically, the semantics of a RISC assembly language is formally defined using recent advances in rewrite-based semantics, and then is used to discover and eliminate erroneous execution paths in the context of WCET analysis. This paper makes two novel contributions: (1) it shows that using a formal semantics of the employed language can be practically feasible in WCET analysis (not only theoretically desirable); and (2) it shows that the discovery and elimination of erroneous execution paths can not only improve the WCET estimation, but can also be achieved using off-the-shelf technology for rewrite-based semantics.
PDF, Slides(PDF), Matching Logic, WCET'11, BIB

Personal tools