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

Installation

Documentation

• Examples for Parity and Hamming Refinement Patterns
• Screenshots showing the plugin within the platform.
• A walk-through guide with screenshots.
• Small example for the N-version programming and Recovery Block patterns
  
• Refinement Patterns (slides from EFTS'2008)
  
• A. Iliasov. Refinement patterns for rapid development of dependable systems. Proc. Engineering Fault Tolerant Systems Workshop (at ESEC/FSE, Croatia), ACM Digital Library. (September 4, 2007)

Examples