Vérification par Modèles

Une technique de vérification automatique qui explore exhaustivement l'espace d'états d'un modèle formel d'un système (généralement un système de transition à états finis) pour déterminer si le modèle satisfait une spécification exprimée dans une logique temporelle ou modale, et qui fournit des traces contre‑exemples lorsque la propriété est violée.

La vérification de modèles est le processus de vérification algorithmique qui explore l'espace d'états d'un modèle formel pour déterminer s'il satisfait une spécification donnée, souvent exprimée en logiques temporelles ou modales.