From graphical design in STATEMATE to formal specification in Event B

In this paper, we present a specification technique borrowing features from two classes of specification methods, formal and semi-formal ones. The proposed technique uses STATEMATE as semi formal method and the Event B as formal one. The design is initially expressed graphically with STATEMATE, then translated to Event B and verified using powerful support tools of the B method. This paper presents a scheme for the translation of statecharts and communication between activity-charts to Event B method. We propose a solution to specify time in the event based B method and a derivation of temporal expressions (timeout in statecharts) to Event B. By an example of a real time system, we illustrate our technique