- Trainer/in: Karine Altisen
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.
Descriptif :
Les outils élémentaires de mathématiques discrètes, tels quel’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