CoIn Tool Set

BENEŠ, Nikola, Barbora BÜHNOVÁ, Ivana ČERNÁ a Milan KŘIVÁNEK. CoIn Tool Set. 2009.

Základní údaje

Originální název

CoIn Tool Set

Název česky

Sada nástrojů CoIn

Autoři

BENEŠ, Nikola (203 Česká republika, garant, domácí), Barbora BÜHNOVÁ (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, domácí) a Milan KŘIVÁNEK (203 Česká republika, domácí)

Vydání

2009

---

Další údaje

Jazyk

angličtina

Typ výsledku

Software

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Odkazy

URL

Kód RIV

RIV/00216224:14330/09:00028846

Organizační jednotka

Fakulta informatiky

Klíčová slova česky

formální verifikace; ověřování modelu; komponentově-interakční automaty; state/event LTL

Klíčová slova anglicky

formal verification; model checking; component-interaction automata; state/event LTL

Technické parametry

Nástroj pro ověřování vlastností komponentově interakčních automatů

Štítky

Component-Interaction automata, formal verification, Model checking, state/event LTL

Příznaky

Mezinárodní význam

---

Anotace

V originále

The purpose of the CoIn Tool Set is to assist developers along the modelling and verification process using component-interaction (CI) automata. The Tool Set currently consists of two parts: a graphical modelling tool, which enables the developer to create CI automata models visually using a GUI, and a verification environment for formal verification of created models with the model-checking technique. The properties to be checked are specified using temporal logic, namely a variant of State/Event LTL.

Česky

Účelem sady nástrojů CoIn je pomáhat vývojářům při modelování a verifikaci za pomoci komponentově-interakčních (CI) automatů. Sada nástrojů se v současnosti skládá ze dvou částí: modelovacího nástroje, který umožňuje vytvářet modely CI automatů pomocí grafického rozhraní, a verifikačního prostředí pro formální verifikaci vytvořených modelů pomocí techniky ověřování modelu (model checking). Ověřované vlastnosti jsou specifikovány v temporální logice State/Event LTL, resp. její variantě.

---

Návaznosti

GA201/09/1389, projekt VaV	Název: Verifikace a analýza velmi velkých počítačových systémů Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačový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