MADE IN FRANCE

B Method Training
– Level 2: Practice B

PRACTICE B

OBJECTIVES :

  • Understand the principles of developing a B project.
  • Practice building “good” B models.
  • Understand advanced Language B concepts.

AUDIENCE :

  • Any person who wishes to acquire further knowledge on B Method.
  • Any person who must participate in a B project by writing models.

PREREQUISITES :

  • Level 1 B Training, or knowledge of B Method principles.
  • Basic IT knowledge.
  • Mathematical knowledge of a scientific secondary education level.

PROGRAM

1 – DEVELOPMENT OF A B PROJECT

  • Description of the path leading from informal specifications to formal specifications.
  • A review of the modular construction of a B project and a description of the various types of links between B modules, as well as the rules governing these links.
  • A first methodological base on which to build a B project as an assembly of modules.

2 – B MODEL BUILDING PRACTICE

Through exercises, the formal significance of “complying with specifications” is explained, as well as the manner in which it translates into the duty to provide proof with Atelier B.

Then, the participant creates formal specifications in practical sessions on complete examples based on informal requirements, and designs and analyzes how proof makes any non-compliance impossible. The principles for drafting models facilitating proof are studied.

3 – ADVANCED CONCEPTS IN B

Description of all of the advanced principles of B Language that have not been presented or detailed in the Level 1 training. This involves challenges relating to link invariants, homonymy of data and the building of loops.