In the paper one of approaches to modelling, specification and verification of automaton programs are considered. The automata programming technology is effective enough in design and verification (the analysis of correctness) software for reactive and controlling systems. This technology, besides other methods of software construction “without errors”, is much more constructive, as it allows to begin “struggling against errors” at the algorithmization stage. However, in spite of the fact that the idea of automata programming is directed on the construction of reliable programs, the problem of the program correctness analysis still remains actual. From the point of view of modelling and analysing program systems the automata approach to programming has a number of advantages in comparison with the traditional approach. When constructing a model for a program written in the traditional style, there is a serious problem of the adequacy of this program model to the initial program. The model can be unable to take into account a number of program properties or can generate nonexisting properties. Under the automata programming such a problem is excluded, as a collection of communicating automata, describing the logic of the program, is already an adequate program model. This fact is an indisputable advantage of the automata technology. Moreover, the model has a finite set of states, that is, in practice, a necessary condition for successful automatic verification by the model checking method. Besides, properties of automata programs are naturally and clearly formulated and specified. These properties obviously correspond with communicating automata representing the logic of an automata program. The practical result of the work is an application of the tool SPIN and the temporal logic LTL for specification and verification of hierarchical automaton programs.