Towards Verification of Ensemble-Based Component Systems
The result's identifiers
Result code in 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>
Alternative codes found
RIV/00216224:14330/14:00073436
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Towards Verification of Ensemble-Based Component Systems
Original language description
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
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GAP202%2F11%2F0312" target="_blank" >GAP202/11/0312: Software Components in Embedded Systems: Development and Verification</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2014
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
Article name in the collection
Proceedings of the 10th International Symposium on Formal Aspects of Component Software
ISBN
978-3-319-07601-0
ISSN
0302-9743
e-ISSN
—
Number of pages
18
Pages from-to
41-60
Publisher name
Springer
Place of publication
Berlin
Event location
Nanchang, China
Event date
Oct 28, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000342900000005