Gérard Berry
Algorithmes, machines et langages
Année 2014-2015
Prouver les programmes : pourquoi, quand, comment ?
Cinquième leçon : La vérification de modèles (model-checking)
Ce cours termine la présentation générale des méthodes de vérification formelle par la vérification de modèles, plus connue sous son nom anglais original de model-checking. Cette méthode est bien différente des précédentes car elle s’intéresse essentiellement aux programmes d’états finis, ceux dont on peut au moins conceptuellement dérouler complètement toutes les exécutions possibles en temps et espace fini. De plus, contrairement aux méthodes précédemment décrites, le model-checking s’intéresse principalement aux programmes parallèles. Le parallélisme peut y être synchrone comme dans les circuits ou les langages synchrones présentés les années précédentes, ou asynchrones comme dans les protocoles de communication, les réseaux et les algorithmes distribués. Le model-checking est né au début des années 1980, quasi-simultanément en deux endroits : Grenoble avec J-P. Queille et J. Sifakis, qui ont développé le système CESAR et sa logique temporelle, et les USA avec E. Clarke et E. Emerson qui ont développé la logique temporelle CTL et le système EMV. Ces travaux ont donné le prix Turing 2007 à Clarke, Emerson et Sifakis. Ils s’appuyaient eux-mêmes sur les travaux d’Amir Pnueli (prix Turing en 1996) sur la logique temporelle. Le model-checking s’est considérablement développé ensuite, et constitue certainement la méthode formelle la plus utilisée dans l’industrie, en particulier dans la CAO de circuits.
L’idée de base est de construire le graphe de toutes les exécutions possibles d’un programme, qu’on appelle son modèle. Ce modèle peut prendre la forme d’une structure de Kripke (logicien et philosophe de la logique modale), c’est-à-dire d’un graphe où les états sont étiquetés par des prédicats élémentaires, ou encore d’une structure de transitions, où les étiquettes sont portées par les transitions entre états. Une fois construit, le modèle devient indépendant du langage qui l’a engendré. Pour raisonner sur un modèle, un moyen très répandu est l’utilisation de logiques temporelles, définissent les propriétés temporelles à l’aide de propriétés élémentaires des états ou transitions et de quantificateurs sur les états ou les chemins de son graphe. On peut ainsi exprimer et vérifier des propriétés de sûreté (absence de bugs), comme « à aucun moment l’ascenseur ne peut voyager la porte ouverte », d’absence de blocages de l’exécution, ou de vivacité, comme « l’ascenseur finira par répondre à toutes les demandes des passagers » ou encore « chaque processus obtiendra infiniment souvent la ressource partagée s’il la demande infiniment souvent ».
Nous présenterons d’abord la logique CTL*, la plus générale, qui permet d’imbriquer arbitrairement les quantifications d’états et de chemin sur les structures de Kripke. Mais cette logique très expressive est difficile à utiliser et les calculs y sont d’un coût prohibitif. Deux sous-logiques différentes sont utilisées : LTL (Linear Temporal Logic), qui ne quantifie pas sur les états et considère donc seulement des traces linéaires, et CTL, logique arborescente qui permet de quantifier sur les chemins mais avec des restrictions par rapport à CTL*. Ces deux logiques sont d’expressivités différentes et ont chacune des avantages et des inconvénients que nous discuterons brièvement. LTL est la logique la mieux adaptées pour la vérification de propriétés de vivacité, comme le montre L. Lamport (prix Turing 2014) avec son système TLA+. Mais, au contraire, elle ne permet pas d’exprimer des prédicats sur l’existence de calculs particuliers.
La modélisation par systèmes de transitions, systématisée par R. Milner (prix Turing 1992) dans l’étude des calculs de processus communicants, permet de bien mieux composer les exécutions de ces processus parallèles. Une notion fondamentale introduite par Milner est la bisimulation, équivalence comportementale qui permet de comparer finement ce que peuvent faire ou ne pas faire les processus. Nous montrons que la réduction par bisimulation fournit une alternative très intéressante et intuitive aux logiques temporelles pour la vérification de modèles, en particulier en liaison avec les langages synchrones.
Une dernière façon de conduite la vérification de modèles est de remplacer les formules temporelles par des programmes observateurs, qui prennent en entrée les entrées et les sorties du programme à vérifier et ont pour charge d’envoyer un signal de bug s’ils détectent une anomalie. Cette méthode est en particulier idéale pour les langages synchrones comme Esterel et Lustre étudiés les années précédentes, car les observateurs peuvent être écrits dans ces mêmes langages de façon plus simple qu’en logique temporelle, au moins pour les propriétés de sûreté qui sont les plus importantes dans leur domaine d’application. Cette méthode n’est en fait pas disjointe des précédentes, cat les formules temporelles sont souvent traduites en automates observateurs pour la vérification.
Il faut noter que, dans tous les cas, le programme à vérifier évolue dans un environnement qu’il est important et souvent indispensable de modéliser aussi avec les mêmes techniques. La modélisation de l’environnement n’est pas forcément plus simple que celle du programme lui-même, et, particulièrement en logique temporelle, il faut s’assurer que le modèle d’environnement construit n’est pas vide, sous peine que toutes les propriétés à vérifier ne deviennent trivialement vraies. Cela demande d’étudier la satisfiabilité des formules d’environnement, ce qui n’est pas forcément simple.
Nous terminons le cours par une brève présentation de l’algorithmique du model-checking, qui se divise en deux grandes classes de méthodes et de systèmes associés. Les méthodes explicites énumèrent systématiquement les états et transitions possibles. Comme la taille du modèle peut être gigantesque, ces méthodes utilisent des machines massivement parallèles ainsi que de nombreuses façons de réduire la complexité de l’analyse : calcul à la volée du modèle et des propriétés, exploration aléatoire du graphe, réduction par utilisation par symétrie ou commutation d’actions indépendantes, abstractions diverses, etc. Les méthodes implicites, introduites plus tard, utilisent des représentations symboliques des espaces d’états et de transitions, par exemple en utilisant des fonctions caractéristiques d’ensembles. Leur avantage est que la taille des formules servant à l’exploration du modèle n’est plus associée à la taille de l’espace d’états, leurs inconvénients étant que leur temps de calcul est difficilement prévisible et leur implémentation sur machine parallèle problématique. Les Binary Decision Diagrams (BDDs), la plus ancienne des représentations implicites en calcul booléen, seront étudiés au cours suivant. La satisfaction Booléenne (SAT) ou modulo théories (SMT) devient de plus en plus la méthode de choix pour le model-checking implicite. Nous l’illustrerons sur l’exemple bien connu du Sudoku, pertinent ici même si sa résolution n’est pas vraiment du model-checking temporel. Comme les méthodes explicites, les méthodes implicites font appel à de nombreuses techniques pour lutter contre l’explosion exponentielle du temps de calcul ou de la taille mémoire. Elles seront étudiées les années suivantes.
Nous insisterons enfin sur deux propriétés essentielles des model-checkers, qui les rendent attirants pour les utilisateurs : le fait qu’ils ne demandent pas à leur utilisateur de connaître précisément les techniques qu’ils emploient, et leur faculté de produire des contre-exemples minimaux pour les propriétés fausses, qui est primordiale à la fois pour le débogage et la génération de tests.
