• Votre sélection est vide.

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

Aspects formels du génie logiciel

  • ECTS

    6 crédits

  • 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 concerne les modèles formels de la programmation, de la modélisation et de la spécification. Les styles de programmation aussi bien dans le cas séquentiel que concurrent sont abordés. L’étude des systèmes formels (munis de leur système de preuve) supports des différentes méthodes formelles de vérification et de validation complète l’étude des langages de programmation. Des exemples d’application des méthodes formelles illustrent chaque type de méthode introduite. Une expérimentation d'une méthode et d'un outil de modélisation et de preuves formelles est menée, par exemple au travers de la méthode B et de l’atelier B.

2) La seconde concerne les outils industriels de vérification formelle des logiciels. Les outils expérimentés seront par exemple la plateforme Why3 (extraction de programmes OCaml), l’outil Krakatoa de vérification de programmes Java, la plateforme Frama-C d’analyse de programmes C, etc.

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.

Lire plus

Heures d'enseignement

  • Aspects formels du génie logiciel - CMCM25h
  • Aspects formels du génie logiciel - TDTD10h
  • Aspects formels du génie logiciel - TPTP15h

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