Contributions à l'analyse de systèmes par approximation d'ensembles réguliers

Dans cette thèse nous nous intéressons à une technique de vérification basée sur les approximations par réécriture dans le but de l'automatiser et d'étendre son domaine d'application. L'utilisation de cette technique permet la vérification de propriétés pour des systèmes informatique. Une sur-approximation des termes atteignables par réécriture est calculée et nous pouvons déterminer si des termes indésirables (représentant la propriété) appartiennent à la sur-approximation. Si ils n'appartiennent pas à la sur-approximation alors on est sûr que les termes indésirables ne sont pas atteignables par le système et la propriété est vérifiée, sinon nous ne pouvons pas conclure à cause de la sur-approximation. C'est dans ce cadre que se placent les contributions de cette thèse. Tout d'abord nous présentons une méthode de raffinement d'approximation, s'inspirant du paradigme CEGAR (Counterexample-Guided Abstraction Refinement), déterminant comment construire automatiquement une approximation qui ne contient pas de terme indésirable. Si cette construction échoue alors des termes indésirables sont atteignables et on peut conclure que le système analysé ne vérifie pas la propriété. De plus, à partir d'un graphe des réécritures, nous présentons comment vérifier trois modèles de propriétés LTL exprimant des conditions sur l'ordre d'application des règles de réécriture. D'autre part, nous présentons dans cette thèse deux nouvelles applications de cette technique : la vérification de spécifications écrites avec l'algèbre de processus CCS (sans renommage) et l'analyse d'atteignabilité par approximation de deux problèmes indécidables pour les machines de Turing