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.


Download

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

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.

Installation

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.

Documentation

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

Examples

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

Triple Modular Redundancy
download
N-version programming
download
Recovery Block
download
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.
download