Certifying execution time in multicores

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Certifying execution time in multicores

Popis výsledku v původním jazyce

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

Název v anglickém jazyce

Certifying execution time in multicores

Popis výsledku anglicky

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

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/EE2.3.30.0034" target="_blank" >EE2.3.30.0034: Podpora zkvalitnění týmů výzkumu a vývoje a rozvoj intersektorální mobility na ČVUT v Praze</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Science of Computer Programming

ISSN

0167-6423

e-ISSN

—

Svazek periodika

111

Číslo periodika v rámci svazku

P3

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

30

Strana od-do

505-534

Kód UT WoS článku

000368556800007

EID výsledku v databázi Scopus

2-s2.0-84940954804