B Method Training - Level 2 : Practice B


TRAINING / LEVEL 2 : PRACTICE B


OBJECTIVES :

> Understand the principles of developing a B project.
> Practice building “good” B models.
> Understand advanced Language B concepts.
> Discover event-driven B.

WHO SHOULD PARTICIPATE :

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

PREREQUISITES:

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

ORGANIZATION :

> 9 persons at most per formation
> The training takes place in the CLEARSY offices in Aix or Paris (Except in exceptional circumstances).
> Contact CLEARSY for future training dates.

DURATION :

4 days

PRICES:

A rebate of 15% is granted for a group of at least 3 people from the same organization.

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 Workshop B. Then, the participant creates formal specifications in practical sessions on complete examples based on informal prerequisites, and designs and analyzes how proof renders 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 Language B 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.

4 – INTRODUCTION TO EVENT-DRIVEN B

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.

5 – PRACTICAL ORGANIZATION

More than half of the training is in the form of Tutorials and Practical Tasks in order to better become familiar with the modular building of a B project and advanced notions of Language B. To this end, the Practical Task session on the modeling and design of a control system for traffic lights at an intersection will take up the greatest portion of the Practical Tasks. It is followed by a Tutorial and Practical Task session on event-driven B.

pictos-6

> DOWNLOAD PROGRAM :
B TRAINING – LEVEL 2