Component Substitutability via Equivalencies of Component-Interaction Automata

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F07%3A00019439" target="_blank" >RIV/00216224:14330/07:00019439 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Component Substitutability via Equivalencies of Component-Interaction Automata

Original language description

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 comparebehaviours 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 s

Czech name

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

Czech description

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

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

IN - Informatics

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2007

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Electronic Notes in Theoretical Computer Science

ISSN

1571-0661

e-ISSN

—

Volume of the periodical

182

Issue of the periodical within the volume

1

Country of publishing house

MO - MACAU

Number of pages

17

Pages from-to

39

UT code for WoS article

—

EID of the result in the Scopus database

—