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

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

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.

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