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.
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.
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.
Video duration: 15:03
This video presents the founding notions of B: projects, libraries, modules, components, abstract machine, refinement, implementation, and proof.
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.
Video duration: 16:31
This video presents the concept of machine consistency and the details behind this concept including its formal definition.
Video duration: 22:10
This video explains how we can define and use sets and constants in abstract machines.
Video duration: 26:44
This video introduces the use of mathematical relations in abstract machines to store information.
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.
Video duration: 32:31
This video presents the mathematical definition of arrays and its use to describe the components behaviour.
Video duration: 19:30
This lecture presents how the B method provides support for non-determinism.
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.
Video duration: 21:57
Data Refinement - Part II.
Video duration: 32:06
In this lecture, we present how the refinement process allows the resolution of non-deterministic constructs.
Video duration: 43:07
This lecture presents a special sort of refinement component that constitutes the final refinement: IMPLEMENTATION.
Video duration: 26:43
This video presents how the B-Method provides support to loops, an essential programming construct.
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.
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.
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.
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.
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.
Video duration: 07:55
|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|