Chebotarev A. Provably-correct development of algorithms of reactive systems operation

The object is the provably-correct design of reactive algorithms at the initial stage of their development; the aim is to ensure the error-free design of industrial reactive algorithms; the methods are mathematical logic and automata theory; the novelty consists in the original theory and methodology of provably-correct design of reactive algorithms; the main results include the two-level system of specification languages, the methods of checking specifications for consistency, solving the problem of ensuring correct join operation of the system under design and its environment, a number of new methods for synthesis of automaton from its logical specification; the field of implementations is the development of control systems for safety-critical objects.