MADE IN FRANCE

Teaching B

The B formal method is taught in many institutions and universities, on all continents, for:

  • Software development (B language)
  • System modeling (Event-B language)

The teaching is based on the Atelier B “community version” which is fully functional and fully usable for modeling, proof and C code generation. Formal B models can be animated and verified (model-checking) with the ProB tool.

A MOOC dedicated to the B method is available to all. It contains 20 videos for a duration of 6h50, covering the basics of the method, from modeling to project management. The site hosts the models used for the videos as well as the proof files. The MOOC was realized in collaboration with the Instituto Metropole Digital / UFRN (Natal, Brazil).

Furthermore, the University of Düsseldorf hosts a repository of B formal models () from a wide variety of industrial and academic modelers, which can be used for training and self-improvement.

Finally, the CLEARSY Safety Platform can be programmed with the B language for the realization of critical applications. Among the two configurations of the safety platform (for education / for industry), the “for education” version is available as :

The software simulator is available free of charge and without restrictions. It was demonstrated during a tutorial at the ABZ 2021 conference (see video).

The added value of the CLEARSY Safety Platform is that students can “bring things to life” (see modeling variables change on the simulator or LEDs flash on the board). Hands-on courses and sessions have been given around the world for the past four years and this has been well received by:

  • theoretical profiles who can connect their abstract models to the physical world
  • by the embedded systems / IoT profiles who can discover formal modeling and verification.

These cards are already used for master / master 2 courses in France, Germany, Italy, Canada and Brazil.