> Learn to prove a B model with a B Workshop.
WHO SHOULD PARTICIPATE :
> Any person who wishes to verify a B project.
> 9 persons at most per session
> The training takes CLEARSY offices in Aix or Paris (Except in excpetional circumstances).
> Contact CLEARSY for future training dates.
> A rebate of 15% is granted for a group of at least 3 people from the same organization.
1 – 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.
2 – AUTOMATIC PROVER PRINCIPLES
> Description of the strategies and mechanisms of Worship B’s automatic prover.
3 – 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
4 – 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. 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.