Ouvrir cette fenêtre en pleine page
  • Imprimer
  • Partager
    • Courriel
    • Twitter
    • Facebook
    • del.icio.us
    • Viadeo
    • LinkedIn

Validation des spécifications formelles de la mise à jour dynamique des applications Java Card

(Document en Français)

Accès au(x) document(s)

Modalités de diffusion de la thèse :
  • Thèse consultable sur internet, en texte intégral.
  • Accéder au(x) document(s) :
    • https://www.theses.fr/2018LIMO0085/abes
    • https://theses.hal.science/tel-01977915
    Ce document est protégé en vertu du Code de la Propriété Intellectuelle.

Informations sur les contributeurs

Auteur
Lounas Razika
Date de soutenance
10-11-2018

Directeur(s) de thèse
Lanet Jean-Louis - Mezghiche Mohamed
Président du jury
Ahmed-Nacer Mohamed
Rapporteurs
Boukala-Ioualalen Malika - Imache Rabah
Membres du jury
Ahmed-Nacer Mohamed - Aït-Ameur Yamine

Laboratoire
XLIM - UMR CNRS 7252
Ecole doctorale
École doctorale Sciences et Ingénierie des Systèmes, Mathématiques, Informatique (Limoges ; 2018-2022)
Etablissement de soutenance
Limoges,
Université M'hamed Bougara de Boumerdès (Algérie)

Informations générales

Discipline
Informatique
Classification
Informatique

Mots-clés libres
Mise à jour dynamique des programmes, Méthodes formelles, Java Card, Correction de la mise à jour dynamique des programmes
Mots-clés
Systèmes embarqués (informatique),
Fichiers (informatique) -- Traitement,
Méthodes formelles (informatique)
Résumé :

La mise à jour dynamique des programmes consiste en la modification de ceux-ci sans en arrêter l'exécution. Cette caractéristique est primordiale pour les applications critiques en continuelles évolutions et nécessitant une haute disponibilité. Le but de notre travail est d'effectuer la vérification formelle de la correction de la mise à jour dynamique d'applications Java Card à travers l'étude du système EmbedDSU. Pour ce faire, nous avons premièrement établi la correction de la mise à jour du code en définissant une sémantique formelle des opérations de mise à jour sur le code intermédiaire Java Card en vue d'établir la sûreté de typage des mises à jour. Nous avons ensuite proposé une approche pour vérifier la sémantique du code mis à jour à travers la définition d'une transformation de prédicats. Nous nous sommes ensuite intéressés à la vérification de la correction concernant la détection de points sûrs de la mise à jour. Nous avons utilisé la vérification de modèles. Cette vérification nous a permis de corriger d'abord un problème d'inter blocage dans le système avant d'établir d'autres propriétés de correction : la sûreté d'activation et la garantie de mise à jour. La mise à jour des données est effectuée à travers les fonctions de transfert d'état. Pour cet aspect, nous avons proposé une solution permettant d'appliquer les fonctions de transfert d’état tout en préservant la consistance du tas de la machine virtuelle Java Card et en permettant une forte expressivité dans leurs écritures.

Informations techniques

Type de contenu
Text
Format
PDF

Informations complémentaires

Entrepôt d'origine
STAR : dépôt national des thèses électroniques françaises
Identifiant
2018LIMO0085
Numéro national
2018LIMO0085

Pour citer cette thèse

Lounas Razika, Validation des spécifications formelles de la mise à jour dynamique des applications Java Card, thèse de doctorat, Limoges, Université de Limoges, 2018. Disponible sur https://aurore.unilim.fr/ori-oai-search/notice/view/2018LIMO0085