Č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.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Macao
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/06:00015414
Organization unit Faculty of Informatics
ISSN 1571-0661
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
Changed by Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 31/3/2010 15:38.
Abstract
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.
Abstract (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 projectName: Automatizovaná verifikace softwaru
Investor: Czech Science Foundation, Automated software verification
1ET400300504, research and development projectName: 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 projectName: 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
PrintDisplayed: 27/9/2023 18:11