| 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
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.
|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
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
|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.