X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/c9035994deb49df7f4452f1f4737481b1caf4b17..264ef3c685ebeeda441b6663562a14a43cb2eae1:/demandeInscription/synthese.tex diff --git a/demandeInscription/synthese.tex b/demandeInscription/synthese.tex index a2761f2..38b3497 100755 --- a/demandeInscription/synthese.tex +++ b/demandeInscription/synthese.tex @@ -60,7 +60,7 @@ %les afficher complÚtement. pdftitle={Demande d'inscription à l'HDR de JF COUCHOT}, %informations apparaissant dans pdfauthor={Jean-Fran\c{c}ois Couchot}, %dans les informations du document - pdfsubject={Algèbre et géométrie} %sous Acrobat. + pdfsubject={Demande d'inscription à l'HDR de JF COUCHOT} %sous Acrobat. } @@ -149,7 +149,7 @@ Je relève de l'école doctorale 37 Sciences Pour l'Ingénieur et Microtechnique L'avis du directeur de l'équipe et du directeur de l'école doctorale est annexé à cette synthèse (section~\ref{sec:avis:directeur}). -\JFC{joindre l'avis de Raphale, d'Olga de Nicolas et de PH. Lutz} +\JFC{joindre l'avis de Raphaël, d'Olga de Nicolas et de PH. Lutz} \newpage @@ -157,7 +157,7 @@ annexé à cette synthèse (section~\ref{sec:avis:directeur}). On considère en entrée de la démarche une description mathématique d'un programme: par exemple une fonction enrichie avec une spécification du contexte dans lequel elle est invoquée (la pré-condition) et -une spécfication exprimant quelles propriétés sont garanties en retour (la +une spécification exprimant quelles propriétés sont garanties en retour (la post-condition). Lorsque pré-condition et post-condition sont équivalentes, on parle d'invariant. La thématique de \emph{vérification de programmes par preuve automatique} @@ -208,7 +208,7 @@ de 5000 lignes de Code C annoté fourni par Dassault aviation. -\subsection*{Publication issues de ces recherches} +\subsection*{Publications issues de ces recherches} \begin{enumerate} @@ -299,11 +299,246 @@ Analyse d'atteignabilit\'e d\'eductive. \newpage -\section{Exposé des recherches réalisées au cours de la période postdoctorale (5 pages maximum)} +\section{Exposé des recherches réalisées au cours de la période postdoctorale} +\JFC{chapeau à refaire} + + +\subsection{Convergence de systèmes dynamiques discrets} + +Un système dynamique discret (SDD) est une fonction $f$ +du $n$-cube ($\{0,1\}^n$) dans lui même et un mode opératoire +(parallèle, unaire, généralisé) qui peut être itéré +en synchrone ou en asynchrone. +Ils ont été étudiés à de maintes reprises~\cite{Rob95,Bah00,bcv02}. +Pour chacun de ces modes, il existe des critères (suffisants) de convergence +globale ou locale, souvent basés sur le fait que $f$ est +est un opérateur contractant ans un espace. + +Les modes asynchrones ont une dynamique avec plus de liberté +puisqu'ils autorisent chaque élément à modifier sa valeur avant +de connaître les valeurs des autres éléments dont il dépend. +Cependant, lorsque les calculs à effectuer sur certains n{\oe}uds +sont coûteux en temps et/ou que les temps de communication sont élevés, +ces modes peuvent présenter une convergence plus rapide que le cas synchrone. + +Dans~\cite{BCVC10:ir}, j'ai formalisé le mode des +\emph{itérations mixes} (introduit dans~\cite{abcvs05}) +qui combine synchronisme et asynchronisme. +Intuitivement, les n{\oe}uds qui pourraient engendrer des cycles dans +les itérations asynchrones sont regroupés dans une même classe. +Les noeuds à l'intérieur celle-ci groupe seront itérés de manière +synchrone et les itérations asynchrones sont conservées entre les groupes. +Pour gommer les différences entre les n{\oe}uds d'une même classe +lorsqu'ils sont vus depuis des n{\oe}uds extérieurs, j'ai défini le +mode des \emph{itérations mixes avec délais uniformes}. + + +Grâce à cette formalisation, j'ai pu énoncer puis démontrer un théorème +établissant que pour des conditions classiques de convergence des itérations +synchrones d'une fonction $f$, les itérations mixes à délai uniforme +convergent aussi vers le même point fixe. + + +L'étude de convergence de SDD est simple à vérifier +pratiquement pour le mode synchrone. Lorsqu'on introduit des stratégies +pseudo périodiques pour les modes unaires et généralisées, le problème +se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones +et mixes prenant de plus en compte les délais. +Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement ont déjà été présentées~\cite{BM99,bcv02}. +Cependant, comme ces implantations ne sont pas exhaustives, elles ne sont intéressantes que lorsqu'elles fournissent un contre-exemple. +Lorsqu'elles exhibent une convergence, +cela ne permet que donner une intuition de convergence, pas une preuve. +Autant que je sache, aucune démarche de preuve formelle automatique +de convergence n'avait jamais été établie. + + +J'ai montré dans~\cite{Cou10:ir} comment simuler +des SDDs selon tous les modes pour établir +formellement leur convergence (ou pas). +Cette simulation est basée sur l'outil SPIN de \emph{Model-Checking} +qui est une classe d'outils adressant le problème de vérifier automatiquement +qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion +combinatoire, les outils de cette classe +appliquent des méthodes d'ordre partiel, d'abstraction, +de quotientage selon une relation d'équivalence. + +Pour cela, j'ai présenté pour cela une démarche de traduction d'un SDD +dans PROMELA qui est le langage de SPIN. +J'ai énoncé puis prouvé ensuite la correction et la complétude de la démarche +Des données pratiques comme la complexité et des synthèses d'expérimentation +ont aussi été fournies. + + + +\subsection{Construction de fonctions chaotiques} +Pr. Christophe Guyeux de l'équipe AND a proposé dans sa thèse~\cite{guyeuxphd} +une caractérisation des fonctions $f$ de $\{0,1\}^n$ dans lui même +dont les itérations sont chaotiques selon Devanney dans certains mode: +il est nécessaire et suffisant que son graphe des itérations soit +fortement connexe. +J'ai proposé plusieurs méthodes de construction de +fonctions ayant de tels graphes d'itérations~\cite{bcgr11:ip,chgw+14:onp}. + +Dans la première~\cite{bcgr11:ip}, +l'algorithme enlève des arcs et vérifie ensuite que +la forte connexité est maintenue. +Même si cet algorithme retourne toujours des fonctions dont le graphe +des itérations est fortement connexe, il n'en est pas pour autant efficace +car il nécessite une vérification à posteriori de la +forte connexité sur le graphe entier composé de $2^n$ sommets. +La seconde méthode propose une solution à ce problème en présentant +des conditions suffisantes sur un graphe à $n$ sommets +qui permettent d'obtenir des graphes d'itérations fortement connexes. +Ce théorème a aussi été prouvé dans~\cite{bcgr11:ip} +et des instanciations effectives +ont été produites. +Une troisième méthode~\cite{chgw+14:onp} s'appuie sur les codes +de Gray, ou de manière équivalente sur les cycles hamiltoniens du graphe des +itérations: un cycle qui visite chaque n{\oe}ud exactement une fois est un +\emph{cycle hamiltonien}. +La démarche consiste à enlever du graphe un de ses cycles hamiltoniens dont +la démarche de génération est un problème connu. + +Ces méthodes ont permis d'étendre à l'infini la classe des fonctions +dont les itérations sont chaotiques. + + +\subsection{Apprentissage par réseaux neuronaux} +Nous disposons grâce aux travaux présentés à la section précédente d'un grand +nombre de fonctions dont les itérations sont chaotiques. +Nous avons entrepris d'étudier ces itérations et plus particulièrement leur +apprentissage par un réseau de neurones. +J'ai notamment pu contribuer à montrer pratiquement qu'il +est très difficile (voir impossible) de les prédire +à l'aide de tels outils d'intelligence artificielle~\cite{bcgs12:ij}. + + +Nous nous sommes attaqués à un problème physique d'optimisation de +l'écoulement d'un flux d'air le long d'un véhicule. +Ce flux peut être modifié si l'on active des injecteurs d'air placés +par exemple sur le becquet du véhicule. +Le flux d'air peut être modélisé à l'aide d'équations de Navier-Stokes +dont on ne connaît pas de méthode analytique de résolution. +De plus, le nombre de Reynolds calculé dans cette situation fait apparaître +que le régime est extrêmement turbulent, donc difficile à prévoir. +Nous avons souhaité +continuer nos expériences d'apprentissage à l'aide +de réseau de neurones dans ce contexte~\cite{cds12:ip,cds13:ij}. + +Il est apparu comme judicieux de mémoriser les configurations +représentant l'état des actionneurs à l'aide de nombres binaires. +De plus les codes de Gray, dont deux mots adjacents ne diffèrent que d'un +bit se sont présentés comme une des manière de mémoriser les sorties du +réseau de neuronnes comme un seul nombre binaire. +Quand on sait que trouver un chemin hamiltonien (comme étudié dans la partie précédente) dans un +$n$-cube revient à trouver un code +de Gray dans un mot de $n$-bits. Les compétences acquises lors du travail +sur les chemins hamiltoniens ont ainsi pu être réutilisées et approfondies. +Les résultats pratiques quant à l'utilisation de ces codes ce sont cependant +révélés comme moins pertinents que l'utilisation de $n$ sorties. + +\subsection{Génération de nombres pseudo-aléatoires} + +Au commencement de ce travail, notre équipe disposait d'un générateur de nombres +pseudo-aléatoires (PRNG) +basé sur une seule fonction dont nous avions prouvé la chaoticité +des itérations, à savoir la négation booléenne vectorielle. Cependant pour +réussir les tests statistiques dédiées aux PRNGs, il était nécessaire d'itérer +un grand nombre (arbitraire) de fois cette fonction entre deux +sorties. + +Avec la production d'une grande collection de fonctions à itérations chaotiques, +j'ai proposé de répondre à la question suivante: comment engendrer des fonctions +dont les itérations vont produire des nombres simulant correctement l'aléa. +J'ai d'abord caractérisé les fonctions dont les itérations produisent des nombres +selon une distribution uniforme~\cite{bcgr11:ip}. Pour cela il a fallu réécrire +l'algorithme de génération comme une marche aléatoire dans une partie du $n$-cube, +de se ramener à une chaîne de Markov puis d'utiliser la théorie élaborée sur ce sujet +pour conclure. Par la même occasion, nous avons démontré que certaines fonctions +chaotiques ne peuvent pas produire un aléa suivant une distribution uniforme. +La sortie est biaisée. + +J'ai proposé ensuite des méthodes permettant de trouver de telles +fonctions en commençant par filtrer celles qui ne disposent pas +de cette caractéristique parmi toutes les fonctions chaotiques qui peuvent +être engendrées~\cite{bcgr11:ip}. J'ai démontré ensuite que supprimer +un cycle hamiltonien dans un $n$-cube permettait d'engendrer directement +des fonctions avec une telle caractéristique~\cite{chgw+14:oip}. +De plus, je me suis attaché à montrer l'importance +de l'équilibrage du chemin hamiltonien à enlever. + +Les générateurs produits ont d'abord été évalués avec succès +ont confirmé la qualité de +ceux-ci~\cite{bcgw11:ip,chgw+14:onp,chgw+14:oip} en se confrontant à +des batteries de tests telles que Die-Hard, NIST, TestU01. + +Plus récemment, nous avons entrepris de trouver des bornes du temps d'arrêt +d'obtention d'une distribution uniforme d'un générateur construit en enlevant un chemin hamiltonien équilibré dans un $n$-cube. Le travail est en cours de soumission +en journal international. + + + +\subsection{Masquage d'information} + +La propriété de transitivité des fonctions chaotiques implique que l'on peut +atteindre tout point depuis le voisinage de n'importe quel point. +Lorsqu'on cherche à embarquer une marque dans un media, +si l'on souhaite de plus que celle-ci soit robuste, \textit{i.e.}, +ne puisse pas être enlevée facilement, il paraît naturel d'embarquer +cette marque sur une grande partie du media. L'utilisation de fonctions chaotique +paraît alors judicieuse. + +J'ai participé à la formalisation de la méthode de +marquage de médias~\cite{bcg11b:ip,bcg11:ij} et particularisé +ceci à des images numériques fournissant un +nouveau contexte pour l'étude théorique et mathématique d'algorithmes de marquage. +La chaos-sécurité a été introduite comme une nouvelle propriété +de tels algorithmes de marquage comme existe +déjà la ($\epsilon$-)stego-securité. +Nous avons de plus montré la robustesse d'un tel marquage dans les +domaines fréquentiels usuel (DWT et DCT domains). + +Des instances de ces algorithmes ont été présentées en sélectionnant de manière +pertinenente les fonctions à itérer soit pour garantir une robustesse +élevée~\cite{bcfg12b:ip,bcfg+13:ip} soit pour masquer l'information dans le média +et être le moins détectable possible~\cite{bcfg12a:ip}. + +D'autre méthodes de watermarking ont été investiguées +particulièrement celles basées sur la Quantization Index Modulation (QIM), méthodes +étant supposées comme les plus robustes. Mes principales contributions +sur ce travail --en collaboration avec des membres de l'Université Antonine au Liban--, +ont été +d'intégrer ceci à du marquage de document PDF puis de +présenter ce problème comme un problème d'optimisation. +Grâce à une telle présentation nous avons pu trouver les paramètre optimaux +des méthodes QIM assurant à la fois robustesse et indetectabilité. +Le travail est en cours de soumission en journal international. + +Lorsque l'objectif visé est l'indétectabilité, on parle de \emph{stéganographie}. +Ce domaine a été adressé en critiquant notament les scenarios usuels d'évaluation +des algorithmes de steganographie. J'ai proposé un cadre complémentaire permettant +d'apprécier ces schémas de masquage~\cite{fccg15:ip}. +J'ai deplus participé à l'élaboration de l'algorithme STABYLO~\cite{ccg15:ij} +qui est un schéma de +stéganographie basé l'enfouissement de l'information dans les contours +d'une image. Ma contribution a principalement été la formalisation de l'algorithme, +son étude de complexité. Grâce a l'optimisation de cette dernière, +nous avons pu montrer +que cet algorihtme présente un excellent compromis entre la sécurité +fournie et sa complexité. + + + + + +\subsection{Application à la génomique} + +Core génome + + + +\subsection*{Publications issues de ces recherches} -(ou post-DEA pour les candidats autorisés à présenter leur demande sans -thèse), en identifiant les grandes thématiques de recherche, la démarche suivie et les -retombées en terme de publications et/ou de brevets ; \newpage \section{Perspectives de recherche (1 à 2 pages maximum)} @@ -341,8 +576,8 @@ Internationaux ; Nationaux ; Communications diverses. \section{Avis du directeur de l'Equipe}\label{sec:avis:directeur} \bibliographystyle{alpha} -\bibliography{biblio} -\include{Bibliographie} +\bibliography{abbrev,biblioand} + \end{document}