Model Checking
Le model checking vérifie de manière exhaustive si tous les états d'un système satisfont des propriétés de logique temporelle, en trouvant automatiquement les états contre-exemples qui les violent.
Objectif
Vérifier de manière exhaustive la sûreté et la vivacité des systèmes concurrents, en découvrant automatiquement les interblocages et les courses de données.
Mécanisme
Le système est modélisé comme une machine à états et les propriétés sont exprimées en logique temporelle (LTL/CTL). L'énumération explicite d'états ou les BDD symboliques parcourent tous les états. Si une propriété échoue, un chemin contre-exemple est produit. SPIN et NuSMV sont des outils courants.
Cas d’usage
- Vérification de la concurrence
- Vérification de protocoles
- Vérification du matériel