Perepelytsya I. Models and methods for static analysis of asynchronous information processing systems

This thesis is devoted to problems of mathematical modelling software systems. An architectural approach based on asynchronous transfer of control between components of the system is considered in this work. It is a promising approach today. It ensures system adaptability which is important for large systems that have a great time of existence. So developers should realise mechanisms to ensure their re-engineering. In the thesis a general model of components for asynchronous system was built. It was transformed by series of equivalent transformations to the algebraic structures known as pre-automaton. The expressive ability of pre-automatic models is better than expressive ability automata models. In particular, the pre-automatic model has ability to model such kind of system behaviour as live-lock. In the thesis a criterion of existence for live-lock was obtained. Due to the fact that pre-machines is closely related to the directed graph, which arcs are labelled by prefix codes, the concept of a region was generalised. An interval was defined as a maximal region. This allows to introduce the concept of a derivative graph similar to a derivative graph for a control flow graph flow and to build derivatives series for pre-machines. This series identifies the hierarchical structure which inherent to the corresponding pre-automata. The theoretical results allowed to construct the set of computational methods for static analysis of pre-machine and to develop the complex of utilities, which realize these methods.