×

zbMATH — the first resource for mathematics

On abstractions for timing analysis in the \(\mathbb{K}\) framework. (English) Zbl 1367.68058
Peña, 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).
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.
For the entire collection see [Zbl 1250.68046].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Software:
K-Maude
PDF BibTeX XML Cite
Full Text: DOI