D 2005

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

BRIM, Luboš, Ivana ČERNÁ, Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ

Základní údaje

Originální název

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

Název česky

Component-Interaction automaty pro verifikačně orientovanou specifikaci komponentových systémů

Autoři

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

Vydání

Ames, USA, Proceedings of SAVCBS 2005, s. 31-38, 2005

Nakladatel

Department of Computer Science, Iowa State University

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

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

Odkazy

Kód RIV

RIV/00216224:14330/05:00012815

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

ADLs; Component-Interaction automata; component interaction; verification

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 29. 11. 2006 14:53, doc. Ing. RNDr. Barbora Bühnová, Ph.D.

Anotace

ORIG CZ

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

Česky

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

Návaznosti

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