BENEŠ, Nikola, Ivana ČERNÁ, Jiří SOCHOR, Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ. A Case Study in Parallel Verification of Component-Based Systems. In Pre-proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'08). Budapest, Hungary: ETAPS, 2008. s. 35-51. ISSN 1571-0661.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název A Case Study in Parallel Verification of Component-Based Systems
Název česky Případová studie paralelní verifikace komponentových systémů
Autoři BENEŠ, Nikola (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, domácí), Jiří SOCHOR (203 Česká republika, domácí), Pavlína VAŘEKOVÁ (203 Česká republika, domácí) a Barbora ZIMMEROVÁ (203 Česká republika, garant, domácí).
Vydání Budapest, Hungary, Pre-proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'08), od s. 35-51, 17 s. 2008.
Nakladatel ETAPS
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Maďarsko
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/08:00024388
Organizační jednotka Fakulta informatiky
ISSN 1571-0661
Klíčová slova anglicky Component-based systems; formal verification; parallel model checking
Štítky Component-based systems, formal verification, parallel model checking
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Nikola Beneš, Ph.D., učo 72525. Změněno: 17. 12. 2010 12:31.
Anotace
In large component-based systems, the applicability of formal verification techniques to check interaction correctness among components is becoming challenging due to the concurrency of a large number of components. In our approach, we employ parallel LTL-like model checking to handle the size of the model. We present the results of the actual application of the technique to the verification of a complex model of a real system created within the CoCoME Modelling Contest. In this case study, we check the validity of the model and the correctness of the system via checking various temporal properties. We concentrate on the component-specific properties, like local deadlocks of components, and correctness of given use-case scenarios.
Anotace česky
Článek prezentuje výsledky aplikace paralelní verifikace na ověření korektnosti interakce mezi komponentami ve skutečném komponentovém systému definovaném v rámci CoCoME Modelling Contest. V prezentované případové studii se věnujeme jak ověření správnosti modelu, tak i kontrole správnosti systému prostřednictvím verifikace různých temporálních vlastností.
Návaznosti
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET400300504, projekt VaVNázev: Realistická aplikace formálních metod v komponentových systémech
Investor: Akademie věd ČR, Realistická aplikace formálních metod v komponentových systémech
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
VytisknoutZobrazeno: 30. 1. 2023 18:58