B Training

Objectives

• Understand the fundamental principles of Method B.
• Discover Language B.

Who should participate

• Any person who wishes to understand the principles of Method B and discover its benefits.
• Any person who must participate in the development of a B project or who wishes to review B models.

Prerequisites

• Knowledge of general principles relating to the development cycle of a system or software (specificartion concepts).
• Basic IT knowledge.
• Mathematical knowledge of a scientific secondary education level.

Duration

• 4 Days

Organization

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

Prices

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

Program

Method B principles

• Definition of B: a formal specification and design method with proof that may reach a concrete level (C internet code, ADA).
• Advantage of formal specifications and the building of a model through the systematic description of its properties.
• Modularity and hierarchy concepts: a B model is built in a modular manner, its properties are introduced hierarchically.
• Validation through proof: proof guarantees conformity with invariant properties; it is exhaustive in ensuring that the code complies with its specifications.
• Method B benefits.
• Description of the main uses of B within industry.

Language B

• Description of elements constituting Language B: predicates, mathematical expressions (integers, Boolean, enumerations, sets, relations, functions), substitutes that form the dynamic of the modeled system.
• The three types of B components (abstract machines, sophistication and implementation).

Practical Organization

• More than half of the training involves Tutorials or Practical Tasks in order to better become familiar with specifications in B, the drafting of a design in B based on the same specifications and the proof that.
• The design complies with its specifications. The Practical Task sessions use Workshop B. One of the Practical Task sessions is an introduction to Workshop B and Method B by studying an existing project.