I confirm that I have knowledge on the Creative Commons Attribution-NonDerivative- CC BY-NC-ND license and what it stands for. I also confirm that I have read the terms in the link below and I am fully aware of these terms.
I understand that the materials supplied to me can not be altered or used for commercial purposes. Derivations can not be created and, if I share the materials listed below, I must do so under the same license and always quoting the authors. "
This video explains why you should follow the MOOC on B and what its expected benefits on your career are.
Level: Basic
Video duration: 02:55
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.
Level: Basic
Video duration: 08:43
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.
Level: Basic
Video duration: 15:03
This video presents the founding notions of B: projects, libraries, modules, components, abstract machine, refinement, implementation, and proof.
Level: Basic
Video duration: 09:29
This video introduces the notion of abstract machines, based on an example that is verified, animated and for which C source code is generated.
Level: Basic
Video duration: 16:31
This video presents the concept of machine consistency and the details behind this concept including its formal definition.
Level: Basic
Video duration: 22:10
This video explains how we can define and use sets and constants in abstract machines.
Level: Basic
Video duration: 26:44
This video introduces the use of mathematical relations in abstract machines to store information.
Level: Basic
Video duration: 23:28
This video presents the mathematical definitions of functions and sequences, as well as their properties, operations and usage to store information.
Level: Basic
Video duration: 32:31
This video presents the mathematical definition of arrays and its use to describe the components behaviour.
Level: Basic
Video duration: 19:30
This lecture presents how the B method provides support for non-determinism.
Level: Basic
Video duration: 26:35
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.
Level: Basic
Video duration: 21:57
Data Refinement - Part II.
Level: Basic
Video duration: 32:06
In this lecture, we present how the refinement process allows the resolution of non-deterministic constructs.
Level: Basic
Video duration: 43:07
This lecture presents a special sort of refinement component that constitutes the final refinement: IMPLEMENTATION.
Level: Basic
Video duration: 26:43
This video presents how the B-Method provides support to loops, an essential programming construct.
Level: Basic
Video duration: 31:42
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.
Level: Basic
Video duration: 07:35
This video show how a B model is transformed into C code and which constraints have to be met to be successful.
Level: Basic
Video duration: 12:22
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.
Level: Basic
Video duration: 13:28
This video explains how to improve automatic proof performances and provides some hints about the relation between modelling and ease to prove.
Level: Basic
Video duration: 09:49
This video describes the B development cycle, provides metrics and explains how to reduce the complexity and to simplify the organisation of a project.
Level: Basic
Video duration: 07:55
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.
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 |