Graphical design of reactive systems

Reactive systems can be designed graphically using Statecharts. This paper presents a scheme for the translation of Statecharts into the Abstract Machine Notation (AMN) of the B method. By an example of a conveyor system, we illustrate how the design can be initially expressed graphically with Statecharts, then translated to AMN and analysed in AMN, and then further refined to executable code.