CoIn Tool Set

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

Basic information

• Original name: CoIn Tool Set
• Name in Czech: Sada nástrojů CoIn
• Authors: BENEŠ, Nikola (203 Czech Republic, guarantor, belonging to the institution), Barbora BÜHNOVÁ (203 Czech Republic, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, belonging to the institution) and Milan KŘIVÁNEK (203 Czech Republic, belonging to the institution).
• Edition: 2009.

Other information

• Original language: English
• Type of outcome: Software
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Czech Republic
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14330/09:00028846
• Organization unit: Faculty of Informatics
• Keywords (in Czech): formální verifikace; ověřování modelu; komponentově-interakční automaty; state/event LTL
• Keywords in English: formal verification; model checking; component-interaction automata; state/event LTL
• Technical parameters: Nástroj pro ověřování vlastností komponentově interakčních automatů
• Tags: Component-Interaction automata, formal verification, Model checking, state/event LTL
• Tags: International impact

Abstract

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.

Abstract (in Czech)

Úč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ě.

Links

• GA201/09/1389, research and development project: Name: Verifikace a analýza velmi velkých počítačových systémů

Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET400300504, research and development project: Name: Realistická aplikace formálních metod v komponentových systémech

Investor: Academy of Sciences of the Czech Republic, Realistic application of formal methods in component systems