The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems

BENEŠ, Nikola, Luboš BRIM, Ivana ČERNÁ, Jiří SOCHOR, Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ. The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems. In Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08). Málaga, Spain: Department of Computer Science, University of Málaga, 2008, s. 221-225. ISSN 1571-0661.

Základní údaje

Originální název

The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems

Název česky

CoIn Tool: Modelování a verifikace interakcí v komponentových systémech

Autoři

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

Vydání

Málaga, Spain, Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08), s. 221-225, 2008

Nakladatel

Department of Computer Science, University of Málaga

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Španělsko

Utajení

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

Kód RIV

RIV/00216224:14330/08:00024294

Organizační jednotka

Fakulta informatiky

ISSN

Klíčová slova anglicky

component-based systems; Component-Interaction automata; formal verification; LTL; model checking

Štítky

Component-based systems, Component-Interaction automata, formal verification, LTL, Model checking

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

The paper presents a modelling and model-checking tool designed for formal verification of interactions among components in hierarchical component-based systems. As distinct from existing verification frameworks, the presented CoIn Tool is able to analyse complex hierarchical models on the fly, and to verify linear temporal properties involving both state and action propositions.

Česky

Článek prezentuje modelovací a verifikační nástroj navržený pro formální ověřování správnosti interakcí mezi komponentami v hierarchických komponentových systémech. Na rozdíl od existujících verifikačních nástrojů je prezentovaný CoIn Tool schopný analyzovat složité hierarchické modely on-the-fly a verifikovat lineární temporální vlastnosti vyjadřující se jak o stavech tak i akcích studovaných modelů.

---

Návaznosti

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ů