Outils pour utilisateurs

Outils du site


formations:masters:ue:m2:modspec9

Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentesRévision précédente
formations:masters:ue:m2:modspec9 [2023/04/21 09:17] – supprimée - modification externe (Unknown date) 127.0.0.1formations:masters:ue:m2:modspec9 [2023/04/21 09:17] (Version actuelle) – ↷ Page déplacée de formations:masters:cours:m2:modspec9 à formations:masters:ue:m2:modspec9 treinen
Ligne 1: Ligne 1:
 +
 +
 +====== Modélisation et spécification (M2) ======
 +
 +
 +===== Description =====
 +
 +Ce cours aborde d'une part la construction de modèles formels pour la description du comportement des systèmes informatiques et d'autre part la construction de spécifications (les propriétés attendues) de ces systèmes. 
 +
 +===== Syllabus =====
 +==== Sujets centraux ====
 +
 +
 +
 +  - Modélisation
 +    * Les systèmes de transitions étiquetés 
 +    * La composition parallèle
 +    * Les réseaux de Petri
 +  - Spécification
 +    * Logique temporelle LTL 
 +    * Exemples de propriétés
 +    * Algorithmes de décision
 +    * Logique temporelle CTL 
 +    * Exemples et algorithmes
 +    * Comparaison d'expressivité
 +  - Utilisation d'outils de model-checking (PRISM, NuSMV,...)
 +
 +
 +===== Pré-requis =====
 +
 +  - Bonne maîtrise de la logique propositionnelle 
 +  - Automates finis 
 +  - Algorithmique dans les graphes
 +