Définitions

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.

Organisme de formation

CPF, Pole Emploi, Plan de formation   OF N°11755165975 - 17 rue etex, Paris

Recevez des exclus !

Abonnez-vous et recevez des infos en exclu

24pm academy
17 rue etex 75018 Paris
O6 62 55 OO 1O

Search