Automatic refinement

PRESENTATION

Refinement is at the heart of the B method. It allows to consider first only the abstraction of a software before taking into account the design and implementation details. The automation of refinement allows to speed up the development of a software by entrusting to a tool the mechanical transformation of a complete abstract model into an implementable model.

Such a tool, called an automatic refiner, transforms a machine into a set of machines, refinements and implementations using a set of transformation rules called refinement rules.

The process of automatic refinement then breaks down into a large number of small transformations (which lead to simpler proof obligations).

Historically, the first automatic refiner for B was developed by Matra Transport and used many times to develop security software for example:

• For the subways in Caracas and New York (Carnarsie Line),
• The automatic shuttle at Charles de Gaulle airport.
• Another automatic refiner, BART (B Automatic Refiner Tool), was developed during the ANR Rimel project and then integrated into Atelier B.

The refinement process is interactive: The tool applies the refinement rules recursively and stops when no rule is available to refine a variable or substitution. The tool user must then add a refinement rule to the rule base, either by creating one from scratch or by adapting an existing rule. This process repeats until the target machine is fully refined. Neither the tool nor the refinement rules need to be validated: the generated models must be proven afterwards – if they are wrong, the proof cannot be successful.

 

IMPROVEMENTS

The automatic refinement process can induce conflicts when refining variables that may need to be both abstracted and implemented. The algorithms of the automatic refinement engine do not efficiently handle such situations and the conflict situations have to be resolved by the user, by modifying/adding ad-hoc refinement rules. The automation of the conflict resolution procedures was the subject of an internship.