Towards Verification of Ensemble Based Component Systems

D 2014

Towards Verification of Ensemble Based Component Systems

BARNAT, Jiří, Nikola BENEŠ, Tomáš BUREŠ, Ivana ČERNÁ, Tomáš KEZNIKL et. al.

Základní údaje

Originální název

Towards Verification of Ensemble Based Component Systems

Autoři

BARNAT, Jiří (203 Česká republika, domácí), Nikola BENEŠ (203 Česká republika, domácí), Tomáš BUREŠ (203 Česká republika), Ivana ČERNÁ (203 Česká republika, garant, domácí), Tomáš KEZNIKL (203 Česká republika) a František PLÁŠIL (203 Česká republika)

Vydání

Neuveden, Formal Aspects of Component Software, od s. 41-60, 20 s. 2014

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/14:00073436

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-07601-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-07602-7_5

UT WoS

000342900000005

Klíčová slova anglicky

component-based systems; component ensembles; formal verification

Změněno: 27. 4. 2015 05:32, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

The relatively new domain of Ensemble-Based Component Systems (EBCS) brings a number of important verification challenges that stem mainly from the dynamism of EBCS. In this paper, we elaborate on our previous work on EBCS verification. In particular, we focus on verification of applications based on the DEECo component model – a representative of EBCS – and evaluate it on a real-life case study. Since our verification technique employs a specialized DEECo semantics to make the verification problem tractable, our goal is to investigate the practical relevance of the properties that can be addressed by the verification. Specifically, we compare the specialized semantics with the realistic general semantics of DEECo to identify verification properties that are preserved by the specialized semantics. We further investigate the tractability of verification 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 project ASCENS.

Návaznosti

GAP202/11/0312, projekt VaV

Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)

Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification

Citovat

BARNAT, Jiří, Nikola BENEŠ, Tomáš BUREŠ, Ivana ČERNÁ, Tomáš KEZNIKL a František PLÁŠIL. Towards Verification of Ensemble Based Component Systems. In José Luiz Fiadeiro, Zhiming Liu, Jinyun Xue. Formal Aspects of Component Software. Neuveden: Springer International Publishing, 2014, s. 41-60. ISBN 978-3-319-07601-0. Dostupné z: https://dx.doi.org/10.1007/978-3-319-07602-7_5.

@inproceedings{1132037,
   author = {Barnat, Jiří and Beneš, Nikola and Bureš, Tomáš and Černá, Ivana and Keznikl, Tomáš and Plášil, František},
   address = {Neuveden},
   booktitle = {Formal Aspects of Component Software},
   doi = {http://dx.doi.org/10.1007/978-3-319-07602-7_5},
   editor = {José Luiz Fiadeiro, Zhiming Liu, Jinyun Xue},
   keywords = {component-based systems; component ensembles; formal verification},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-319-07601-0},
   pages = {41-60},
   publisher = {Springer International Publishing},
   title = {Towards Verification of Ensemble Based Component Systems},
   year = {2014}
}

TY  - JOUR
ID  - 1132037
AU  - Barnat, Jiří - Beneš, Nikola - Bureš, Tomáš - Černá, Ivana - Keznikl, Tomáš - Plášil, František
PY  - 2014
TI  - Towards Verification of Ensemble Based Component Systems
PB  - Springer International Publishing
CY  - Neuveden
SN  - 9783319076010
KW  - component-based systems
KW  - component ensembles
KW  - formal verification
N2  - The relatively new domain of Ensemble-Based Component Systems (EBCS) brings a number of important verification challenges that stem mainly from the dynamism of EBCS. In this paper, we elaborate on our previous work on EBCS verification. In particular, we focus on verification of applications based on the DEECo component model – a representative of EBCS – and evaluate it on a real-life case study. Since our verification technique employs a specialized DEECo semantics to make the verification problem tractable, our goal is to investigate the practical relevance of the properties that can be addressed by the verification. Specifically, we compare the specialized semantics with the realistic general semantics of DEECo to identify verification properties that are preserved by the specialized semantics. We further investigate the tractability of verification 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 project ASCENS.
ER  -

BARNAT, Jiří, Nikola BENEŠ, Tomáš BUREŠ, Ivana ČERNÁ, Tomáš KEZNIKL a František PLÁŠIL. Towards Verification of Ensemble Based Component Systems. In José Luiz Fiadeiro, Zhiming Liu, Jinyun Xue. \textit{Formal Aspects of Component Software}. Neuveden: Springer International Publishing, 2014, s.~41-60. ISBN~978-3-319-07601-0. Dostupné z: https://dx.doi.org/10.1007/978-3-319-07602-7\_{}5.

Podrobný výpis o publikaci