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).
Lenght	3 days
Organization	10 persons maximum per training session The training takes places in ClearSy’s premises in Aix or Paris (except in exceptional circumstances). Contact ClearSy for upcoming training session dates.
Prices	€1,780, excluding tax, per person. A 15% discount is granted for a group of at least three people from the same organization.
Program	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 automatization of these principles possible? 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? Use of the Graphic Interface Description of the interface and practice examples Practical Structure More than two thirds of the training is conducted in the form of practice assignments.