finer plugin - Event-B refinement automation tool

This pages contains information about the Finer plugin which adds the refinement patterns support to the RODIN platform. Refinement patterns provide a way to mechanically obtain a refined version of a specification.  A pattern is a set of rules describing how elements of an abstract specification are transformed to produce a refined version of the specification An important property of these rules is the preservation of correctness and refinement properties. It is possible to proof for a given pattern that for any matching input specification it always produces a valid refinement. Hence, specifications constructed by refinement patterns does not need to analysed and proved as it is the case with manual refinement. Many interesting refinement transformation can be described as refinement patterns.
A refinement pattern is not attached to its context as it is the case with a specification and can be used in different developments. Also, being self-contained, a pattern can be passed from from one developer to another. Refinement patterns are convinient for documenting refinement procedures. The plugin has the ability to create a naive refinement pattern from a manual refinement. In many cases, such pattern can be used as a starting point for a real reusable pattern.
One of the most attractive features of the refinement patterns is that pattern application is almost instantaneous and requires know insights about the pattern design. Different refinement paths can be investigated without investing considerable time and modelling efforts by just selecting different patterns. This is a considerable advantage over manual refinement where a developer would be reluctant to redo modelling steps once committed to a particular solution.


Version 0.1.7
  • fixed pattern import bug
Version 0.1.5
Compiled JAR (RODIN platform version 0.7.4 or higher)
Source (Java 1.5, requires Eclipse PDE and RODIN platform source 0.7.4 or newer)

Distributed under the terms of GNU GPL. The next major release (version 0.2) will feature a user-friendly pattern editor that would the underlying XML representation.
Feedback is welcome, please write to alex at iliasov dot org.


First of all, you will need the latest version of the RODIN platform. After the platform is installed, copy the plugin JAR file into the plugins directory oinside the platform installation. The platform must be restarted to activate the plugin.


A user manual for the plugin is under development. It is expected to be released in early January of 2008.


Below are some large-scale example. For the first three patterns correctness proofs have been done.

Triple Modular Redundancy
N-version programming
Recovery Block
B2Latex pretty-printer. This pattern produces an exact copy of its input, so it is completely useless as a refinement pattern but as a side effect it writes a formatted latex output of an input specification. The pattern requires this latex definitions file and also the bsymb.sty which is available from the RODIN platform web page.