Application of reinforcement learning algorithms to software verification

Cette thèse présente une forme nouvelle de vérification de systèmes probabilistes en utilisant des algorithmes d’apprentissage par renforcement. Le développement de très grands et très complexes systèmes logiciels est souvent l’aboutissement d’un travail d’équipe. L’objectif est de satisfaire le client en lui livrant le produit spécifié, sans erreurs et à temps. Des erreurs humaines sont toujours faites lors du développement de tels systèmes, mais elles sont d’autant plus faciles à corriger si elles sont détectées tôt dans le processus de production. Pour ce faire, on a recours à des méthodes de vérification et de validation. Dans cette thèse, nous avons réussi à adapter des tech- niques d’apprentissage supervisé pour solutionner des problèmes de vérification de logi- ciels. Cette approche nouvelle peut-être utilisée, même si le modle complet n’est pas disponible, ce qui est une nouveauté en théorie de la vérification probabiliste. Dans cette thèse, nous ne nous intéressons pas seulement à vérifier si, oui ou non, un système se comporte exactement comme ses spécifications, mais aussi, à trouver, dans la négative, à quel point il s’en écarte.This thesis presents a novel form of system verification through reinforcement learning algorithms. Large and complex software systems are often developed as a team effort. The aim of the development is to satisfy the customer by delivering the right product, with the right quality, and in time. Errors made by developers will always occur when a system is developed, but their effect can be reduced by removing them as early as possible. Software verification and validation are activities that are conducted to im- prove product quality. In this thesis we will adapt the techniques used in reinforcement learning to Software verification to verify if implemented system meets its specifica- tions. This new approach can be used even if the complete model of the system is not available, which is new in probabilistic verification. This thesis main aim is not only to answer the question whether the system behaves according to its specifications but also to find the degree of divergence between the system and its specifications