Spécification et vérification de code pour plate-forme embarquée

Abstract

La vérification est une procédure qui vise à assurer le bon fonctionnement d’un système, en général automatisé et critique, en garantissant qu’il vérifie certaines propriétés. De nos jours, les systèmes automatisés sont omniprésent : processus industriels, automobile, avionique, ferroviaire, énergie atomique... La présence de tels systèmes dans des applications critiques, couplée à leur complexité croissante, rend indispensable leur vérification de façon automatique afin de garantir la sûreté de leur fonctionnement. En plus, les contraintes économiques imposent souvent un temps de développement court, ce qui rend accru le besoin de méthodes de vérification efficaces et à coût réduit. Les méthodes formelles, incluant la méthode du ”Model-Checking”, ont été appliquées avec succès dans plusieurs domaines, entre autres, réseaux, protocoles de sécurité, protocoles de télécommunication et contrôle automatique. Ils permettent de produire une description, dite spécification du système en question, puis, à partir de la spécification, vérifier automatiquement les propriétés désirées avant d’implémenter le système. Les algorithmes de Model-Checking sont, en général, conçus pour la vérification totale du système considéré. Lorsque le graphe modélisant le système est de taille raisonnable, c’est à dire qu’il peut être géré par la mémoire principale, les méthodes de model-checking sont très efficaces dans l’exploration de ce graphe et la détection des erreurs éventuelles. Cependant, la plupart des systèmes logiciels réels, possèdent des graphes d’états de très grande taille. En effet, l’espace d’états, représentant tous les comportements possibles d’un système ou d’un protocole complexe est habituellement exponentiel en le nombre de processus le comportant. Cette évolution importante dans la taille du graphe connue sous le nom d’explosion combinatoire de la taille de l’espace d’états, constitue encore, même après plusieurs années de travail, l’obstacle principal de la vérification automatique par model checking.