OUTILS FORMELS DE MODÉLISATION

Ce cours introduit les premiers outils qui permettent de modéliser formellement et de raisonner sur des systèmes informatiques. L'accent est mis sur les concepts fondamentaux de modèles existants et de leurs propriétés formelles. L'expression puis la validation de propriétés des systèmes modélisés seront également abordées au moyen de techniques algorithmiques et de mécanismes de raisonnement symbolique.

Les outils élémentaires de mathématiques discrètes, tels que l'induction seront introduits et ensuite différents outils fondamentaux de modélisation seront abordés :

Introduction à la logique propositionnelle et du 1er ordre) et aux preuves :

• Formule logique comme outil de modélisation, syntaxe et sémantique
• Formule logique comme outil de raisonnement, déduction naturelle

Quelques modèles simples pour les systèmes à événements discrets :

• Machines à états discrets : automates simples, à entrées/sorties
• Spécification de propriétés et diagnostics

Documentation : Liste d’ouvrages de référence et notes de cours. Préparation pour : Génie logiciel.