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, Highly Parallel and Distributed Computing Systems
1ET400300504, research and development projectName: Realistická aplikace formálních metod v komponentových systémech
Investor: Academy of Sciences of the Czech Republic, Realistic application of formal methods in component systems
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, Techniques for automatic verification and validation of software nad hardware systems
Type Name Uploaded/Created by Uploaded/Created Rights
A Case Study in Parallel Verification of Component-Based Systems   File version Černá, I. 3/6/2011

Properties

Name
A Case Study in Parallel Verification of Component-Based Systems
Address within IS
https://is.muni.cz/auth/publication/762866/pdmc08_coin.pdf
Address for the users outside IS
https://is.muni.cz/publication/762866/pdmc08_coin.pdf
Address within Manager
https://is.muni.cz/auth/publication/762866/pdmc08_coin.pdf?info
Address within Manager for the users outside IS
https://is.muni.cz/publication/762866/pdmc08_coin.pdf?info
Uploaded/Created
Fri 3/6/2011 13:56, prof. RNDr. Ivana Černá, CSc.

Rights

Right to read
  • anyone on the Internet
  • a concrete person prof. RNDr. Ivana Černá, CSc., učo 1419
  • a concrete person prof. Ing. Jiří Sochor, CSc., učo 2446
  • a concrete person doc. Ing. RNDr. Barbora Bühnová, Ph.D., učo 39394
  • a concrete person Mgr. et Mgr. Pavlína Moravcová Vařeková, učo 4042
  • a concrete person RNDr. Nikola Beneš, Ph.D., učo 72525
Right to upload
 
Right to administer:
  • a concrete person prof. RNDr. Ivana Černá, CSc., učo 1419
  • a concrete person prof. Ing. Jiří Sochor, CSc., učo 2446
  • a concrete person doc. Ing. RNDr. Barbora Bühnová, Ph.D., učo 39394
  • a concrete person Mgr. et Mgr. Pavlína Moravcová Vařeková, učo 4042
  • a concrete person RNDr. Nikola Beneš, Ph.D., učo 72525
Attributes
 

pdmc08_coin.pdf

Application
Open the file
Download file.
Address within IS
https://is.muni.cz/auth/publication/762866/pdmc08_coin.pdf
Address for the users outside IS
https://is.muni.cz/publication/762866/pdmc08_coin.pdf
File type
PDF (application/pdf)
Size
322,4 KB
Hash md5
3e9f77aa0ffac18a14f95866e340f779
Uploaded/Created
Fri 3/6/2011 13:56

pdmc08_coin.txt

Application
Open the file
Download file.
Address within IS
https://is.muni.cz/auth/publication/762866/pdmc08_coin.txt
Address for the users outside IS
https://is.muni.cz/publication/762866/pdmc08_coin.txt
File type
plain text (text/plain)
Size
36,6 KB
Hash md5
ffc34d07264ca128b1db4fcdb672c8de
Uploaded/Created
Fri 3/6/2011 14:07
Print
Report a file uploaded without authorization. Displayed: 26/4/2024 06:08