ULg-INFO-056 -- Guy Leduc -- 30-30-00 -- Cours de 2ème cycle
Connaître et savoir appliquer des méthodes formelles pour spécifier et vérifier des logiciels répartis.
En utilisant un langage formel de spécification (LOTOS) comme support, ce cours a pour but d'étudier les méthodes formelles d'ingénierie de systèmes informatiques répartis. On y étudie différents styles de spécification de la dynamique et de l'architecture de ces systèmes, à différents niveaux d'abstraction. On traite ensuite des méthodes d'analyse de spécification : exécution symbolique, génération d'un modèle, vérification de relations entre modèles. L'accent est mis sur les principes et méthodes applicables à des systèmes de taille réaliste, et sur les logiciels de support utilisables.
En guise de travaux pratiques, les étudiants devront mener à bien un petit projet en appliquant méthodiquement les logiciels mis à leur disposition. La cotation se fera sur base de ce travail.