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

BENEŠ, Nikola, Luboš BRIM, Ivana ČERNÁ, Jiří SOCHOR, Pavlína VAŘEKOVÁ and 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, p. 221-225. ISSN 1571-0661.

Basic information

Original name

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

Name in Czech

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

Authors

BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, belonging to the institution), Jiří SOCHOR (203 Czech Republic, belonging to the institution), Pavlína VAŘEKOVÁ (203 Czech Republic, belonging to the institution) and Barbora ZIMMEROVÁ (203 Czech Republic, guarantor, belonging to the institution)

Edition

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

Publisher

Department of Computer Science, University of Málaga

---

Other information

Language

English

Type of outcome

Proceedings paper

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Spain

Confidentiality degree

is not subject to a state or trade secret

RIV identification code

RIV/00216224:14330/08:00024294

Organization unit

Faculty of Informatics

ISSN

Keywords in English

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

Tags

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

Tags

International impact, Reviewed

---

Abstract

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.

In Czech

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

---

Links

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
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems