The model is the basic element of Event B method. The variables of Event B represent the state and the events represent the transitions of a system. Event B can decompose a model into another transition system from an abstract level to a less abstract one by its refinement capability. Refinement preserves the proved properties of transition system. The structure of an Event B model is given by the following elements.

MODEL nameM
REFINES nameR
. . .
VARIABLES . . .
INVARIANT . . .
ASSERTIONS . . .
INITIALISATION . . .
EVENTS . . .
END

The VARIABLES clause defines a set of variables. The EVENTS clause defines events. The INVARIANT clause describes the properties of the attributes defined in the clause VARIABLES. Typing information and safety properties are described in this clause. TheASSERTIONS are logical expressions that can be proved from the invariants. The INITIALISATION clause presents initial values to the variables of the corresponding clause. The EVENTSclause defines all the events that may occur in a given model.