Component-Interaction Automata as a Verification-Oriented Component-Based System Specification

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.

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

References:

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

---

Abstract

V originále

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).

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 project	Name: 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 project	Name: 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