Patterns for Refinement Automation - Formal Methods for Components and Objects - page 85

Fig. 3. The Event-B refinement patterns tool architecture
relies on two major RODIN Platform components: the Platform database, which stores
models, proof obligations and proofs constituting a development; and the prover which
is a collection of automated theorem provers supplemented by the interactive prover.
The overall tool architecture is presented in Figure 3. The core of the tool is the pat-
tern instantiation engine . The engine uses an input model, imported from the Platform
database, and a pattern, from the pattern library, to produce a model refinement. The
engine implements only the core pattern language: the sequential and parallel compo-
sition, and forall construct. The method-specific model transformations (in this case,
Event-B model transformations) are imported from the model transformation library .
The process of a pattern instantiation is controlled by the pattern instantiation wiz-
ard . The wizard is an interactive tool which inputs pattern configuration from a user. It
validates user input and provides hints on selecting configuration values. Pattern con-
figuration is constructed in a succession of steps: the values entered at a previous step
influence the restrictions imposed on the values of a current step configuration.
The result of a successful pattern instantiation is a new model and, possibly, a set of
instantiation proof obligations - additional conditions that must be verified every time
when a pattern is applied. The output model is added to a current development as a
refinement of the input model and is saved in the Platform database. The instantiation
proof obligations are saved in an Event B context file. The RODIN platform builder
automatically validates and passes them to the Platform prover.
The tool is equipped with a pattern editor . The current version (0.1.7)[13] uses the
XML notation and an XML editor to construct patterns. The next release is expected to
employ a more user-friendly visual editor. The available refinement patterns are stored
in the local pattern library . Patterns in the library are organised in a catalogue tree,
according to the categories stated in pattern specifications. A user can browse through
the library catalogue using a graphical dialogue. This dialogue is used to select a pattern
for instantiation or editing.