Component Substitutability via Equivalencies of Component-Interaction Automata

ČERNÁ, Ivana, Pavlína VAŘEKOVÁ and Barbora ZIMMEROVÁ. Component Substitutability via Equivalencies of Component-Interaction Automata. In Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'06). Macao: UNU-IIST, 2006, p. 115-130. ISSN 1571-0661.

Basic information

Original name

Component Substitutability via Equivalencies of Component-Interaction Automata

Name in Czech

Vyměnitelnost komponent na základě ekvivalencí Component-interaction automatů

Authors

ČERNÁ, Ivana (203 Czech Republic, guarantor), Pavlína VAŘEKOVÁ (203 Czech Republic) and Barbora ZIMMEROVÁ (203 Czech Republic)

Edition

Macao, Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'06), p. 115-130, 2006

Publisher

UNU-IIST

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Macao

Confidentiality degree

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

RIV identification code

RIV/00216224:14330/06:00015414

Organization unit

Faculty of Informatics

ISSN

Keywords in English

component-based systems; reconfiguration correctness; component substitutability; independent implementability

Tags

component substitutability, Component-based systems, independent implementability, reconfiguration correctness

Tags

International impact, Reviewed

---

Abstract

V originále

We provide a new look at formal aspects of component substitutability (replacement of a component with a new one) and independent implementability (reuse of a component in any system where its implementation satisfies the specification given by the environment), in view of an underlying formalism called Component-interaction automata. Our aim is to offer a formal characterization of preconditions that lead to reconfiguration correctness (proper component substitution and safe independent implementation). Such preconditions then guarantee that the updated system remains equivalent to the former one and hence there is no need to verify it again. The contribution of the paper is twofold. First, we formally define three relations that allows us to compare behaviours of two components with respect to reconfiguration correctness. Namely, the equivalence relation, specification--implementation relation, and substitutability relation. Second, we formally characterize the problem of component substitutability for both equivalent and non-equivalent components, and the problem of independent implementability. The characterizations are captured in several propositions which are proved in the text.

In Czech

Článek nabízí nový pohled na formální aspekty vyměnitelnosti dvou komponent a nezávislé implementace komponenty (umožnuje použití komponenty v jakémkoli systému kde implementace komponenty vyhovuje specifikaci stanovené prostředím), s využitím formalismu zvaného Component-interaction automaty. Cílem práce je poskytnout formální charakterizaci podmínek, které vedou k rekonfigurační korektnosti (správná substituce komponent a bezpečná nezávislá implementace). Tyto podmínky posléze zaručují, že nový systém (po výměně komponenty) zůstane ekvivalentní původnímu, a tedy není nutné ho opakovaně verifikovat.

---

Links

GA201/06/1338, research and development project	Name: Automatizovaná verifikace softwaru Investor: Czech Science Foundation, Automated software verification
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