The language and methods of automata-based software engineering integrated with object-oriented and predicate software engineering methods are developed. A program is constructed as a finite state automation presented in the form of control state hypergraph. Automata-based methods are illustrated on the programs of alarm clock modeling and ATM adaptation layer (type 2) protocol.