The B-Method: from specification to code

This course introduces the B-method: the basic concepts ranging from the most basic structures like the B machine to proofs using the Atelier-B interactive prover. After the course, students will be able to develop software from specification to source code using the B formal development approach.


The B Method - Marketing Video

This video explains why you should follow the MOOC on B and what its expected benefits on your career are.

0 de 02min

Level: Basic

Video duration: 02:55

Lecture 01: Course Introduction

This video presents the structure of the course, provides an overview of the different kinds of formal methods and specification styles, and tells us some myths on formal methods.

0 de 08min

Level: Basic

Video duration: 08:43

Lecture 02: Overview of the B method

This video briefly introduces the tool Atelier-B, the B and Event-B languages, and some industrial references. The main concepts of B are exposed.

0 de 15min

Level: Basic

Video duration: 15:03

Lecture 03: The concepts of B

This video presents the founding notions of B: projects, libraries, modules, components, abstract machine, refinement, implementation, and proof.

0 de 09min

Level: Basic

Video duration: 09:29

Lecture 04: Introduction to Abstract Machines

This video introduces the notion of abstract machines, based on an example that is verified, animated and for which C source code is generated.

0 de 16min

Level: Basic

Video duration: 16:31

Lecture 05: Machine Consistency

This video presents the concept of machine consistency and the details behind this concept including its formal definition.

0 de 22min

Level: Basic

Video duration: 22:10

Lecture 06: Sets and Constants

This video explains how we can define and use sets and constants in abstract machines.

0 de 26min

Level: Basic

Video duration: 26:44

Lecture 07: Relations

This video introduces the use of mathematical relations in abstract machines to store information.

0 de 23min

Level: Basic

Video duration: 23:28

Lecture 08: Functions and Sequences

This video presents the mathematical definitions of functions and sequences, as well as their properties, operations and usage to store information.

0 de 32min

Level: Basic

Video duration: 32:31

Lecture 09: Arrays

This video presents the mathematical definition of arrays and its use to describe the components behaviour.

0 de 19min

Level: Basic

Video duration: 19:30

Lecture 10: Non-determinism

This lecture presents how the B method provides support for non-determinism.

0 de 26min

Level: Basic

Video duration: 26:35

Lecture 11: Data Refinement - Part I

This lecture presents the main concepts of data refinement, that is, how to transform data from an abstract mathematical representation into a more concrete data structure.

0 de 21min

Level: Basic

Video duration: 21:57

Lecture 12: Data Refinement - Part II

Data Refinement - Part II.

0 de 32min

Level: Basic

Video duration: 32:06

Lecture 13: Refinement of Non-determinism

In this lecture, we present how the refinement process allows the resolution of non-deterministic constructs.

0 de 43min

Level: Basic

Video duration: 43:07

Lecture 14: Implementation

This lecture presents a special sort of refinement component that constitutes the final refinement: IMPLEMENTATION.

0 de 26min

Level: Basic

Video duration: 26:43

Lecture 15: Loops

This video presents how the B-Method provides support to loops, an essential programming construct.

0 de 31min

Level: Basic

Video duration: 31:42

Lecture 16: Structuring

This video details the different ways of structuring a B project in order to lower the complexity of the modelling and to ease the proof.

0 de 07min

Level: Basic

Video duration: 07:35

Lecture 17: Code Generation

This video show how a B model is transformed into C code and which constraints have to be met to be successful.

0 de 12min

Level: Basic

Video duration: 12:22

Lecture 18: Introduction to Proofs

The video explains what proving a software against its specification means, what automatic proof is, and introduces interactive proof and the notion of proof tree.

0 de 13min

Level: Basic

Video duration: 13:28

Lecture 19: Proofs

This video explains how to improve automatic proof performances and provides some hints about the relation between modelling and ease to prove.

0 de 09min

Level: Basic

Video duration: 09:49

Lecture 20: Managing Projects

This video describes the B development cycle, provides metrics and explains how to reduce the complexity and to simplify the organisation of a project.

0 de 07min

Level: Basic

Video duration: 07:55


Supplementary material

Click HERE to access the Atelier B CLEARSY Youtube Channel.

Click HERE to access a GitHub containing the models, proof files and generated code used in the videos.


If you want to contribute with further material, please contact us.


Tools


Lecturers

Marcel Oliveira
Thierry Lecomte

Staff

Danise Suzy da Silva Oliveira Head of SPM
Bárbara Cecília de Macedo Freitas Designer
Edinara Medeiros de Araújo Designer
José Antônio Bezerra Júnior Designer
Laura Caroline Dias Fernandes Designer
Fabylane Nívea dos Santos Bezerra de Carvalho Video Producer
Heloisa Madalena Oliani Caravina Video Producer
Lívia de Souza Motta Video Producer
Victor Hugo Roque Video Producer
Rodrigo Reinaldo Ferreira Web Developer
Tadeus Lima de Araújo Web Developer
Willyelns Germano Xavier Web Developer

References

The B-Method: an Introduction

Steve Schneider

Macmillan Education UK, 19 de out de 2001 - 384 pages

reference-book Click on image for more information.
reference-book Click on image for more information.

B Language Reference Manual

Version 1.8.10

Document created by ClearSy