Model Checking

Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d'origine informatique ou électronique). Il s'agit de vérifier algorithmiquement si un modèle donné, le système lui-même ou une abstraction du système, satisfait une spécification, souvent formulée en termes de logique temporelle.

On peut distinguer 2 aspects du model checking:

• Il peut s'agir de démontrer qu'une certaine classe de propriétés, ou une certaine logique, est décidable, ou que sa décision appartient à une certaine classe de complexité.
• Il peut s'agir de rechercher des algorithmes efficaces sur des cas intéressants en pratique, de les implémenter, et de les appliquer à des problèmes réels.

Les premiers travaux sur le model checking de formules de logique temporelle ont été menés par Edmund M. Clarke et E. Allen Emerson en 1981, ainsi que par Jean-Pierre Queille et Joseph Sifakis en 1982. Clarke, Emerson et Sifakis se sont vu attribuer le Prix Turing 2007 pour leurs travaux sur le model checking.

Sommaire 1 Fonctionnement formel 1.1 Test de vacuité d'automate, méthodes explicites 1.2 Méthodes symboliques 1.3 Résolution SAT, SMT 1.3.1 Model checkers 2 Références

Fonctionnement formel

Test de vacuité d'automate, méthodes explicites

Une façon de procéder consiste à exprimer le système à vérifier et la propriété à tester sous la forme d'automates.

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 étiqueté 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.

Énumérer explicitement tous les états de l'automate peut être coûteux, c'est pourquoi on procède généralement par des méthodes symboliques, introduites par Ken McMillan et Ed Clarke.

Méthodes symboliques

Une approche, répandue pour la vérification de propriétés exprimées dans la logique temporelle arborescente CTL, est fondée sur la représentations des états et des transitions du système par des ensembles. De nombreuses méthodes de représentation d'ensembles d'états ont vu le jour. La plus connue utilise les diagrammes de décision binaire (BDD).

Le fonctionnement d'un model-checker symbolique consiste en l'obtention de points fixes pour déterminer les états accessibles ainsi que ceux qui satisfont une ou plusieurs propriétés. Ces points fixes sont calculés à l'aide de deux transformateurs de prédicats associés au franchissement des transitions : Le premier (Post) détermine, pour un ensemble d'états donnés, l'ensemble des états successeurs tandis que le second (Pre) est l'opération réciproque du premier. Ces techniques sont souvent plus efficaces pour les systèmes présentant un fort degré de concurrence mais font intervenir des mécanismes trop lourds pour des systèmes séquentiels.

Résolution SAT, SMT

Enfin, au lieu de considérer l'ensemble des traces d'exécution du système, on peut se limiter à des traces finies, de longueur bornée. L'existence d'une trace vérifiant une certaine propriété est équivalente à la satisfiabilité d'une certaine formule logique. Par exemple, si I identifie les états initiaux du système, F les états dont on veut tester l'accessibilité, et T est une relation de transition, alors on considérera .

Si les états du système sont données par des n-uplets de booléens, alors on se ramène au problème de la satisfiabilité d'une formule propositionnelle (problème SAT). Il existe divers logiciels, nommés SAT solvers, qui peuvent décider « efficacement en pratique » le problème SAT. De plus, ces logiciels fournissent habituellement un exemple de valuation satisfaisant la formule en cas de succès. Certains peuvent produire des éléments d'une preuve de non satisfiabilité en cas d'échec.

Une évolution récente est l'ajout, en sus de variables booléennes, de variables entières ou réelles. Les formules atomiques ne sont alors plus seulement les variables booléennes, mais des prédicats atomiques sur ces variables entières ou réelles, ou plus généralement des prédicats pris dans une théorie. On parle alors de satisfiabilité modulo une théorie (par exemple, on pourra considérer comme prédicats atomiques les égalités et inégalités linéaires). Une approche consiste à remplacer les prédicats atomiques par des variables booléennes supplémentaires, et à résoudre le système via SAT. S'il n'y a pas de valuation vérifiant la formule booléenne, la formule originale n'était pas non plus satisfiable. S'il existe une valuation, il faut vérifier que celle-ci soit cohérente par rapport à la théorie. Par exemple, si on a remplacé x < 5 par un booléen b₁ et x > 6 par un booléen b₂, la valuation b₁ = b₂ = vrai est incohérente par rapport à la théorie des inégalités linéaires. En pratique, il faudra donc savoir décider effectivement la satisfiabilité d'une conjonction de prédicats atomiques.

Model checkers

• Alloy
• APMC
• CADP
• Csml, Mcb
• CWB
• LoTREC
• Smv
• Spin
• Spot
• NuSMV

Références

• Automatic verification of finite state concurrent systems using temporal logic, E.M. Clarke, E.A. Emerson, and A.P. Sistla, ACM Trans. on Programming Languages and Systems, 8(2), p. 244–263, 1986.
• Symbolic Model Checking, Kenneth L. McMillan, Kluwer, (ISBN 0792393805), also online
• Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999, ISBN 0262032708
• Logic in Computer Science: Modelling and Reasoning About Systems, Michael Huth and Mark Ryan, Cambridge University Press, 2004. DOI

Informatique théorique
Théorie du calcul	Calculabilité Décidabilité et indécidabilité • Ensemble récursif • Problème de l'arrêt • Récursivement énumérable Modèle de calcul Automate fini • Automate cellulaire • Machine de Turing • Thèse de Church Modes de calcul Concurrence • Parallèlisme • Théorie de l'ordonnancement Mesure et échelle de complexité Réduction polynomiale • Problème NP-complet
Logique, syntaxe et sémantique	Logique mathématique Assistant de preuve • Calcul des prédicats • Correspondance de Curry-Howard • Fonction récursive • Lambda-calcul • Théorème d'incomplétude de Gödel • Théorie des types Grammaire formelle et systèmes de réécriture Compilation • Expression rationnelle • Grammaire formelle • Langage rationnel • Théorie des langages Sémantique Sémantique des langages de programmation • Sémantique dénotationnelle • Sémantique axiomatique • Sémantique opérationnelle Spécifier, vérifier et concevoir des programmes Interprétation abstraite • Méthodes formelles • Model checking
Algorithmique, complexité et mathématiques discrètes	Algorithmique Algorithme génétique • Algorithme glouton • Algorithme probabiliste • Complexité algorithmique • Diviser pour régner • Heuristique • Programmation dynamique Problèmes et algorithmes numériques Algorithme du simplexe • Géométrie algorithmique • Algorithme d'Euclide • Test de primalité Problèmes et algorithmes non-numériques Algorithmes de la théorie des graphes • Arbre (informatique) • Liste (informatique) • Table de hachage • Tas (informatique) Théorie des graphes Coloration de graphe • Problèmes de cheminement Recherche opérationnelle Optimisation • Optimisation combinatoire • Théorie de l'ordonnancement Données et codage Codage • Codage de l'information • Compression de données • Cryptage • Cryptanalyse • Cryptographie • Théorie de l'information