Other formats:
BibTeX
LaTeX
RIS
@misc{789513,
author = {Zimmerová, Barbora},
address = {Czech Republic},
keywords = {Component-based systems; component interaction; automata-based modelling; formal analysis; component equivalence; substitutability},
language = {eng},
location = {Czech Republic},
publisher = {Masaryk University, Faculty of Informatics},
title = {Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction},
year = {2008}
}
TY - GEN
ID - 789513
AU - Zimmerová, Barbora
PY - 2008
TI - Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction
VL - PhD thesis
PB - Masaryk University, Faculty of Informatics
CY - Czech Republic
KW - Component-based systems
KW - component interaction
KW - automata-based modelling
KW - formal analysis
KW - component equivalence
KW - substitutability
N2 - 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.
ER -
ZIMMEROVÁ, Barbora. \textit{Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction}. Czech Republic: Masaryk University, Faculty of Informatics. PhD thesis. 2008.
|
