Ce mémoire d'habilitation résume la majeure partie de mes recherches, depuis la fin de mon doctorat, fin 2004, jusqu'à aujourd'hui. Le but essentiel de mes recherches est le développement de méthodes fondées sur des bases mathématiques et performantes en pratique pour s'assurer de la correction des logiciels. J'utilise des approximations pour permettre une bonne performance, tandis que la validité des résultats est garantie par l'emploi exclusif de sur-approximations des ensembles des comportements des programmes. Ma recherche est basée sur l'interprétation abstraite, une théorie très puissante des approximations de sémantiques permettant aisément de les développer, les comparer, les combiner. Je m'emploie en particulier au développement de nouveaux composants réutilisables d'abstraction, les domaines abstraits, qui sont directement implantables en machine, ainsi qu'à leur utilisation au sein d'analyseurs statiques, qui sont des outils de vérification automatique de programmes. Mes premières recherches concernaient l'inférence de propriétés numériques de programmes séquentiels, tandis que mes recherches actuelles se tournent vers l'analyse de programmes concurrents, d'où le titre de ce mémoire. Les deux premiers chapitres de ce mémoire constituent une introduction, tandis que les suivants présentent mon travail d'habilitation proprement dit. Le premier chapitre est une introduction informelle à la problématique de l'analyse de programmes, aux méthodes existantes, leurs forces et leurs faiblesses. Le deuxième chapitre présente de manière formelle les outils dont nous aurons besoin par la suite : les bases de l'interprétation abstraite, quelques domaines abstraits existants et la construction d'analyses statiques par interprétation abstraite, ainsi que quelques résultats utiles que j'ai obtenu en doctorat. Le troisième chapitre est consacré aux aspects spécifiques de l'analyse de programmes concurrents. Cette recherche, très personnelle, a abouti à la construction d'une méthode d'analyse de programmes concurrents, paramétrée par le choix de domaines abstraits, et basée sur une notion d'interférence abstrayant les interactions entre threads. Ainsi, l'analyse construite est modulaire pour les threads. Cette méthode est reliée aux preuves rely-guarantee proposées par Jones, ce que nous montrons formellement dans une première partie. Nous construisons ensuite une analyse à grands pas basée sur les interférences, efficace et facile à implanter. Les deux dernière parties étudient les liens entre l'analyse et les modèles mémoires faiblement cohérents (désormais incontournables) ainsi que le raffinement de l'analyse pour tenir compte des propriétés spécifiques des ordonnanceurs temps-réels (nous étudions en particulier l'effet des priorités des threads et l'emploi d'objets de synchronisation). Le quatrième et le cinquième chapitres sont consacrés à la constructions de domaines abstraits. Ceux-ci ne sont pas spécifiquement liés au problème de la concurrence ; ils sont utiles à l'analyse de tous programmes, séquentiels comme concurrents. Le chapitre 4 étudie des domaines numériques inférant des égalités et inégalités affines, développés en collaboration avec Liqian Chen, alors doctorant en visite à l'ENS. La motivation première était l'emploi de nombres à virgule flottante afin d'améliorer l'efficacité du domaine des polyèdres, mais ces travaux ont également débouché sur la découverte de nouveaux domaines, basés sur les relations affines à coefficients intervalles, que nous présentons également. Le chapitre 5 étudie les abstractions de types de données réalistes, comme ceux rencontrés dans le langage C : les entiers machines, les nombres à virgule flottante, et les blocs structurés (tableaux, structures, unions). Nos abstractions modélisent finement les détails de l'encodage en mémoire des données afin de permettre l'analyse de programmes qui en dépendent (par exemple, ceux utilisant le type-punning). Ces abstractions sont motivées par nos expériences d'analyses, avec les outils Astrée et AstréeA, de programmes C industriels ; ceux-ci employant fréquemment ce type de constructions de bas niveau. Le sixième chapitre est consacré aux applications des méthodes présentées ci-dessus à la construction d'outils d'analyse statique. Il décrit en particulier mon travail sur l'outil Astrée que j'ai co-développé avec l'équipe Abstraction pendant et après mon doctorat, et qui a été industrialisé en 2009. Mes résultats théoriques et appliqués ont contribué au succès d'Astrée, tandis que celui-ci m'a fourni de nouveaux thèmes de recherches, sous la forme de problèmes concrets dont la résolution n'a pu se faire que grâce à des développements théoriques. Ce chapitre décrit également AstréeA, une extension d'Astrée utilisant l'abstraction d'interférences proposée plus haut pour l'analyse de programmes concurrents (Astrée étant limité aux programmes séquentiels). Il décrit également Apron, une bibliothèque de domaines abstraits numériques que j'ai co-développée. Il s'agit d'un outil plus académique, dont le but est d'encourager la recherche sur les domaines numériques abstraits. Le mémoire se conclue par quelques perspectives sur des recherches futures.

Ce mémoire présente une nouvelle approche pour le calcul de temps d'exécution au pire (WCET) de tâche temps-réel critique, en particulier en ce qui concerne les aléas dus aux caches mémoire. Le point général est fait sur la problématique et l'état de l'art en la matière, mais l'accent est mis sur la théorie elle-même et son formalisme, d'abord dans le cadre monotâche puis dans le cadre multitâche. La méthode utilisée repose sur une technique d'interprétation abstraite, comme la plupart des autres méthodes de calcul de WCET, mais le formalisme est dans une approche probabiliste (bien que déterministe dans le cadre monotâche) de par l'utilisation de chaînes de Markov. La généralisation au cadre multitâche utilise les propriétés proba- bilistes pour faire une évaluation pessimiste d'un WCET et d'un écart type au pire, grâce à une modification astucieuse du propagateur dans ce cadre. Des premières évaluations du modèle, codées à la main à partir des résultats de compilation d'applications assez simples montrent des résultats promet- teurs quant à l'application du modèle sur des programmes réels en vraie grandeur.

La connaissance de l'attitude, de l'altitude, de la segmentation du sol et du mouvement est essentielle pour la navigation d'un drone, en particulier durant les phases critiques de décollage et d'atterrissage. Dans ce travail de thèse, nous présentons un système stéréoscopique hybride composé d'une caméra fisheye et d'une caméra perspective pour estimer les paramètres de navigation d'un drone. À partir de ce capteur, une approche systémique est proposée. Contrairement aux méthodes classiques de stéréovision basées sur l'appariement de primitives, nous proposons des méthodes qui évitent toute mise en correspondance entre les vues hybrides. Une technique de plane-sweeping est suggérée pour déterminer l'altitude et détecter le plan du sol. La rotation et la translation du mouvement sont ensuite découplés : la vue fisheye contribue à évaluer l'attitude et l'orientation tandis que la vue perspective contribue à apporter l'échelle métrique de la translation. Le mouvement peut ainsi être estimé de façon robuste et à l'échelle métrique grâce à la connaissance de l'altitude. Cette méthode repose sur l'algorithme des 2-points complété par un filtre de Kalman. Nous proposons des approches robustes, temps réel et précises, exclusivement basées sur la vision avec une implémentation C++. Bien que cette approche évite l'utilisation de capteurs autres que les caméras, ce système peut également être appuyé par une centrale inertielle.

Le concept de réseau offre un modèle de représentation pour une grande variété d'objets et de systèmes, aussi bien naturels que sociaux, dans lesquels un ensemble d'entités homogènes ou hétérogènes interagissent entre elles. Il est aujourd'hui employé couramment pour désigner divers types de structures relationnelles. Pourtant, si chacun a une idée plus ou moins précise de ce qu'est un réseau, nous ignorons encore souvent les implications qu'ont ces structures dans de nombreux phénomènes du monde qui nous entoure. C'est par exemple le cas de processus tels que la diffusion d'une rumeur, la transmission d'une maladie, ou même l'émergence de sujets d'intérêt commun à un groupe d'individus, dans lesquels les relations que maintiennent les individus entre eux et leur nature s'avèrent souvent être les principaux facteurs déterminants l'évolution du phénomène. C'est ainsi que l'étude des réseaux est devenue l'un des domaines émergents du 21e siècle appelé la "Science des réseaux". Dans ce mémoire, nous abordons trois problèmes de la science des réseaux: le problème de la diffusion dans les réseaux sociaux, où nous nous sommes intéressés plus particulièrement à l'impact de la dynamique du réseau sur le processus de diffusion, le problème de l'analyse des réseaux sociaux, dans lequel nous avons proposé une solution pour tirer parti de l'ensemble des informations disponibles en combinant les informations sur la structure du réseau et les attributs des noeuds et le problème central de la collecte de données sociales, où nous nous sommes intéressés au cas particulier de la collecte de données en milieux sauvages.

La conception des systèmes multimédia embarqués présente de nombreux défis comme la croissante complexité du logiciel et du matériel sous-jacent, ou les pressions liées aux délais de mise en marche. L'optimisation du processus de débogage et validation du logiciel peut aider à réduire sensiblement le temps de développement. Parmi les outils de débogage de systèmes embarqués, un puissant outil largement utilisé est l'analyse de traces d'exécution. Cependant, l'évolution des techniques de tra¸cage dans les systèmes embarqués se traduit par des traces d'exécution avec une grande quantité d'information, à tel point que leur analyse manuelle devient ingérable. Dans ce cas, les techniques de recherche de motifs peuvent aider en trouvant des motifs intéressants dans de grandes quantités d'information. Concrètement, dans cette thèse, nous nous intéressons à la découverte de comportements périodiques sur des applications multimédia. Donc, les contributions de cette thèse concernent l'analyse des traces d'exécution d'applications multimédia en utilisant des techniques de recherche de motifs périodiques fréquents. Concernant la recherche de motifs périodiques, nous proposons une définition de motif périodique adaptée aux caractéristiques de la programmation paralléle. Nous proposons ensuite une représentation condensée de l'ensemble de motifs périodiques fréquents, appelée Core Periodic Concepts (CPC), en adoptant une approche basée sur les relations triadiques. De plus, nous définissons quelques propriétés de connexion entre ces motifs, ce qui nous permet de mettre en oeuvre un algorithme efficace de recherche de CPC, appelé PerMiner. Pour montrer l'efficacité et le passage à l'échelle de PerMiner, nous réalisons une analyse rigoureuse qui montre que PerMiner est au moins deux ordres de grandeur plus rapide que l'état de l'art. En plus, nous réalisons un analyse de l'efficacité de PerMiner sur une trace d'exécution d'une application multimédia réelle en présentant l'accélération accompli par la version parallèle de l'algorithme. Concernant les systèmes embarqués, nous proposons un premier pas vers une méthodologie qui explique comment utiliser notre approche dans l'analyse de traces d'exécution d'applications multimédia. Avant d'appliquer la recherche de motifs fréquents, les traces d'exécution doivent ˆetre traitées, et pour cela nous proposons plusieurs techniques de pré-traitement des traces. En plus, pour le post-traitement des motifs périodiques, nous proposons deux outils : un outil qui trouve des pairs de motifs en compétition ; et un outil de visualisation de CPC, appelé CPCViewer. Finalement, nous montrons que notre approche peut aider dans le débogage des applications multimédia à travers deux études de cas sur des traces d'exécution d'applications multimédia réelles.

La Tolérance aux pannes Byzantines (BFT) est de plus en plus cruciale avec l'évolution d'applications et en raison de la croissance de l'innovation technologique en informatique. Bien que des dizaines de protocoles BFT aient été introduites dans les années précédentes, leur mise en œuvre ne semble pas satisfaisant. Pour faire face à cette complexité, due à la dépendance d'un protocole d'une situation, nous tentons une approche qui permettra de sélectionner un protocole en fonction d'une situation. Ceci nous paraît, en s'inspirant de tout système d'encrage, comme une démarche nécessaire pour aborder la problématique de la BFT. Dans cette thèse, nous introduisons un modèle de sélection ainsi que l'algorithme qui permet de simplifier et d'automatiser le processus d'élection d'un protocole. Ce mécanisme est conçu pour fonctionner selon 3 modes : statique, dynamique et heuristique. Les deux derniers modes, nécessitent l'introduction d'un système réactif, nous ont conduits à présenter un nouveau modèle BFT: Adapt. Il réagit à tout changement et effectue, d'une manière adaptée, la commutation entre les protocoles d'une façon dynamique. Le mode statique permet aux utilisateurs de BFT de choisir un protocole BFT en une seule fois. Ceci est très utile dans les services Web et les " Clouds " où le BFT peut être fournit comme un service inclut dans le contrat (SLA). Ce mode est essentiellement conçu pour les systèmes qui n'ont pas trop d'états fluctuants. Pour ce faire, un processus d'évaluation est en charge de faire correspondre, à priori, les préférences de l'utilisateur aux profils du protocole BFT nommé, en fonction des critères de fiabilité et de performance. Le protocole choisi est celui qui réalise le meilleur score d'évaluation. Le mécanisme est bien automatisé à travers des matrices mathématiques, et produit des sélections qui sont raisonnables. D'autres systèmes peuvent cependant avoir des conditions flottantes, il s'agit de la variation des charges ou de la taille de message qui n'est pas fixe. Dans ce cas, le mode statique ne peut continuer à être efficace et risque de ne pas pouvoir s'adapter aux nouvelles conditions. D'où la nécessité de trouver un moyen permettant de répondre aux nouvelles exigences d'une façon dynamique. Adapt combine un ensemble de protocoles BFT ainsi que leurs mécanismes de commutation pour assurer l'adaptation à l'évolution de l'état du système. Par conséquent, le "Meilleur" protocole est toujours sélectionné selon l'état du système. On obtient ainsi une qualité optimisée de service, i.e., la fiabilité et la performance. Adapt contrôle l'état du système grâce à ses mécanismes d'événements, et utilise une méthode de "Support Vector Regrssion" pour conduire aux prédictions en temps réel pour l'exécution des protocoles (par exemple, débit, latence, etc.). Ceci nous conduit aussi à un mode heuristique. En utilisant des heuristiques prédéfinies, on optimise les préférences de l'utilisateur afin d'améliorer le processus de sélection. L'évaluation de notre approche montre que le choix du "meilleur" protocole est automatisé et proche de la réalité de la même façon que dans le mode statique. En mode dynamique, Adapt permet toujours d'obtenir la performance optimale des protocoles disponibles. L'évaluation démontre, en plus, que la performance globale du système peut être améliorée de manière significative. Explorer d'autres cas qui ne conduisent pas de basculer entre les protocoles. Ceci est rendu possible grâce à la réalisation des prévisions d'une grande précision qui peuvent atteindre plus de 98%dans de nombreux cas. La thèse montre que cette adaptabilité est rendue possible grâce à l'utilisation des heuristiques dans un mode dynamique.

Ce travail présente l'approche UML/PNO (Unified Modelling Language with Petri Net Objects) pour la spécification de systèmes temps réel. La méthode propose d'enrichir la description semi-formelle UML du système par une modélisation formelle basée sur les réseaux de Petri. Les concepts UML de sous-système et d'interface ont été étendus afin d'améliorer la description de la vue système en termes de tructuration, gestion de projet et organisation de la modélisation. L'objectif est également d'adapter la méthode de modélisation système à une approche " orientée composant " pour le temps réel. Le concept " d'objet composé " permet d'intégrer des spécificités temps réel au sein du composant (protocole de communication, contrainte temporelle, effet observable). Le comportement des objets est spécifié à l'aide des réseaux de Petri à places et transitions stochastiques temporelles afin de permettre la validation et la vérification du système en cours de spécification. L'approche de validation propose des traductions semi-automatiques des diagrammes UML en réseaux de Petri. Les techniques classiques de simulation et d'évaluation de performances peuvent alors être appliquées. Ces traductions présentent l'avantage de rassembler, sur un même modèle à réseau de Petri, tous les aspects dynamiques du composant apparaissant dans différents diagrammes UML et de vérifier ainsi la cohérence de son comportement et de son utilisation. La vérification utilise les techniques d'analyse formelle, basées sur l'utilisation conjointe du graphe de classes et de la logique linéaire. Une approche de vérification quantitative des contraintes temporelles est proposée au niveau de l'analyse des besoins et des exigences du système. Une partie de ce travail a été concrétisée par l'intégration d'un module (ArgoPNO) dans l'atelier de génie logiciel ArgoUML. A ce jour, une première automatisation de la démarche de vérification des contraintes temporelles est opérationnelle sur cet outil.

Avec l'utilisation de plus en plus répandue de la simulation numérique dans de nombreuses branches de l'industrie, le calcul haute performance devient essentiel à la société. Si les plates-formes de calcul parallèle de plus en plus puissantes continuent à être construites, leur utilisation devient cependant de plus en plus un casse-tête. En effet, leur complexité croît avec la multiplication des ressources de calcul et de stockage impliquées, leurs fonctionnalités hétérogènes, et leur répartition non-uniforme. De nouveaux outils logiciels sont nécessaires pour faciliter l'exploitation de ces plates-formes. Je présente tout d'abord mes travaux visant à rendre plus accessibles et portables les mécanismes de communication développés par les constructeurs de réseaux haute performance pour le calcul. J'ai appliqué ce principe d'une part aux réseaux traditionnels de type Ethernet, et d'autre part aux communications entre processus locaux, afin d'améliorer les performances du passage de messages (MPI) sans dépendre de technologies matérielles spécialisées. J'explique ensuite comment faciliter la gestion des calculateurs hiérarchiques modernes. Il s'agit, d'une part, de modéliser ces plates-formes en représentant l'organisation des ressources de manière suffisamment simple pour masquer les détails techniques du matériel, et suffisamment précise pour permettre aux algorithmes de prendre des décisions de placement ou d'ordonnancement ; d'autre part, je propose des outils améliorant la gestion des architectures modernes où l'accès à la mémoire et aux périphériques n'est plus uniforme. Cela permet d'améliorer les performances de bibliothèques de calcul parallèle en tenant compte de la localité.

Die Informatik ist von besonderer Bedeutung für die Gestaltung unser alltäglichen Lebensumstände und ist eine Schlüsseltechnologie des 21. Jahrhunderts. Die Fakultät für Informatik vertritt dieses Fachgebiet umfassend und kompetent mit anwendungsorientierten Schwerpunktsetzungen. In unseren Forschungsschwerpunkten - Eingebettete selbstorganisierende Systeme - Intelligente multimediale Systeme - Parallele verteilte Systeme bieten wir international wettbewerbsfähige Forschung und Entwicklung zu aktuellen Problemstellungen. Unsere Lehre basiert auf dem Leitmotiv der beständigen Erneuerung aus der Forschung. Hieraus abgeleitet bieten wir zeitgemäße Bachelor- und Masterstudiengänge mit hervorragenden Studienbedingungen. Die Fakultät hat den Anspruch eines möglichst persönlichen Umgangs zwischen Lehrkörper und Studenten. Mit der Schriftenreihe „Chemnitzer Informatik Berichte“ geben wir Einblicke in die Forschungspraxis der Fakultät. Dabei werden unterschiedliche Forschungsthemen aus den drei Forschungsschwerpunkten und allen Professuren der Fakultät vorgestellt. / Computer science, as a key technology of the 21th century, has an exceptional impact on our everyday life and living standards. The Faculty of Computer Science represents this scientific field in a comprehensive and proficient manner with an application-orientated choice of topics. In the fields of - Embedded and self-organizing systems - Intelligent multimedia systems - Parallel and distributed systems we offer research and development for current problems and challenges on an internationally competitive level. The guiding principle of our education is the continuous innovation through advances in research. Consequently, we are able to provide modern Bachelor and Master programs with excellent academic conditions. The faculty strives to provide a maximally personal interaction between students and staff. With the series of publications „Chemnitz Computer Science Reports“ we give insigths into the reasearch practice of the faculty. We present different subjects of research from the tree research fields and all of the professorships of the Faculty of Computer Science.

Le développement futur des performances sportives est un sujet de mythe et de désaccord entre les experts. Un article, publié en 2004, a donné lieu à un vif débat dans le domaine universitaire. Il suggère que les modèles linéaires peuvent être utilisés pour prédire -sur le long terme- la performance humaine dans les courses de sprint. Des arguments en faveur et en défaveur de cette méthodologie ont été avancés par différent scientifiques et d'autres travaux ont montré que le développement des performances est non linéaire au cours du siècle passé. Une autre étude a également souligné que la performance est liée au contexte économique et géopolitique. Dans ce travail, nous avons étudié les frontières suivantes: le développement temporel des performances dans des disciplines Olympiques et non Olympiques, avec le vieillissement chez les humains et d'autres espèces (lévriers, pur sangs, souris). Nous avons également étudié le développement des performances d'un point de vue plus large en analysant la relation entre performance, durée de vie et consommation d'énergie primaire. Nous montrons que ces développements physiologiques sont limités dans le temps et que les modèles linéaires introduits précédemment sont de mauvais prédicteurs des phénomènes biologiques et physiologiques étudiés. Trois facteurs principaux et directs de la performance sportive sont l'âge, la technologie et les conditions climatiques (température). Cependant, toutes les évolutions observées sont liées au contexte international et à l'utilisation des énergies primaires, ce dernier étant un paramètre indirect du développement de la performance. Nous montrons que lorsque les indicateurs des performances physiologiques et sociétales -tels que la durée de vie et la densité de population- dépendent des énergies primaires, la source d'énergie, la compétition inter-individuelle et la mobilité sont des paramètres favorisant la réalisation de trajectoires durables sur le long terme. Dans le cas contraire, la grande majorité (98,7%) des trajectoires étudiées atteint une densité de population égale à 0 avant 15 générations, en raison de la dégradation des conditions environnementales et un faible taux de mobilité. Ceci nous a conduit à considérer que, dans le contexte économique turbulent actuel et compte tenu de la crise énergétique à venir, les performances sociétales et physiques ne devraient pas croître continuellement.