Exploiter la structure des modèles pour la vérification par la méthode CEGAR

Abstract

Cette thèse a eu pour but l'étude et la mise en oeuvre des méthodes de vérification par abstraction pour les modèles AltaRica. A cette effet, une méthode d'abstraction permettant l'utilisation d'une sous approximation de l'espace des états d'un système dans un algorithme CEGAR est présentée. Son utilisation permet d'accélérer l'algorithme CEGAR, ainsi que de réduire les ressources nécessaires lors de la vérification d'un modèle. Nous nous intéressons à une modélisation d'un sous ensemble du langage AltaRica , pour lequel une méthode d'abstraction hiérarchique est décrite, ainsi qu'un algorithme efficace permettant la vérification de contre-exemples issus de cette abstraction. La méthode proposée permet d'abstraire chaque composant de la hiérarchie indépendamment malgré la présence de priorités dans le modèle. Finalement l'implémentation de l'algorithme PCegar dans le model checker Mec 5 est présentée ainsi qu'une analyse de benchmarks sur des modèles académiques et un modèle industriel.