Spécification et Modélisation Informatiques

Code UE : NFP108

  • Cours
  • 6 crédits
  • Volume horaire de référence
    (+ ou - 10%) : 50 heures

Responsable(s)

Pierre COURTIEU

Public, conditions d’accès et prérequis

Prérequis : connaissance générale de l'informatique, bases de la programmation et de la méthodologie de développement.

Objectifs pédagogiques

Le but du cours est de présenter les outils mathématiques (logique, automates, logique de Hoare etc), utiles pour la spécification et la modélisation de systèmes informatiques. Ils constitue les base du génie logiciel, des réseaux, de la conception et du développement, des bases de données, des systèmes d'information et des systèmes transactionnels. A ce titre, ils sont sous-jacents à de nombreux enseignements du cursus.

Compétences visées

Savoir lire et écrire des spécification de systèmes utilisant des automates finis ou les formalismes logiques vus en cours. Être conscient de l'intérêt de formaliser des spécifications partielles.

Contenu

Outils conceptuels (un sous-ensemble significatif doit être traité)
  • Automates
    • Expressions régulières et automates finis à états
    • Propriétés de clôture
    • Algorithmes de déterminisation, minimisation
  • Calcul des Prédicats et Théorie des Ensembles
    • Calcul des Prédicats : validité, prouvabilité, correction, complétude, indécidabilité.
    • Théorie des Ensembles : ensembles, relations, fonctions
  • Preuve de programme
    • contrat de fonction, pré-post-conditions, invariants de boucles
Exemples d'utilisation
Les exemples du cours porteront sur des applications.
Pour les automates finis, ces applications comportent la modélisation d'automatisme (distributeur de billet, ascenseur), la modélisation de protocoles, des diagrammes
d'états-transition UML, la correction orthographique.  Par ailleurs, on illustrera l'ajout de contraintes OCL sur un modèle UML.
Le cours pourra aborder également les rapports entre spécification logique et le modèle relationnel des bases de données.  Les notions de dépendance fonctionnelle et de de forme normale seront mises en relation avec les concepts ensemblistes.
Concernant la preuve de programme, des algorithme simple sur les nombres et sur les graphes pourraont par exemple être utilisés.
Tous ces sujets ne seront pas nécessairement tous couverts par le cours, qui pourra mettre l'accent sur une partie seulement de ces exemples d'application.

Modalité d'évaluation

Examen écrit éventuellement complété d'une note de contrôle continu sanctionnant des devoirs, projets ou autres travaux personnels.

Cette UE apparaît dans les diplômes et certificats suivants

Chargement du résultat...
Patientez
Intitulé de la formation
Type
Modalité(s)
Lieu(x)
Intitulé de la formation
Type
Lieu(x)
Lieu(x)
Lieu(x) À la carte
Lieu(x) Package
Lieu(x) Paris
Lieu(x) À la carte
Lieu(x) Package
Lieu(x) Bretagne
Lieu(x) À la carte
Lieu(x) Paris
Lieu(x)
Lieu(x)
Lieu(x) Package
Lieu(x) Paris
Lieu(x) À la carte
Lieu(x) Paris
Lieu(x) À la carte
Lieu(x) Paris
Intitulé de la formation Type Modalité(s) Lieu(x)

Contact

EPN05 - Informatique
2 rue Conté 33.1.13A
75003 Paris
Tel :01 40 27 26 81
Safia Sider

Voir le calendrier, le tarif, les conditions d'accessibilité et les modalités d'inscription dans le(s) centre(s) d'enseignement qui propose(nt) cette formation.

Enseignement non encore programmé