Modelling Software-based Systems
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 fourth course MsC in Computer Science is aimed at students on the IT Masters
course at the Maynooth University and is a special coocking for students of my colleague
Professor Rosemary Monahan, who is welcoming me every year. This course is a special
edition that is shorter than the first two courses, which is great news! The aim is to give
students the specific elements of the Event-B language and, above all, to encourage them
to follow a few tutorials.
- The first course MCFSI is part of the curriculum of the last yer students of Telecom
Nancy who are focusing on software engineering.
- The second course MsC in Computer Science is aimed at students on the IT Masters
course at the University of Lorraine.
- The third course DISCONT is aimed at Telecom Nancy students in their final year who
are specialising in software engineering and embedded systems. The course focuses on
hybrid systems and hybrid models. The work of the ANR DISCONT project (see website
at ANR or website at LORIA )
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.