\input zb-basic
\input zb-ioport
\iteman{io-port 06101669}
\itemau{As\u{a}voae, Mihail; As\u{a}voae, Irina M\u{a}riuca; Lucanu, Dorel}
\itemti{On abstractions for timing analysis in the $\mathbb{K}$ framework.}
\itemso{Pe\~na, Ricardo (ed.) et al., Foundational and practical aspects of resource analysis. Second international workshop, FOPARA 2011, Madrid, Spain, May 19, 2011. Revised selected papers. Berlin: Springer (ISBN 978-3-642-32494-9/pbk). Lecture Notes in Computer Science 7177, 90-107 (2012).}
\itemab
Summary: Low-level WCET analysis consists of two subproblems: the path analysis and the processor behavior analysis. A successful approach uses an integer linear programming (ILP) solution for the former and an abstract interpretation (AI) solution for the latter. This paper advocates, for this particular ILP + AI approach, the use of a specialized rewrite-based framework, called $\mathbb{K}$. We define this methodology in $\mathbb{K}$, starting from the formal executable semantics of the language and the concrete, parametric, description of the underlying micro-architecture (i.e. instruction cache). The latter is designed to facilitate specification reusability in the abstraction definition. We also analyze the definitional methodology of the ILP + AI approach, from the design perspective.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-32495-6\_6}
\end