B Training

Objectives

• Learn to prove a B model with a B Workshop.

Who should participate

• Any person who wishes toverify a B project.

Duration

• 3 Days

Organization

• 9 persons at most per session
• The training takes place in the ClearSy offices in Aix or Paris (except in exceptional circumstances).
• Contact ClearSy for future training dates.

Prices

• € 1,780 (excl. tax) per person.
• A rebate of 15% is granted for a group of at least 3 people from the same organization.

Program

Principles of the verification activity

• The verification ("proof") activity with the B Workshop is divided into various phases: the use of an automatic prover to demonstrate most of the obligations of correct proof, an examination of remaining proof obligations to detect errors and the finalization of proof with an interactive prover.

Automatic prover principles

• Description of the strategies and mechanisms of Worship B's automatic prover.

Using the automatic prover

• Description of the principles for using the interactive prover, description of the controls of interactive proof, methodological recommendations for a proper interactive demonstration.

Practical Organization

• Presentation of event-driven B principles. An entire Practical Task session will study its practical application while examining the significance of sophistication proof in this type of modeling. Benchmarks for the appropriate choosing of abstract variables and events will be studied to define in depth their real interpretation.

Practical Organization

• The greater part of the training takes the form of Tutorials and Practical Tasks in order to acquire real practice with Workshop B proof tools. Participants will demonstrate entire projects with Workshop B. The maintenance/back-up aspects of proof are studied.