LogoLogo

Come, David. Analyse de la qualité de code via une approche logique et application à la robotique

Come, David (2019). Analyse de la qualité de code via une approche logique et application à la robotique.

[img]PDF (Accès restreint. S'adresser à l'accueil de la BU Sciences de Toulouse) - Accès intranet - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
2655Kb

Résumé en francais

La qualité d'un code informatique passe à la fois par sa correction fonctionnelle mais aussi par des critères de lisibilité, compréhension et maintenabilité. C'est une problématique actuellement importante en robotique où de nombreux frameworks open-source se diffusent mal dans l'industrie en raison d'incertitudes sur la qualité du code. Les outils d'analyse et de recherche de code sont efficaces pour améliorer ces aspects. Il est important qu'ils laissent l'utilisateur spécifier ce qu'il recherche afin pouvoir prendre en compte les spécificités de chaque projet et du domaine. Il existe deux principales représentations du code : son arbre de syntaxe abstraite (Abstract Syntax Tree en anglais, ou AST) et le graphe de flot de contrôle (Control Flow Graph en anglais, ou CFG) des fonctions qui sont définies dans le code. Les mécanismes de spécification existants utilisent exclusivement l'une ou l'autre de ces représentations, ce qui est dommage car elles offrent des informations complémentaires. L'objectif de ce travail est donc de développer une méthode de vérification de la conformité du code avec des règles utilisateurs qui puissent exploiter conjointement l'AST et le CFG. La méthode repose sur une nouvelle logique développée dans le cadre de ces travaux : FO++ , qui une extension temporelle de la logique du premier ordre. Cette logique a plusieurs avantages. Tout d'abord, elle est indépendante de tout langage de programmation et dotée d'une sémantique formelle. Ensuite, elle peut être utilisée comme moyen de formaliser les règles utilisateurs une fois instanciée pour un langage de programmation donné. Enfin, l'étude de son problème de model-checking offre un mécanisme de vérification automatique et correct de la conformité du code. Ces différents concepts ont été implémentés dans Pangolin, un outil pour le langage C++. Étant donné le code à vérifier et une spécification (qui correspond à une formule de FO++ , écrite dans le langage utilisateur de Pangolin), l'outil indique si oui ou non le code respecte la spécification. Il offre de plus un résumé synthétique de l'évaluation pour pouvoir retrouver le potentiel code fautif ainsi qu'un certificat de correction du résultat. Pangolin et FO++ ont trouvé une première application dans le domaine de la robotique via l'analyse de la qualité des paquets ROS et formalisation d'un design-pattern spécifique à ROS. Une seconde application plus générale concerne le développement de programme en C++ avec la formalisation de diverses règles de bonnes pratiques pour ce langage. Enfin, on montre comment il est possible de spécifier et vérifier des règles intimement liées à un projet en vérifiant des propriétés sur Pangolin lui-même.

Sous la direction du :
Directeur de thèse
Wiels, Virginie
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Modélisation et Ingénierie des Systèmes (MOIS) ISAE/ONERA
Mots-clés libres :Logique - Robotique - Model-checking - Qualité du code - Vérification
Sujets :Informatique
Déposé le :16 Jul 2019 14:16