Paper Info
Title
Certifying execution time in multicores
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. We present a verification framework for embedded real-time systems that uses the worst-case execution time as safety parameter.The verification mechanism uses the certifying properties of duality theory to check WCET estimates.The verification is performed on embedded systems that have low computational resources.We propose efficient verification of programs running on multicore architectures based on Abstract-Carrying Code.Experimental results demonstrate our claims on verification efficiency for a subset of the Malardalen WCET benchmarks.
Year
DOI
Venue
2015
10.1016/j.scico.2015.06.006
Science of Computer Programming
Keywords
Field
DocType
Abstract interpretation,Abstraction-carrying code,WCET,LP,LR-servers
Functional verification,Programming language,Abstract interpretation,Computer science,Server,Correctness,Denotational semantics,High-level verification,Multi-core processor,Scalability
Journal
Volume
Issue
ISSN
111
P3
0167-6423
Citations 
PageRank 
References 
2
0.36
49
Authors
6
Name
Order
Citations
PageRank
Vitor Rodrigues120.36
Benny Akesson253735.94
Mário Florido312214.44
Simão Melo de Sousa4959.60
João Pedro Pedroso518317.09
Pedro B. Vasconcelos681.12