 |  |  |  |  |
| | |
|||||||||||||
| INFO0060-1 | Vérification de systèmes parallèles et logique temporelle | ||||||||||||||
| |||||||||||||||
| Durée : | 30h Th, 30h Pr | ||||||||||||||
| |||||||||||||||
| ECTS : |
| ||||||||||||||
| |||||||||||||||
| Titulaire(s) : | Pascal Gribomont, Pierre Wolper | ||||||||||||||
| |||||||||||||||
| |||||||||||||||
| Aperçu général : | Le cours comporte deux parties. La première est consacrée à la vérification algorithmique de systèmes parallèles basée sur l'exploration de l'espace des états. Elle couvre les techniques d'exploration de l'espace des états, les optimisations possibles de cette exploration et son utilisation pour la vérification de formules de logique temporelle par ''vérification de modèle'' (model checking). Ce dernier problème est traité à l'aide des automates sur mots infinis auxquels une introduction est donnée. La deuxième partie introduit la méthode des invariants et des assertions inductives. On étudie des techniques permettant de construire des invariants et des techniques permettant de les valider. On s'intéresse spécialement aux outils permettant d'automatiser en partie le processus de vérification, et au cas particulier fréquent où la majorité des variables du système à vérifier sont booléennes. | ||||||||||||||
| |||||||||||||||
| Objectif du cours : | Introduire les bases théoriques et algorithmiques de la vérification des systèmes parallèles. | ||||||||||||||
| |||||||||||||||
| Pré-requis : | Notions de programmation parallèle (cours INFO012-0) et notions de logique (cours INFO051-0). | ||||||||||||||
| |||||||||||||||
| Travaux pratiques : | utilisation de systèmes de vérification | ||||||||||||||
| |||||||||||||||
| Organisation : | Cours théorique, exercices sur la matière théorique, exercices de vérification. | ||||||||||||||
| |||||||||||||||
| Notes de cours : | disponibles sur internet | ||||||||||||||
| |||||||||||||||
| Evaluation : | Examen oral | ||||||||||||||
| |||||||||||||||
| Contacts : | Enseignants : P. Gribomont - Tél. 04/366 26 67 - e-mail gribomont@montefiore.ulg.ac.be P. Wolper - Tél. 04/366 20 99 - e-mail pw@montefiore.ulg.ac.be Assistant: information non disponible actuellement. | ||||||||||||||
| |||||||||||||||
| Remarques : | Des informations concernant ce cours peuvent être consultées à l'adresse Web : http://www.montefiore.ulg.ac.be/~pw/cours/verif.html | ||||||||||||||
| |||||||||||||||
ULg : Administration de l'Enseignement et des Etudiants - Affaires Académiques
Responsable de l'information : Monique Marcourt, directrice A.E.E.
Date de validité des données : 23/01/2004
Réalisation SEGI