• Votre sélection est vide.

    Enregistrez les diplômes, parcours ou enseignements de votre choix.

EC Aspects formels du génie logiciel

  • Composante

    Sciences Fondamentales et Appliquées

Description

Cette UE approfondit l’UE "Logiciels sûrs" du M1 en abordant d’une part différents aspects de la vérification formelle, et d’autre part en complétant celle-ci par une étude de cas reposant sur des outils utilisés dans l’industrie du logiciel.

L'enseignement se compose de deux parties.

1) La première partie concerne les modèles formels de la programmation, de la modélisation et de la spécification. En particulier les différentes approches de la vérification formelle (vérification déductive, model-checking, interprétation abstraite) de logiciels pourront être abordés. Les systèmes formels (munis de leur système de preuve) supports des différentes méthodes formelles de vérification seront étudiés.

2) La seconde partie est axée sur l'expérimentation des outils industriels de vérification formelle des logiciels. Les outils expérimentés seront par exemple la plateforme Why3, la plateforme Frama-C d’analyse de programmes C, Key l'outil de vérification de programmes Java ou d'autres outils de vérification formelle émergeant dans ce domaine très actif.

Lire plus

Objectifs

- Maîtriser les modèles formels de la programmation, de la modélisation et de la spécification.
- Mettre en oeuvre des outils industriels de vérification formelle des logiciels.

Compétences visée : maîtriser le développement d’une vérification formelle d’un logiciel. Savoir s’orienter dans les différentes technologies disponibles. Comprendre les enjeux d’une vérification formelle et la pertinence de sa mise en oeuvre.

Lire plus

Heures d'enseignement

  • Aspects formels du génie logiciel - CMCM20h
  • Aspects formels du génie logiciel - TDTD14h
  • Aspects formels du génie logiciel - TPTP16h

Pré-requis nécessaires

UE Logiciels sûrs et Génie Logiciel 1 et 2 de la première année du master d’Informatique. Notions de logique.

Lire plus

Compétences visées

Maîtriser le développement d’une vérification formelle d’un logiciel. Savoir s’orienter dans les différentes technologies disponibles. Comprendre les enjeux d’une vérification formelle et la pertinence de sa mise en oeuvre.

Lire plus