MF

Imprimer

MF : Modèles et formalités

Responsable : Antoine Beugnard (mail)

Équipe pédagogique : Antoine Beugnard, Fabien Dagnat, Serge Garlatti (mail)

Description

La notion de modèle est centrale en science. Tout ce qu'on manipule n'est finalement qu'un modèle du système que l'on souhaite étudier (System under Study – SuS), qu'on en parle, en fasse un dessin ou en construise une représentation mathématique. Le but de ce module est d'aborder la problématique de la modélisation (comment et pourquoi produire un modèle) en informatique. Pour atteindre ce but, nous présenterons plusieurs problèmes et montrerons quels outils syntaxiques et sémantiques ont été proposés pour les modéliser (bien si possible). Au delà d'un catalogue, une attention particulière sera posée sur les principes sous-jacents à ces outils de modélisation et de raisonnement.

Mots-clés: systèmes formels, logique, modèles

Pré-requis : Quelques formalismes mathématiques ; bases de la programmation ;

Savoir et savoir faire associés

À l'issu de cette formation les étudiants seront capables d'expliquer et de réaliser une démarche de modélisation en utilisant des outils formels (mathématiques) ou semi-formels (diagrammes). Des logiques, du lambda calcul ou des notations comme UML serviront d'illustration aux mécanismes de modélisation mis en oeuvre ainsi qu'aux utilisations de ces modélisations.

Structure générale et contenu

  • Introduction à la modélisation (2h)
    • Construire un modèle
    • Syntaxe et sémantique
    • Interprétation
    • Principes généraux
  • Modèles formels de calcul (8h)
    • Notion de sémantique
    • Formalisation pour la mécanisation du raisonnement
    • Eléments de lambda calcul (nom, substitution, réduction, confluence, type, induction, preuve)
    • Éléments de pi calcul (système de transitions étiquetées, équivalence de trace et bisimulation)
  • Logiques standards et non standards (8h)
    • Théories axiomatiques et théories des modèles,
    • Calcul des prédicats
    • Logiques modales
  • Synthèse et mise en perspective formel - semi formel (2h)
    • Modélisation semi-formelle (UML comme support) 
    • Diagramme de classe et points de variation sémantiques
    • Processus de modélisation

Références bibliographiques

  • Practical Formal Software Engineering, Bruce Mills
  • Models of Computation: An Introduction to Computability, Maribel Fernandez
  • Introduction aux méthodes formelles, Jean-François Monin
  • Logique Réduction Résolution, René Lalement
  • Communicating and mobile systems: the pi-calculus, Robin Milner

Modalités d'évaluation

  • Examen terminal écrit de 2h

Notes de cours

Buy cheap web hosting service where fatcow web hosting review will give you advices and please read bluehost review for more hosting information.