ZIMMEROVÁ, Barbora. Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction. Czech Republic: Masaryk University, Faculty of Informatics, 2008. PhD thesis.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction
Název česky Modelování a formální analýza komponentových systémů z pohledu interakce mezi komponentami
Autoři ZIMMEROVÁ, Barbora.
Vydání Czech Republic, PhD thesis, 2008.
Nakladatel Masaryk University, Faculty of Informatics
Další údaje
Originální jazyk angličtina
Typ výsledku Audiovizuální tvorba
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky Component-based systems; component interaction; automata-based modelling; formal analysis; component equivalence; substitutability
Štítky automata-based modelling, component equivalence, component interaction, Component-based systems, formal analysis, substitutability
Příznaky Mezinárodní význam
Změnil Změnila: doc. Ing. RNDr. Barbora Bühnová, Ph.D., učo 39394. Změněno: 4. 11. 2012 15:32.
Anotace
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.
Anotace česky
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é.
Návaznosti
GD102/05/H050, projekt VaVNázev: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET400300504, projekt VaVNá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
VytisknoutZobrazeno: 5. 2. 2023 15:35