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. s. 146-176. LNCS 5153. ISBN 978-3-540-85288-9. 2008.

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

• Originální 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í
• WWW: 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

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.

Anotace č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