Model Checking

Ce cours porte sur des méthodes et des outils qui permettent de vérifier automatiquement si un système (software ou hardware) vérifie une spécification donnée.

Programme du cours

• La nécessité de méthodes formelles pour la vérification de systèmes hardware et software
• Rappels sur les systèmes réactives
• Le processus du model-checking et ces avantages
• Modélisation du système (structure de Kripke)
• Modélisation de la spécification (logiques temporelles CTL et LTL, fairness)
• Algorithmes de model-checking et leur complexité
• Améliorations: model-checking symbolique et model-checking à la volée
• Exemples réalistes