Please use this identifier to cite or link to this item:
Title: Certifying execution time in multicores
Authors: Rodrigues,V
de Sousa,SM
João Pedro Pedroso
Issue Date: 2015
Abstract: This article presents a semantics-based program verification framework for critical embedded real-time systems using the worst-case execution time (WCET) as the safety parameter. The verification algorithm is designed to run on devices with limited computational resources where efficient resource usage is a requirement For this purpose, the framework of abstract-carrying code (ACC) is extended with an additional verification mechanism for linear programming (LP) by applying the certifying properties of duality theory to check the optimality of WCET estimates. Further, the WCET verification approach preserves feasibility and scalability when applied to multicore architectural models. The certifying WCET algorithm is targeted to architectural models based on the ARM instruction set and is presented as a particular instantiation of a compositional data-flow framework supported on the theoretic foundations of denotational semantics and abstract interpretation. The data-flow framework has algebraic properties that provide algorithmic transformations to increase verification efficiency, mainly in terms of verification time. The WCET analysis/verification on multicore architectures applies the formalism of latency-rate (LR.) servers, and proves its correctness in the context of abstract interpretation, in order to ease WCET estimation of programs sharing resources.
metadata.dc.type: article
Appears in Collections:CEGI - Articles in International Journals

Files in This Item:
File Description SizeFormat 
  Restricted Access
1.27 MBAdobe PDFThumbnail
View/Open Request a copy

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.