Langages formels et applications

Catalogue des cours de Télécom SudParis

Code

IGSF CSC 4504

Niveau

M1

Graduate

Graduate

Semestre

Spring

Domaine

Informatique

Programme

Programme Ingénieur

Langue

Français/French

Crédits ECTS

4

Heures programmées

45

Charge de travail

90

Coordonnateur(s)

Département

  • Informatique

Acquis d'apprentissage

A l’issue du module CSC 4504, les étudiants seront capables de
1- Comprendre les modèles mathématiques formels utilisés dans le raisonnement automatisé, les systèmes experts et l'apprentissage automatique
2- À partir d’un cahier des charges décrivant un système simple mais réaliste, les étudiants seront capables de :
a) Identifier la structure et les données caractérisant le système ainsi que ses fonctionnalités et les propriétés à vérifier
b) Identifier une hiérarchie des éléments composant le système qui reflèterait la fonctionnalité principale du système et sa décomposition en fonctionnalités secondaires
c) Appliquer la méthode formelle incrémentale B au système ainsi décomposé pour obtenir une spécification mathématique par raffinement qui permettrait de prouver les propriétés à vérifier.

Contenu

- Base de la logique :
- Approche pragmatique et liens avec des notions de base de l'informatique
- logique des propositions
- logique des prédicats
- logique typée et types abstraits
- équivalence entre logique et (certaines) représentations graphiques
- Langage B
- Méthode formelle, utilisée pour le développement de logiciels "critiques" (à haute sécurité)
- machines abstraites
- raffinements
- preuves
- aspects méthodologiques
- Bases de l'intelligence artificielle "symbolique"
- Une autre manière de concevoir et de programmer : programmation "déclarative" ou "par règles"
- notion d'espace de recherche
- représentation des connaissances
- le moteur d'inférences JESS (en Java)
- problèmes classiques (diagnostic, conception, planification, etc)
- raisonnement non monotone
- aspects méthodologiques

Mots-clés

langages formels, langage B, preuve de programmes, intelligence artificielle

Evaluation

1re session = Note de participation + de projet + d’exposés = C1
2e session = pas de 2ème session dans le cadre d’un projet
Note finale = C1

Compétences CDIO

Compétences principales

  • 2.1.1 - Apprendre à poser et formuler les problèmes
  • 2.1.2 - Modélisation
  • 4.4.1 - Processus de conception
  • 4.5.5 - Test, vérification, validation et certification
Fiche mise à jour le 28/08/2018