Next: Ingénierie de systèmes informatiques
Up: Réseaux et systèmes répartis
Previous: Algèbre de processus concurrents
ULG-INFO-060 --
P. Gribomont, P. Wolper --
30-30-0 -- Cours de 3ème cycle
Présenter les techniques modernes de vérification des systèmes
parallèles et en particulier celles basées sur la logique temporelle.
- Concepts élémentaires de programmation parallèle
ULG-INFO-040: Systèmes parallèles - Eléments de logique mathématique
ULG-INFO-051: Logiques pour l'intelligence artificielle
ULB-INFO-362: Eléments de logique appliquée à l'informatique
FUNDP-INFO-2209: Techniques d'Intelligence Artificielle - Initiation à la théorie des langages et des automates
ULG-INFO-016: Introduction à la calculabilité
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.
Exercices sur la matière théorique.
Projets impliquant l'utilisation de systèmes de vérification.
Examen écrit.
- 49
-
P. Gochet et P. Gribomont,
Logique. 2 Méthodes formelles pour l'étude des programmes.
Hermès, Paris, 1994.
- 50
-
G. Holzmann.
Design and Validation of Computer Protocols.
Prentice-Hall International Editions, 1991.
- 51
-
Z. Manna and A. Pnueli.
The Temporal Logic of Reactive and Concurrent Systems:
Specification.
Springer-Verlag, Berlin, 1992.
- 52
-
Z. Manna and A. Pnueli.
The Temporal Logic of Reactive and Concurrent Systems:
Safety.
Springer-Verlag, Berlin, 1995.
- 53
-
A. Thayse et al.
Approche logique de l'intelligence artificielle. 2 De la logique
modale à la logique des bases de données.
Dunod, Paris, 1989.
Next: Ingénierie de systèmes informatiques
Up: Réseaux et systèmes répartis
Previous: Algèbre de processus concurrents
Pierre-Yves SCHOBBENS
Thu Feb 4 19:08:21 MET 1999