Aller au contenu principal

Chukri Soueidi

Lundi 13 Mai 2024

Ingénierie de l'instrumentation pour la vérification de l'exécution

Résumé:

La vérification à l'exécution est une technique de vérification dynamique cruciale pour le raisonnement formel sur les exécutions de programmes, applicable tant au développement d'applications qu'en ligne dans des environnements de production. L'instrumentation joue un rôle crucial pour garantir que les moniteurs reçoivent des traces précises qui abstraient les informations nécessaires du programme en exécution. Sinon, l'intégrité du processus de surveillance est compromise, rendant les résultats peu fiables. Cette thèse se focalise sur la surveillance à l'exécution et les programmes concurrents, en abordant trois défis principaux : la capture des traces correctes, le guidage efficace de l'instrumentation, et l'évaluation de la validité des traces collectées. Pour répondre à ces défis, nous introduisons BISM, un cadre d'instrumentation au niveau du bytecode pour les langages JVM, offrant des abstractions de haut niveau pour divers utilisateurs dans le domaine de la vérification à l'exécution. BISM permet l'extraction d'événements au niveau du bytecode, accommodant la surveillance de propriétés spécifiées avec divers niveaux de granularité. BISM permet également d'écrire des analyses statiques en spécifiant l'instrumentation. Il offre aux utilisateurs avancés la possibilité de modifier de manière non restreinte et flexible le code existant. Ces dernières caractéristiques sont essentielles pour déployer des moniteurs en ligne ou imposer certaines propriétés comme un ordre séquentiel d'événements concurrents. Nous introduisons aussi une méthode nouvelle pour la vérification à l'exécution résiduelle de propriétés paramétriques, réduisant les points d'instrumentation et applicable à des propriétés de sécurité. Pour les programmes concurrents, nous mettons en évidence les limites de l'utilisation de traces linéaires et introduisons une méthodologie de collecte de traces utilisant un algorithme d'horloge vectorielle en temps réel, minimisant l'impact sur l'exécution. Cette méthode intègre une relation de dépendance causale, permettant d'évaluer la validité des traces dans les programmes concurrents pour un verdict de surveillance fiable. Nos contributions sont évaluées à travers des expériences sur divers benchmarks et applications, utilisant BISM dans un contexte plus large d'analyse dynamique, y compris l'analyse de logs, la couverture des tests, et le profilage. Ces travaux améliorent la fiabilité et l'efficacité de cette surveillance pour les programmes concurrents, fournissant des outils pratiques pour l'avancement du domaine.

Mots clés

Verification a L’execution, Instrumentation, programmes concurrents, analyse dynamique Additional Information: A pot de thèse will follow the defense in the IMAG reception hall. This is a great opportunity to discuss the work presented and connect. Everyone is welcome.

Date et lieu

Lundi 13 Mai 2024 à 15h
Auditorium de l'IMAG

Composition du jury

Yliès Falcone
Maître de Conférences, Université Grenoble Alpes, Co-encadrant de thèse
Gwen Salaün
Professeur des Universités, Université Grenoble Alpes, Directeur de thèse
Walter Binder
Full Professor, Università della Svizzera Italiana, Rapporteur
Klaus Havelund

Senior Scientist, NASA Jet Propulsion Laboratory, Rapporteur
Saddek Bensalem
Professeur des Universités, Université Grenoble Alpes, Examinateur
Sylvain Hallé

Full Professor, Université du Québec à Chicoutimi, Examinateur
Julien Signoles
Ingénieur de Recherche, CEA Centre de Paris-Saclay, Examinateur

Publié le 7 mai 2024

Mis à jour le 14 mai 2024