Vérification algorithmique

Par vérification algorithmique ou model checking, on entend un ensemble d’algorithmes et d’outils permettant de décider si un système (matériel et/ou logiciel) vérifie une propriété donnée. Ces techniques connaissent un succès industriel important car elles aident à accroître la confiance que peut avoir un concepteur dans le bon fonctionnement du système. Elles sont surtout appliquées à des programmes et systèmes matériels parallèles et réactifs, c’est à dire qui interagissent de manière continue avec leur environnement et où il est difficile de couvrir toutes les exécutions possibles par des tests. Au cas où la propriété n’est pas vérifiée par le système, l’algorithme génère un contre-exemple qui aide le concepteur à comprendre et à corriger le problème.

Ce module présente d’abord les concepts formels pour la modélisation formelle par des systèmes de transition, ainsi que des logiques temporelles (LTL, CTL, CTL*) dans lesquelles les propriétés peuvent être exprimées. Sont introduits alors les algorithmes fondamentaux de vérification correspondants à ces logiques, à l’aide d’automates et de calcul de points fixes. Le principal problème que pose l’application de ces techniques est l’explosion combinatoire, c’est à dire le grand nombre d’états possibles, et l’on étudiera des techniques dites symboliques (BDDs et bounded model checking), ainsi que certaines techniques de réduction ou d’abstraction de l’espace d’états qui doit être exploré. Dans certains cas intéressants, le système ou ses propriétés de correction peuvent dépendre du temps réel ou faire intervenir des aspects probabilistes, et quelques extensions des techniques de vérification algorithmique à ces classes de systèmes seront présentées.

La présentation des bases conceptuelles et algorithmiques de ces techniques de vérification sera accompagnée par celle d’outils performants et librement disponibles de vérification algorithmique, et par quelques études de cas qui illustrent l’applicabilité de la méthode en pratique.