Modelling and implementation of automata-based hierarchical discrete-event controllers using the B-method

This work uses the formal method B for the implementation of hierarchical control structures for a class of discrete-event systems modelled by Finite State Machines. Given the architecture, their constitutive controllers and communication channels together with their functional specifications, a formal translation is established from the automata-based controllers into abstract machines and relates them with the structuring features of B. Therefore, the implementation can be proved to be correct with respect to the functional specification. The work is illustrated with an example.