BART Tool Training


BART Training Specifics


OBJECTIVES :

Learn to refine a B model automatically with Bart.

TARGET PUBLIC :

Anyone who wants to efficiently produce software using the B Method.

PREREQUISITES :

> Level 2 B Training
(Having completed Level 3 is a plus).

ORGANIZATION :

> 10 persons maximum per training session
> The training takes place in CLEARSY’s offices in Aix or Paris (Except exceptional circumstances).
> Contact CLEARSY for upcoming training session dates.

LENGTH :

3 days.

PRICES :

A 15% discount is granted for a group of at least three people from the same organization.

PROGRAM


1 – REVIEW OF REFINEMENT PRINCIPLES

> Description of the principles of the refinement of an abstract model into a concrete model:
– data refinement,
– substitution refinement.
> Why and how is the automation of these principles possible?

2 – BART TOOLS PRINCIPLES

> How to refine an abstract model: What are the prerequisites for automatic refinement ? How are refinement rules written:
– Refinement rules for variables,
– Refinement rules for operations.
> Presentation of pitfalls to be avoid when refining. How to obtain effective models while limiting the proof effort?

3 – USE OF THE GRAPHIC INTERFACE

> Description of the interface and practice examples.

4 – PRACTICAL STRUCTURES

> More than two thirds of the training is conducted in the form of practice assignments.