Modelling Software-based Systems

Dominique Méry
LORIA & Telecom Nancy
Université de Lorraine
https://members.loria.fr/Mery
dominique.mery@loria.fr

May 15, 2025(4:09 P.M.)

This repository contains course notes, exercises, models and projects from three courses given as part of master’s level training on the Event-B formal method. It provides access to resources in the form of pdf files or Rodin archives. The relationship with the Atelier-B platform is explained.

The table of contents shows the summary of three main courses (at Université de Lorraine/University of Lorraine) based on our experiment using the Event-B method:

The Event-B method is based on a modelling language used to describe state-based models and safety properties of those state-based models. The originality of Event-B lies in its ability to enable incremental and proof-based modelling of reactive systems. The Event-B language contains both set notations and a first-order predicate calculus; it offers the possibility of defining models of reactive systems called machines and contexts and includes the refinement relationship that allows us to follow an incremental development methodology.

Contents
1 Documentation and Tools
2 Course EMU Event-B at Maynooth University
2.1 Slides for the course EMU
2.2 Tutorials
2.3 Event-B Models
3 Course MCFSI at Telecom Nancy
3.1 Slides for the course MCFSI
3.2 Tutorials
3.3 Project
3.4 Event-B Models
3.5 Past exams of the course MCFSI
4 Course MsC in Computer Science: Modelling and verifying software-based systems for Master in Compurer Science of the University of Lorraine
4.1 Slides of the course
4.2 Tutorials
4.3 Event-B Models
4.4 Project
4.5 Past exams of the Course MsC in Computer Science: Modelling and verifying software-based systems for Master in Comp
5 Course DISCONT: Modelling hybrid systems
5.1 Documentation
5.2 Slides for the course 2020-2021
5.3 Slides for the course 2021-2022
References