Computing optimal pairings on abelian varieties with theta functions

David Lubicz1

Description

Computing optimal pairings on abelian varieties with theta functions David Lubicz1,2, Damien Robert3 1CLAR 2IRMAR, Universit de Rennes 1 1LFANT Team, IMB & Inria Bordeaux Sud-Ouest 23/06/2011 (Geocrypt, Bastia)

• computing optimal


• miller's algorithm


• theta functions


• optimal pairings


• let ? ?


• bordeaux - sud ouest

Sujets

• Theta function
• cours

Informations

• Publié par: profil-urra-2012
• Publié le: 01 juin 2011
• Nombre de lectures: 20
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

THESE


En vue de l'obtention du

DOCTORAT DE L’UNIVERSITÉ DE TOULOUSE DOCTORAT DE L’UNIVERSITÉ DE TOULOUSE

Délivré par l'Institut National Polytechnique de Toulouse
Discipline ou spécialité : Systèmes Informatiques Critiques


Présentée et soutenue par Thomas ROBERT
Le 24 juin 2009

Titre : Détection d’erreur au plus tôt dans les systèmes temps-réel
une approche basée sur la vérification en ligne


JURY
Isabelle PUAUT, Rapporteur, Professeur, Université de Rennes 1
Rachid GUERRAOUI, Rapporteur, Professeur, Ecole Polytechnique Fédérale de Lauasanne
Denis CLARAZ, Examinateur, Ingénieur expert, Continental Automotive France
Sébastien FAUCOU, Examinateur, Maître de Conférence, Université de Nantes 1 (IRCCyN)
François VERNADAT, Président, Professeur, INSA Toulouse (LAAS;CNRS)
Jean-Charles FABRE, Directeur de Thèse, Professeur, INP Toulouse (LAAS;CNRS)
Matthieu ROY, Co-Directeur de Thèse, Chargé de Recherche CNRS (LAAS;CNRS)

Ecole doctorale : Ecole Doctorale Systèmes
Unité de recherche : LAAS; CNRS
Directeur(s) de Thèse : Jean-Charles FABRE, Matthieu Roy

Remerciements
Les travaux présentés dans ce mémoire ont été réalisés au laboratoire d’Analyse et
d’Architecture des Systèmes au sein de l’équipe Tolérance aux fautes et Sûreté de Fonc-
tionnement informatique. Pour la qualité de vie que j’ai pu apprécier durant ces quatre
années, je remercie Messieurs Mallik Ghallab et Raja Chatila, les directeurs successifs du
laboratoire durant cette période, pour m’avoir accueilli dans leur laboratoire. Pour des rai-
sons similaires, je tiens à remercier Monsieur Jean Arlat et Madame Karama Kanoun, qui
ont dirigé le groupe TSF, pour m’avoir permis de m’intégrer dans l’équipe et ses activités
de recherche.
Vu le chemin parcouru et les obstacles surmontés, je suis particulièrement reconnais-
sant envers Messieurs Jean-Charles Fabre et Matthieu Roy, respectivement Professeur à
l’Institut National Polytechnique de Toulouse et Chargé de Recherches CNRS au LAAS-
CNRS. Ils ont tous les deux acceptés d’être mes directeurs thèse. J’ai énormément ap-
précié leur disponibilité, et leur soutien tout au long de mes travaux de recherche et de la
phase de rédaction. Je tiens à les remercier tout particulièrement pour leur enthousiasme,
leurs conseils et l’ambiance de travail qu’ils ont su créer durant ces quatre ans, encore une
fois merci.
J’ai été honoré que Monsieur François Vernadat, Professeur à l’Institut National des
Sciences Appliquées de Toulouse, ait accepté de présider mon jury de thèse. J’en profite
pour remercier également :
– Isabelle Puaut, Professeur à l’Université de Rennes I,
– Rachid Guerraoui, à l’École Polytechnique Fédérale de Lausanne,
– Sébastien Faucou, Maître de Conférence à l’Université de Nantes I,
– Denis Claraz, Ingénieur à Continental Automotive,
– Jean-Charles Fabre, Professeur à l’Institut National Polytechnique de Toulouse,
– Matthieu Roy, Chargé de Recherche CNRS au LAAS-CNRS,
pour l’honneur qu’ils m’ont fait en acceptant de participer à mon jury de thèse.
iiiJe suis particulièrement reconnaissant envers Madame Isabelle PUAUT et Monsieur
Rachid Guerraoui pour avoir accepté la charge de rapporteur.
Comme je l’ai souligné au début, le groupe de recherche TSF est une grande famille, je
tiens donc à remercier l’ensemble de ses membres pour l’ambiance qu’ils ont su instaurer.
J’ai en particulier bien aimé participer au réseau d’excellence européen ReSIST qui m’a
permis de tisser des liens assez fort avec de jeunes chercheurs européens. Je n’oublie pas
non plus l’ensemble des personnes travaillant dans les diérents services au LAAS : lo-
gistique, magasin, administration... Toutes ces personnes tendent à rendre la vie au LAAS
plus facile et plus confortable.
Sans les citer tous, je suis très reconnaissant envers les doctorants qui ont partagés
comme moi l’épreuve de force que représente une thèse. Ceux dont je parle se reconnaî-
tront. Pour finir, je tiens à remercier ma famille, et mes amis qui m’ont soutenu et parfois
un peu secoué lorsque je me laissais aller à ma tendance à voir le verre toujours à moitié
vide, merci à tous.Table des matières
Introduction 1
1 Contexte et Problématique 7
1.1 Enjeux de la conception d’un système temps-réel critique . . . . . . . . . 8
1.1.1 Etat et comportement d’une application . . . . . . . . . . . . . . 8
1.1.2 Contraintes comportementales temps-réel . . . . . . . . . . . . . 11
1.1.3 Plate-forme d’exécution et prédictibilité . . . . . . . . . . . . . . 11
1.1.4 La sûreté de fonctionnement du logiciel . . . . . . . . . . . . . . 13
1.1.5 Applications temps-réel tolérantes aux fautes . . . . . . . . . . . 15
1.2 Vérification à l’exécution . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.2.1 Principe de la vérification à l’exécution . . . . . . . . . . . . . . 19
1.2.2 Traces et signaux : les modèles d’exécution . . . . . . . . . . . . 25
1.2.3 Catégories de vérifieurs en-ligne . . . . . . . . . . . . . . . . . . 26
1.3 Observation et analyse . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1.3.1 De l’exécution d’un code vers les événements . . . . . . . . . . . 31
1.3.2 Etat du bloc d’analyse et synchronisation avec l’application . . . 33
1.4 Position de l’étude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1.4.1 Attributs orientés «détection» d’un vérifieur en-ligne . . . . . . . 34
1.4.2 Synthèse de la démarche suivie . . . . . . . . . . . . . . . . . . 36
2 Critère de Détection au plus tôt 39
2.1 Rappels sur les traces et leurs opérations . . . . . . . . . . . . . . . . . . 40
2.2 Historique d’une exécution et processus d’observation . . . . . . . . . . 41
2.2.1 Approche de modélisation suivie . . . . . . . . . . . . . . . . . . 41
2.2.2 Historique d’une exécution en cours . . . . . . . . . . . . . . . . 42
2.2.3 État du processus d’observation . . . . . . . . . . . . . . . . . . 43
2.2.4 Monotonie des observations . . . . . . . . . . . . . . . . . . . . 43
2.2.5 «Latence» et exactitude du processus d’observation . . . . . . . . 44
2.3 Symptômes d’erreur et apparition de l’erreur . . . . . . . . . . . . . . . . 46
v2.3.1 Symptômes d’erreur associés àSpec . . . . . . . . . . . . . . . 46
2.3.2 Date d’apparition de l’erreur . . . . . . . . . . . . . . . . . . . . 47
2.4 Latence de détection et détection au plus tôt . . . . . . . . . . . . . . . . 49
2.4.1 Contribution à la latence de détection . . . . . . . . . . . . . . . 49
2.4.2 Détection causale, «au plus tôt» . . . . . . . . . . . . . . . . . . 51
3 Synthèse d’un détecteur au plus tôt 55
3.1 Automates temporisés et traces temporisées . . . . . . . . . . . . . . . . 56
3.1.1 Rappel sur les automates finis non temporisés. . . . . . . . . . . 57
3.1.2 Les automates temporisés. . . . . . . . . . . . . . . . . . . . . . 58
3.1.3 Interprétation des automates temporisés . . . . . . . . . . . . . . 60
3.2 Synthèse du détecteur au plus tôt . . . . . . . . . . . . . . . . . . . . . . 63
3.2.1 Des symptômes vers l’analyse d’accessibilité . . . . . . . . . . . 64
3.2.2 Etude du comportement en-ligne . . . . . . . . . . . . . . . . . . 69
3.2.3 Test de validité d’un événement. . . . . . . . . . . . . . . . . . . 72
3.2.4 Calcul des échéances à partir de l’abstraction temporelle . . . . . 74
4 Prototypage et évaluation du détecteur 81
4.1 Les enjeux de l’implémentation . . . . . . . . . . . . . . . . . . . . . . . 82
4.1.1 Analyse du comportement attendu . . . . . . . . . . . . . . . . . 82
4.1.2 L’environnement Xenomai . . . . . . . . . . . . . . . . . . . . . 84
4.1.3 Conditionnement des données . . . . . . . . . . . . . . . . . . . 85
4.2 Réalisation et intégration du prototype . . . . . . . . . . . . . . . . . . . 89
4.2.1 Analyse des structures de contrôle de Xenomai . . . . . . . . . . 89
4.2.2 algorithmique et description du prototype . . . . . . . . 93
4.3 Évaluation du coût du détecteur . . . . . . . . . . . . . . . . . . . . . . . 105
4.3.1 Occupation de la mémoire . . . . . . . . . . . . . . . . . . . . . 106
4.3.2 Temps d’exécution . . . . . . . . . . . . . . . . . . . . . . . . . 108
Conclusion générale 121
Bibliographie 125Introduction
12
De manière historique, la notion d’application temps-réel est associ&#