Conception Formelle

Informations

Langue d'enseignement : Français
Crédits ECTS: 6

Programme

  • Heures d'enseignement dispensées à l'étudiant : 48 heures
  • Temps de travail personnel : 102 heures

Objectifs et compétences

Objectifs :
Objectifs pédagogiques :

- La conception de systèmes et de logiciels peut etre rendue beaucoup plus fiable par l'utilisation de méthodes formelles. Le cours est une approche pragmatique de la conception formelle à partir d'études de cas, et de techniques éprouvées: la preuve, le raffinement et la vérification de modèles.

Compétences acquises :

- Capacité d'abstractions comportementales de systèmes (matériels et logiciel) à des fins de vérification de propriétés fonctionnelles et/ou dysfonctionnelles.

- Capacité d'abstraction et de raisonnement logiques sur des données, sur des instructions et des suites d'instructions à des fins de preuves de programmes.

Compétences :
  • Maîtriser l'expression écrite et orale de la langue française et ses techniques d'expression
  • Maîtriser l'expression orale et écrite de la langue anglaise et ses techniques d'expression
  • Comprendre et mettre en oeuvre l'intérêt et les principes de la démarche de recherche fondamentale et/ou appliquée
  • Construire et développer une argumentation.

  • Maîtriser les bases de la logique et organiser un raisonnement mathématique.
  • Être capable de traduire un problème simple en langage mathématique.
  • Modéliser une situation concrète en un énoncé formel au moyen d'outils (e.g., automates, langages, grammaires, graphes)
  • Utiliser les bibliothèques et outils logiciels usuels de son domaine de spécialisation
  • Comprendre et traduire sous forme algorithmique la spécification mathématique d'une méthode de son domaine de spécialisation
  • Comprendre une preuve de correction d'algorithme (e.g., variants/invariants, induction, convergence)
  • Ecrire une preuve de correction d'algorithme

Organisation pédagogique

le mode de fonctionnement de l'UE est présenté au début des enseignements

Contrôle des connaissances

Première session :

Contrôle continu, coefficient 1/3

Examen écrit (3h), coefficient 2/3

Seconde session :

Oral (coefficient 1)

Lectures recommandées

l'ensemble des références bibliographiques est communiqué au début des enseignements

Responsable de l'unité d'enseignement

Alain Griffault

Enseignants

la composition de l'ensemble de l'équipe pédagogique est communiquée au début des enseignements