Certifying execution time in multicores

• 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.

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   (LRLR) servers, and proves its correctness in the context of abstract interpretation, in order to ease WCET estimation of programs sharing resources.