From ClearSy Tools

Contents 1 Introduction 2 Gallery 3 Tutorial & examples 4 Reference manuals 5 Wiki manuals 6 Sourceforge site

Introduction

The BART (B Automatic Refinement Tool) project aims at developing an automatic refinement tool for B machines.

This tool allows for a B0 implementation for a machine or a sufficiently detailed B refinement to be automatically generated.

BART operates on the basis of refinement rules. Additional refinement rules may be added in order to allow for the customization of the refinement of some components.

The BART automatic refinement tool has been developed in the context of the RIMEL project and is integrated into Atelier B 4.0. It comes along with an interactive refinement graphical interface and a sample refinement rule database containing 228 rules.

Gallery

refinement rules database

operation refinement

conflicts while refining

Tutorial & examples

Under construction

Reference manuals

• Bart Specification 1.1 (pdf - French)
• Bart User Manual (alpha version) 29.04.2009 (pdf - English)

Wiki manuals

• BART specification 1.1 (Wiki format - english)

Sourceforge site

BART is now open-source (GPL v3.0) and is hosted on sourceforge.