| Description |
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.
|
