Model checking
Le Model Checking est une technique de vérification automatique des systèmes informatiques (logiciels, circuits logiques, protocoles de communication). Il s'agit de tester algorithmiquement si un modèle donné, le système lui-même ou une abstraction du système, satisfait une spécification logique, généralement formulée en termes de logique temporelle.
Fonctionnement formel
Test de vacuité d'automate
La première étape du Model Checking consiste à exprimer le modèle considéré au moyen d'un graphe orienté, formé de nœuds et de transitions. Chaque nœud représente un état du système, chaque transition représente une évolution possible du système d'un état donné vers un autre état. Parallèlement, le système est décrit par un ensemble de propositions logiques atomiques (e.g. i=2, le processeur 3 est en attente, ...). Chaque état du graphe orienté est étiquetté par l'ensemble des propositions atomiques vraies à ce point d'exécution. Un tel graphe est appelé structure de Kripke.
La deuxième étape du Model Checking consiste à exprimer la négation de la formule de logique temporelle que nous souhaitons tester. La négation de cette formule est donc elle-même transcrite sous forme d'une structure de Kripke, capable de reconnaître exactement l'ensemble des exécutions satisfaisant la négation de la formule donnée. Par exemple, on pourra transcrire une formule LTL en un automate de Büchi non-déterministe (ou, parfois, en un automate de Rabin).
La troisième et dernière étape consiste à réaliser le produit cartésien synchrone des deux structures de Kripke obtenues précédemment. Si le langage reconnu par le produit est vide (pour une propriété d'accessibilité, mais plus généralement pour une propriété d'acceptation mettant en jeu la vivacité et l'équité), alors le système satisfait la formule de logique. Sinon, toute séquence appartenant au langage du produit constitue un contre-exemple à la spécification.