- Learn to prove a B model with Atelier B.
WHO SHOULD PARTICIPATE :
- Any person who wishes to verify a B project.
- 10 persons at most per session.
- The training takes CLEARSY offices in Aix or Paris (Except in exceptional circumstances).
- Contact CLEARSY for future training dates.
- A discount is applied to holders of a AtelierB maintenance contract.
1 – PRINCIPLES OF THE VERIFICATION ACTIVITY
The verification (“proof”) activity with Atelier B 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 Atelier B 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
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 Atelier B proof tools. Participants will demonstrate entire projects with Atelier B. The maintenance/back-up aspects of proof are studied.