A new automata-based programming language has been built by extending the Event-B specification language. When developing models in Event-B, it becomes possible to use automata-based methods in addition to the popular refinement method. Automata-based software engineering, supported by deductive verification in Event-B, can be successfully used for the development of control systems in critical infrastructure with a high cost of error. A model of the Event-B specification in the automata-based programming language is constructed. The Event-B specification is a chain of machine refinements. The machine is defined by a non-deterministic composition of events. An event is the equivalent of a simple conditional statement without else branch. In automata-based software engineering, in addition to non-deterministic composition, a number of other compositions are allowed. The main one is a hypergraphic composition with respect to control states. Parallel process composition, object-oriented and aspect-oriented compositions are also possible. A process can be called from another process. It is possible to send and receive messages. There are different time actions. It is not difficult to rewrite an automata-based program into the Event-B specification. The automata-based software engineering with Event-B is demonstrated by the example of the problem of traffic control on the bridge from the Event-B system manual. A simpler solution with verification in the Rodin tool is proposed. The effectiveness of Event-B verification methods is confirmed by finding three non-trivial errors in our solution.