Informační systém MU
BENEŠ, Nikola, Ivana ČERNÁ, Jiří SOCHOR, Pavlína MORAVCOVÁ VAŘEKOVÁ and Barbora BÜHNOVÁ. A Case Study in Parallel Verification of Component-Based Systems. Electronic Notes in Theoretical Computer Science. Neuveden: Elsevier, 2008, vol. 220, No 2, p. 67-83, 16 pp. ISSN 1571-0661.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name A Case Study in Parallel Verification of Component-Based Systems
Name in Czech Případová studie paralelní verifikace komponentových systémů
Authors BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, belonging to the institution), Jiří SOCHOR (203 Czech Republic, belonging to the institution), Pavlína MORAVCOVÁ VAŘEKOVÁ (203 Czech Republic, belonging to the institution) and Barbora BÜHNOVÁ (203 Czech Republic, guarantor, belonging to the institution).
Edition Electronic Notes in Theoretical Computer Science, Neuveden, Elsevier, 2008, 1571-0661.
Other information
Original language English
Type of outcome Article in a journal
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Hungary
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/08:00024171
Organization unit Faculty of Informatics
Keywords in English Component-based systems; formal verification; parallel model checking
Tags Component-based systems, formal verification, parallel model checking
Tags International impact, Reviewed
Changed by Changed by: RNDr. Nikola Beneš, Ph.D., učo 72525. Changed: 24. 10. 2013 16:19.
Abstract
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.
Abstract (in Czech)
Č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í.
Links
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Research Intents
1ET400300504, research and development projectName: Realistická aplikace formálních metod v komponentových systémech
Investor: Academy of Sciences of the Czech Republic, Information society (National programme of research)
1ET408050503, research and development projectName: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Academy of Sciences of the Czech Republic, Information society (National programme of research)
Displayed: 12. 6. 2021 19:36