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.