LogoLogo

Baklanova, Nadezhda. Formally verified analysis of resource sharing conflicts in multithreaded Java

Baklanova, Nadezhda (2014). Formally verified analysis of resource sharing conflicts in multithreaded Java.

[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
789Kb

Résumé en francais

Les systèmes multi-tâches temps-réels deviennent de plus en plus répandus de nos jours. La correction des systèmes multi-tâches est difficile à assurer, pourtant, la correction est critique pour les logiciels temps-réels. La vérification formelle aide à trouver les erreurs potentielles. Les conflits de partage de ressources qui peuvent produire une incohérence des données sont une sorte d'erreurs. Une solution est le verrouillage exclusif des ressources partagées qui peut mener à des temps d'exécution difficile à prédire, ou à l'interblocage dans le pire cas. La vérification des programmes est souvent effectuée par model checking. Un formalisme répandu de model checking des programmes temps-réels sont les automates temporisés. Ils permettent de vérifier certaines propriétés temporelles dans le modèle du programme et de trouver la séquence d'actions qui mènent à l'erreur. Il existe des algorithmes de vérification effectives pour des automates temporisés qui sont réalisés dans des outils de model checking largement utilisés. Nous avons développé un outil pour l'analyse statique de programmes Java multi-tâches qui trouve des conflits de partage de ressources possibles. Les programmes Java sont annotés avec des informations temporelles, et le modèle du programme est construit, en se basant sur les annotations. Le modèle est un système d'automates temporisés qui est vérifié par le model checker Uppaal. Des conflits de partage de ressources possibles sont trouvés par la vérification. Nous avons développé une étude de cas pour illustrer cette approche. L'analyse est complète: lorsqu'un conflit de partage de ressources peut apparaître dans un programme Java, il est détecté par notre analyse. Le modèle abstrait peut aussi sortir des alertes "faux positifs" qui ne correspondent pas à une configuration accessible dans le programme Java original. Pour s'assurer que la traduction des programmes Java vers des automates temporisés est correcte, nous avons formalisé la traduction dans l'assistant de preuves Isabelle. Nous avons prouvé que la traduction préserve la correspondance entre le programme et son modèle. Pour cela, nous avons développé une sémantique formelle de Java multi-tâche avec des annotations et des automates temporisés. Les preuves montrent que le modèle simule le comportement du programme Java original. Cela veut dire que chaque pas de la sémantique du code Java a une séquence de pas correspondante dans le modèle qui a le même effet sur l'état, c.à.d. des valeurs des variables, temps ou objets verrouillés. Le code vérifié de traduction est généré à partir de la traduction formalisée en utilisant le générateur de code d'Isabelle. Puis notre outil utilise le code vérifié pour générer le modèle d'un programme Java.

Sous la direction du :
Directeur de thèse
Féraud, Louis
Strecker, Martin
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Temps-réel - Systèmes embarqués - Méthodes formelles - Model checking - Vérification formelle - Analyse statique - Java - Automates temporisés
Sujets :Informatique
Déposé le :25 Mar 2015 13:02