Vérification de modèle

La vérification de modèle (ou model checking), consiste vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété.

Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc.. Cela revient à vérifier automatiquement si ce modèle répond à une donnée spécification (alias décision correcte propriétés). En règle générale, on a à l’esprit des matériels ou des logiciels, alors que la spécification contient aussi des prérequis de sécurité telles que l’absence de blocages et d’états critiques similaires pouvant entraîner le plantage du système, ainsi que des exigences de réactivité.

Afin de résoudre un tel problème sur le plan algorithmique, le modèle et la spécification sont tous deux formulés dans un langage mathématique précis. À cette fin, le problème est formulé comme une tâche logique, à savoir vérifier si une structure donnée satisfait à une formule logique donnée. Ce concept général s’applique à de nombreux types de logique et de structures appropriées. Un modèle simple vérifiant le problème vérifie si une formule donnée dans la logique propositionnelle est satisfaite par une structure donnée.