Automata-Based Software Engineering with Event-B.

A new automata-based programming language built by extending the Event-B specification language is proposed. When developing models in Event-B, it becomes possible to use automata-based methods in addition to the popular refinement method. The automata-based software engineering based on Event-B is demonstrated by the example of traffic control on a 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 nontrivial bugs in our solution. [ABSTRACT FROM AUTHOR]