Component-Interaction Automata Approach (CoIn)

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

Základní údaje

Originální název

Component-Interaction Automata Approach (CoIn)

Název česky

Přístup využívající Component-Interaction automaty

Autoři

ZIMMEROVÁ, Barbora (203 Česká republika, garant), Pavlína VAŘEKOVÁ (203 Česká republika), Nikola BENEŠ (203 Česká republika), Ivana ČERNÁ (203 Česká republika), Luboš BRIM (203 Česká republika) a Jiří SOCHOR (203 Česká republika)

Vydání

Berlin / Heidelberg, Germany, The Common Component Modeling Example: Comparing Software Component Models, s. 146-176, LNCS 5153, 2008

Nakladatel

Springer Verlag

---

Další údaje

Jazyk

angličtina

Typ výsledku

Kapitola resp. kapitoly v odborné knize

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Odkazy

URL

Kód RIV

RIV/00216224:14330/08:00024133

Organizační jednotka

Fakulta informatiky

ISBN

978-3-540-85288-9

UT WoS

000259297000007

Klíčová slova anglicky

Component models; modelling; verification; Component Interaction automata

Štítky

Component Interaction automata, Component models, Modelling, verification

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.

Česky

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.

---

Návaznosti

GA201/06/1338, projekt VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
GD102/05/H050, projekt VaV	Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET400300504, projekt VaV	Název: Realistická aplikace formálních metod v komponentových systémech Investor: Akademie věd ČR, Realistická aplikace formálních metod v komponentových systémech
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky