Towards Verification of Ensemble-Based Component Systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F14%3A10144124" target="_blank" >RIV/00216208:11320/14:10144124 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/00216224:14330/14:00073436

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007%2F978-3-319-07602-7_5" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-319-07602-7_5</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-07602-7_5" target="_blank" >10.1007/978-3-319-07602-7_5</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Towards Verification of Ensemble-Based Component Systems

Popis výsledku v původním jazyce

The relatively new domain of Ensemble-Based Component Systems (EBCS) brings a number of important veri?cation challenges that stem mainly from the dynamism of EBCS. In this paper, we elaborate on our previous work on EBCS veri?cation. In particular, we focus on veri?cation of applications based on the DEECo component model - a representative of EBCS - and evaluate it on a real-life case study. Since our veri?cation technique employs a specialized DEECo semantics to make the veri?cation problem tractable, our goal is to investigate the practical relevance of the properties that can be addressed by the veri?cation. Speci?cally, we compare the specialized semantics with the realistic general semantics of DEECo to identify veri?cation properties that are preserved by the specialized semantics. We further investigate the tractability of veri?cation of these properties on a real-life case study from the domain of electrical vehicle navigation - one of the key case studies of the EU FP7 proje

Název v anglickém jazyce

Towards Verification of Ensemble-Based Component Systems

Popis výsledku anglicky

The relatively new domain of Ensemble-Based Component Systems (EBCS) brings a number of important veri?cation challenges that stem mainly from the dynamism of EBCS. In this paper, we elaborate on our previous work on EBCS veri?cation. In particular, we focus on veri?cation of applications based on the DEECo component model - a representative of EBCS - and evaluate it on a real-life case study. Since our veri?cation technique employs a specialized DEECo semantics to make the veri?cation problem tractable, our goal is to investigate the practical relevance of the properties that can be addressed by the veri?cation. Speci?cally, we compare the specialized semantics with the realistic general semantics of DEECo to identify veri?cation properties that are preserved by the specialized semantics. We further investigate the tractability of veri?cation of these properties on a real-life case study from the domain of electrical vehicle navigation - one of the key case studies of the EU FP7 proje

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP202%2F11%2F0312" target="_blank" >GAP202/11/0312: Vývoj a verifikace softwarových komponent v zapouzdřených systémech</a><br>

Návaznosti

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

Rok uplatnění

2014

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 statě ve sborníku

Proceedings of the 10th International Symposium on Formal Aspects of Component Software

ISBN

978-3-319-07601-0

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

18

Strana od-do

41-60

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Nanchang, China

Datum konání akce

28. 10. 2013

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000342900000005