Component-Interaction Automata Approach (CoIn)

ZIMMEROVÁ, Barbora, Pavlína VAŘEKOVÁ, Nikola BENEŠ, Ivana ČERNÁ, Luboš BRIM and Jiří SOCHOR. Component-Interaction Automata Approach (CoIn). In The Common Component Modeling Example: Comparing Software Component Models. Berlin / Heidelberg, Germany: Springer Verlag, 2008, p. 146-176. LNCS 5153. ISBN 978-3-540-85288-9.

Basic information

• Original name: Component-Interaction Automata Approach (CoIn)
• Name in Czech: Přístup využívající Component-Interaction automaty
• Authors: ZIMMEROVÁ, Barbora (203 Czech Republic, guarantor), Pavlína VAŘEKOVÁ (203 Czech Republic), Nikola BENEŠ (203 Czech Republic), Ivana ČERNÁ (203 Czech Republic), Luboš BRIM (203 Czech Republic) and Jiří SOCHOR (203 Czech Republic).
• Edition: Berlin / Heidelberg, Germany, The Common Component Modeling Example: Comparing Software Component Models, p. 146-176, LNCS 5153, 2008.
• Publisher: Springer Verlag

Other information

• Original language: English
• Type of outcome: Chapter(s) of a specialized book
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14330/08:00024133
• Organization unit: Faculty of Informatics
• ISBN: 978-3-540-85288-9
• UT WoS: 000259297000007
• Keywords in English: Component models; modelling; verification; Component Interaction automata
• Tags: Component Interaction automata, Component models, Modelling, verification
• Tags: International impact, Reviewed

Abstract

The aim of our approach to component modelling and verification, is to create a framework for formal analysis of behavioural aspects of large scale component-based systems. For the modelling purpose, we use the Component-interaction automata language. For the verification, we employ a parallel model-checker DiVinE, which is able to handle very large, hence more realistic, models of component-based systems. In this chapter, we present the application of our approach to the modelling and verification of the common modelling example defined at the beginning of this book.

Abstract (in Czech)

Cilem našeho přístupu k modelování a verifikaci komponentových systémů, je vytvoření prostředí pro formální analýzu behaviorálních aspektů velkých komponentových systémů. Pro účely modelování využíváme Component-Interaction automaty, a pro účely verifikace používáme verifikační nástroj DiVinE. V této kapitole představujeme, jak je možné využít náš přístup k modelování a verifikaci jednotného modelovacího příkladu definovaného v úvodu této knihy.

Links

• GA201/06/1338, research and development project: Name: Automatizovaná verifikace softwaru

Investor: Czech Science Foundation, Automated software verification

• 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

• 1ET408050503, research and development project: Name: 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

• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science