Component Substitutability via Equivalencies of Component-Interaction Automata

ČERNÁ, Ivana; Pavlína VAŘEKOVÁ a 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, s. 115-130. ISSN 1571-0661.

Základní údaje

Originální název

Component Substitutability via Equivalencies of Component-Interaction Automata

Název česky

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

Autoři

ČERNÁ, Ivana ORCID; Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ

Vydání

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

Nakladatel

UNU-IIST

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Macao

Utajení

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

Kód RIV

RIV/00216224:14330/06:00015414

Organizační jednotka

Fakulta informatiky

ISSN

Klíčová slova anglicky

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

Štítky

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

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

Česky

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

---

Návaznosti

GA201/06/1338, projekt VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
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
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů