v2.11.0 (5223)

Enseignement ATHENS - TP45 : Formal Methods: Formal specification and verification of systems


Formal methods of system design means using mathematics to develop error-free systems. The mathematics needed is not complicated; it's just basic logic. The word "formal" means the use of a formal language, so that the system's operating logic can be machine checked.

This course is an introduction to the vast world of formal methods. It provides frameworks within which students can specify, develop, verify, and prove systems in a systematic, rather than ad hoc manner.

The course begins with review of propositional logic and predicate logic. Then we look at formal specifications, to cover set theoretic specification methods via B method, temporal specification via temporal logic and automata theory. The training includes both theoretical and practical parts. Each student will carry out an investigation of an existing formal verification system, applying it to a suitable problem of the student’s choice. Among possible projects will be the formal verification of problem solutions such as designing control systems, designing algorithms, or sophisticated data structures.

24 heures en présentiel

effectifs minimal / maximal:


Diplôme(s) concerné(s)

Parcours de rattachement

Pour les étudiants du diplôme Diplôme d'ingénieur

some programming experience, and some mathematical ability.

Format des notes

Numérique sur 20

Littérale/grade européen

Pour les étudiants du diplôme Diplôme d'ingénieur

Vos modalités d'acquisition :


L'UE est acquise si Note finale >= 10
  • Crédit d'UE électives acquis : 3

La note obtenue rentre dans le calcul de votre GPA.

Pour les étudiants du diplôme Programme d'Echange Européen ATHENS

Veuillez patienter