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.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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 0302-9743
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ěnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2015 05:32.
Anotace
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 VaVNá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
VytisknoutZobrazeno: 9. 6. 2024 07:31