Certifying execution time in multicores
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F15%3A00232408" target="_blank" >RIV/68407700:21230/15:00232408 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1016/j.scico.2015.06.006" target="_blank" >http://dx.doi.org/10.1016/j.scico.2015.06.006</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.scico.2015.06.006" target="_blank" >10.1016/j.scico.2015.06.006</a>
Alternative languages
Result language
angličtina
Original language name
Certifying execution time in multicores
Original language description
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 ofduality 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
Czech name
—
Czech description
—
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/EE2.3.30.0034" target="_blank" >EE2.3.30.0034: Support of inter-sectoral mobility and quality enhancement of research teams at Czech Technical University in Prague</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2015
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Science of Computer Programming
ISSN
0167-6423
e-ISSN
—
Volume of the periodical
111
Issue of the periodical within the volume
P3
Country of publishing house
NL - THE KINGDOM OF THE NETHERLANDS
Number of pages
30
Pages from-to
505-534
UT code for WoS article
000368556800007
EID of the result in the Scopus database
2-s2.0-84940954804