BRIM, Luboš, Ivana ČERNÁ, Pavlína VAŘEKOVÁ and Barbora ZIMMEROVÁ. Component-Interaction Automata as a Verification-Oriented Component-Based System Specification. In Proceedings of SAVCBS 2005. Ames, USA: Department of Computer Science, Iowa State University, 2005, p. 31-38.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Component-Interaction Automata as a Verification-Oriented Component-Based System Specification
Name in Czech Component-Interaction automaty pro verifikačně orientovanou specifikaci komponentových systémů
Authors BRIM, Luboš (203 Czech Republic, guarantor), Ivana ČERNÁ (203 Czech Republic), Pavlína VAŘEKOVÁ (203 Czech Republic) and Barbora ZIMMEROVÁ (203 Czech Republic).
Edition Ames, USA, Proceedings of SAVCBS 2005, p. 31-38, 2005.
Publisher Department of Computer Science, Iowa State University
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
WWW URL
RIV identification code RIV/00216224:14330/05:00012815
Organization unit Faculty of Informatics
Keywords in English ADLs; Component-Interaction automata; component interaction; verification
Tags ADLs, component interaction, Component-Interaction automata, verification
Tags International impact, Reviewed
Changed by Changed by: doc. Ing. RNDr. Barbora Bühnová, Ph.D., učo 39394. Changed: 29/11/2006 14:53.
Abstract
In the paper, we present a new approach to component interaction specification and verification process which combines the advantages of both architecture description languages (ADLs) at the beginning of the process, and a general formal verification-oriented model connected to verification tools at the end. After examining current general formal models with respect to their suitability for description of component-based systems, we propose a new verification-oriented model and discuss its features. The model is designed to preserve all the interaction properties to provide a rich base for further verification, and allows the system behaviour to be configurable according to the architecture description (bindings among components) and other specifics (type of communication used in the synchronization of components).
Abstract (in Czech)
Práce popisuje nový přístup k specifikaci a verifikaci komponentových systémů, který kombinuje výhody jazyků pro popis architektury (ADL) a možnosti automatického ověřování temporálních vlastností modelů.
Links
GD102/05/H050, research and development projectName: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
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
PrintDisplayed: 15/7/2024 05:10