Potiyenko S. Algebraic methods for verification of asynchronous parallel systems

New methods of static analysis are developed for the systems represented in a form of basic protocols. Algorithms of checking properties of the system are built for consistency and completeness, satisfiability of safety conditions. Approaches to reachability problem solution are suggested using as static analysis as model checking methods using abstractions. New algorithms of forward and backward predicate transformers have been built as functions which derive from given formula a new one that defines state class of the system. Algorithms for decomposition of subsets of languages MSC, SDL and UML into basic protocols are developed for using created formal methods for verification of industrial projects.