A 2008

Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction

ZIMMEROVÁ, Barbora

Basic information

Original name

Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction

Name in Czech

Modelování a formální analýza komponentových systémů z pohledu interakce mezi komponentami

Authors

ZIMMEROVÁ, Barbora

Edition

Czech Republic, PhD thesis, 2008

Publisher

Masaryk University, Faculty of Informatics

Other information

Language

English

Type of outcome

Audiovisual works

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

is not subject to a state or trade secret

Organization unit

Faculty of Informatics

Keywords in English

Component-based systems; component interaction; automata-based modelling; formal analysis; component equivalence; substitutability

Tags

International impact
Changed: 4/11/2012 15:32, doc. Ing. RNDr. Barbora Bühnová, Ph.D.

Abstract

V originále

Construction of flawless component-based systems is in principle a non-trivial task, due to a high possibility of discrepancies in interaction of components, caused by missing information about their deployment context at design time. At the same time, growing computational capacity of today's computers creates scope for automated formal analysis of large-scale systems, which could help to support the mentioned task. However, before formal methods can be applied, the systems under consideration need to be represented in a mathematical notation that is understood by formal tools. The representation should be sufficiently precise to include necessary information for formal analysis. But on the other hand, it needs to abstract from the aspects of the system that are not crucial for the analysis, and could increase the size of created model over the level that can be technically handled. This thesis aims to contribute to the current state of the art in formal analysis of component-based systems in two ways. First, it proposes a formal approach to modelling component-based systems in view of interaction among components, which is, in our opinion, one of the essential aspects of component-based systems that call for formal analysis. The task is supported by a new formal automata-based language for component-interaction modelling, named Component-Interaction automata. Besides the definition of the language including discussion of various types of composition that it implements, a significant part of the thesis is dedicated to the application of the language to component interaction modelling. It first studies modelling guidelines underlying the modelling process, and then examines applicability of the language to a number of interesting modelling issue, like modelling of internal state of a component, delegation of events via exception handling, asynchronous communication schemes, or construction and destruction of component instances. The second contribution of the thesis is oriented to the formal analysis of component-based systems. Based on the Component-Interaction Automata formalism, and the notion of equivalence between them, the thesis employs the component equivalence to build a theory of correctness by construction for component-based systems. In this aim, it concentrates on the elaboration of the design situations, where evaluation of a predefined kind of relationship between components can prevent future flaws in the system, such as integration of independently developed components or substitution of existing components with new ones.

In Czech

Vývoj bezchybných komponentových systémů je velice obtížný úkol z důvodu vysoké pravděpodobnosti konfliktů ve vzájemné interakci komponent, které jsou z principu komponentového vývoje vytvořeny nezávisle na sobě. Vzhledem k rostoucím možnostem výpočetní techniky se pro řešení tohoto úkolu nabízí využití automatizovaných formálních metod. Před samotnou aplikací formálních metod je však třeba vytvořit model studovaného systému, pro který je třeba nalézt vhodný modelovací formalismus. Ten by měl být dostatečně přesný, aby zachytil všechny podstatné informace pro formální analýzu. Na druhou stranu ale musí abstrahovat od těch aspektů, které nejsou pro analýzu nezbytné a mohly by vést k nepřiměřenému nárůstu velikosti modelu. Cílem této práce je přispět k vývoji v oblasti formální analýzy komponentových systémů ve dvou směrech. Prvním je navržení formálního přístupu k modelování interakcí mezi komponentami. Pro tyto účely navrhujeme nový modelovací jazyk, nazvaný Component-Interaction automaty. Kromě definice jazyka a diskuze jeho možných kompozičních operátorů, je velká část práce věnována jeho aplikaci na modelování interakcí mezi komponentami. Práce provádí celým modelovacím procesem a poté se věnuje zachycení nejrůznějších aspektů reálných systémů, jakými jsou interní stavy komponent, práce s výjimkami, modelování asynchronní komunikace, nebo konstrukce a destrukce instancí komponent. Druhým směrem studovaným v této práci je formální analýza vytvořených modelů. Na základě formalismu Component-Interaction automatů a definované ekvivalenci mezi jednotlivými modely, práce navrhuje přístup k vývoji komponentových systémů garantující správnost z podstaty použitých kroků vývoje. Konkrétně studujeme takové situace v procesu vývoje, kdy může ověření vzájemného vztahu artefaktů na různých úrovních předejít vzniku chyb v systému. Takovými situacemi jsou například integrace nezávisle vytvořených komponent, nebo výměna existujících komponent za nové.

Links

GD102/05/H050, research and development project
Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
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