Abstract

This repository contains course notes, exercises, models and projects from two courses given as part of master’s level training on modelling an verifying software-based systems. It provides access to resources in the form of pdf files, TLA files, ACSL files or Rodin files. Moreover, it aims to prepare students of the fourth year of University to apply modelling techniques for software-based systems. It is divided into two main parts:

• Part 1 MALG is shared by students in software engineering and in CPS engineering; the course is oganised in 6 weeks (6 lectures x 2h00 ) (6 tutorials x 2 h 00). Topics are transition systems, invariance, safety, fixed-point theory, induction principles, Floyd/Hoare proof systems,

• Part 2 is divided into two distinct streams:

  • MOVEX-SE is the course is oganised in 6 weeks (6 lectures x 2h00 ) (6 tutorials x 2 h 00)
  • MOVEX-CPS the course is oganised in 6 weeks (6 lectures x 2h00 ) (6 tutorials x 2 h 00)

The table of contents shows the summary of two main courses (at Université de Lorraine/University of Lorraine) based on our experiment using the modelling languages as TLA, Event-B and ACSL

• The first course MALG is part of the curriculum of the second year students of Telecom Nancy who are focusing on software engineering.
• The second course MOVEX is part of the curriculum of the second year students of Telecom Nancy who are focusing on embedded systems, as well as students of seconf year of ENSEM.