Afin de garantir qu'un programme respectera toutes ses contraintes temporelles, nous devons être capable de calculer une estimation fiable de son temps d'exécution au pire cas (WCET: worst case execution time). Cependant, identifier une borne précise du pire temps d'exécution devient une tâche très complexe du fait de la sophistication croissante des processeurs. Ainsi, l'objectif de nos travaux de recherche a été de définir une méthode formelle qui puisse s'adapter aux évolutions du matériel. Cette méthode consiste à développer un modèle du processeur cible, puis à l'exécuter symboliquement afin d'associer à chaque trace d'exécution un temps d'exécution au pire cas. Une méthode de fusionnement est également prévue afin d'éviter une possible explosion combinatoire. Cette méthode a pour principale contrainte de ne pas introduire trop d'imprécision sur les temps calculés. / To ensure that a program will respect all its timing constraints we must be able to compute a safe estimation of its worst case execution time (WCET). However with the increasing sophistication of the processors, computing a precise estimation of the WCET becomes very difficult. In this report, we propose a novel formal method to compute a precise estimation of the WCET that can be easily parameterized by the hardware architecture. Assuming that we developed an executable timed model of the hardware, we use symbolic execution to precisely infer the execution time for a given instruction flow. We also merge the states relying on the loss of precision we are ready to accept, in order to avoid a possible states explosion.

Cette recherche a été inspirée par les travaux de John Bowlby sur l’attachement ainsi que par les écrits psychanalytiques de Sigmund Freud et de Donald Winnicott sur le développement de la relation père-garçon. Trois objectifs ont été formulés dans la présente étude : A) Les jeunes garçons d’âge préscolaire pourraient-ils projeter, à travers quelques sessions de jeu symbolique libre, leurs représentations paternelles? B) S’ils les projettent, quelle est la nature de ces représentations paternelles? C) Existe-t-il une relation entre le type d’attachement (évalué par un instrument standard) et les représentations paternelles projetées dans le jeu symbolique libre? Dix garçons de quatre ans ont été filmés à la maison et dans une garderie pendant, en moyenne, quatre sessions totalisant par enfant, une durée moyenne de deux heures trente minutes de jeu symbolique. Le type d’attachement a été évalué à l’aide de l’Attachment Story Completion Task. Les résultats démontrent que l’ensemble des garçons ont été en mesure de projeter des représentations paternelles basées sur la figure du père. Tous ces garçons ont perçu le père comme une figure de protection et huit enfants sur dix ont exprimé verbalement leur attachement à ce dernier. Un enfant de type évitant (type A) n’a pas évoqué la figure du père dans son jeu. Ce père était rarement à la maison pour s’occuper de son garçon. Enfin, le dernier enfant, de type ambivalent (un enfant particulièrement agressif de type C), a présenté dans son jeu des interactions négatives avec le père et ce, tout au long des sessions de jeu symbolique. Il appert ainsi que le jeu symbolique permet à l’enfant de projeter des représentations de la figure paternelle. Ces représentations sont en lien avec le type d’attachement que l’enfant détient au moment de l’évaluation. / This research was inspired by the work of John Bowlby on infant attachment and the psychoanalytic writings of Freud and Winnicott on the father figure. Three objectives were formulated for this exploratory study; a) Will the young preschool boy spontaneously project his paternal representations in the context of a series of symbolic free play sessions? b) If so, what is the nature of the paternal representations? c) Is there a relationship between the type of attachment as evaluated with a standardized instrument and the paternal representation projected into the free play sessions? Ten four year old boys were filmed in their own homes and in the daycare setting during an average of four sessions each for a total of two and a half hours. The type of attachment was evaluated with the Attachment Story Completion Task. The results showed that all of the boys were capable of projecting paternal representations onto the father figures. All of the children perceived these figures as a source of protection and eight out of ten verbally expressed their attachment to them. One insecure boy (type A) did not invoke the father figure in his play and in real life his father was rarely at home. The remaining insecure boy (a very angry type C) showed consistent negative interaction with the father figure throughout the sessions. It seems that the symbolic play allow the child to project adequatly the representation of the father figure. These representations are linked to the attachment type that the children possessed at the moment of the evaluation.

Cette thèse porte sur la modélisation et vérification des signatures en ligne. La première partie a pour thème principal la modélisation biomécanique des mouvements de la main. Un modèle basé sur le critère de Minimum de Secousse (MS) a été choisi parmi plusieurs théories du contrôle moteur. Ensuite, le problème de la segmentation des trajectoires en traits qui correspondent au modèle cinématique choisi a été étudié, ce qui a conduit à la mise au point d'une méthode de segmentation itérative. Le choix du modèle et de la méthode de segmentation sont basé sur le compromis entre la qualité de reconstruction et la compression. Dans la deuxième partie, le modèle polynomial issu du critère de MS est volontairement dégradé. Les zéros non-Réels des polynômes sont jetés et les effets de cette dégradation sont étudiés dans une perspective de vérification biométrique. Cette dégradation est équivalente à la technique connue sous le nom d’Infinity Clipping, initialement appliqué à des signaux de parole. Pour les signatures en ligne, comme pour la parole, la préservation de l'information essentielle a été observée sur des tâches de vérification de signature. En fait, en utilisant seulement la distance de Levenshtein sur la représentation dégradée, un taux d'erreur comparable à ceux des méthodes plus élaborées a été obtenu. En outre, la représentation symbolique issue de l’Infinity Clipping permet d’établir une relation conceptuelle entre le nombre de segments obtenus par la segmentation itératif basée sur le MS et la complexité de Lempel-Ziv. Cette relation est potentiellement utile pour l'analyse des signatures en ligne et pour l’amélioration des systèmes de reconnaissance / This thesis deals with the modelling and verification of online signatures. The first part has as main theme the biomechanical modelling of hand movements associated to the signing gesture. A model based on the Minimum Jerk (MJ) criterion was chosen amongst the several available motor control theories. Next, the problem of signature trajectory segmentation into strokes that better fit the chosen kinematic model is studied, leading to the development of an iterative segmentation method. Both the choice of the model and the segmentation method are strongly based on the tradeoff between reconstruction quality and compression. On the second part, the polynomial model provided by the MJ criterion is intentionally degraded. The non-Real zeroes of the polynomials are discarded and the effects of this degradation are studied from a biometric verification perspective. This degradation is equivalent to the signal processing technique known as Infinity Clipping, originally applied to speech signals. On signatures, as for speech, the preservation of essential information was observed on signature verification tasks. As a matter of fact, using only the Levenshtein distance over the infinitely clipped representation, verification error rates comparable to those of more elaborate methods were obtained. Furthermore, the symbolic representation yielded by the infinity clipping technique allows for a conceptual relationship between the number of polynomial segments obtained through the Minimum Jerk-Based iterative segmentation and the Lempel-Ziv complexity. This relationship is potentially useful for the analysis of online signature signals and the improvement of recognition systems

No description available.

À l’île de La Réunion, la marche sur le feu est un cycle rituel hindou annuel qui dure dix-huit jours. Rythmé par des prières et des mises en scène, son acmé est la spectaculaire traversée pieds nus d’un tapis de braises ardentes. Les individus choisissent délibérément de se soumettre à l’épreuve du feu, ils se sacrifient en l’honneur de la divinité. Dans le cadre de l’anthropologie de la performance, par l’analyse du cycle rituel et des paroles des pratiquants, cette recherche propose d’appréhender les motivations qui exhortent un individu à s’engager dans cette pratique à l’intérieur de l’univers créole. Elle propose de découvrir les modalités par lesquelles l’individu abandonne l’espace sécure et fait face au risque. L’idée directrice de cette thèse est que l’implication dans le rituel n’est jamais sans réserve, elle est un choix entériné par un désir sous-jacent, plus ou moins conscient, de changement d’une situation que le pratiquant souhaite améliorer ou d’un problème qu’il entend régler. La préparation à l’épreuve demande de plonger dans l’intime, de scruter l’être au plus profond. Le rituel, dans son efficacité, a un impact sur la vie future. La marche sur le feu est, in fine, une réponse à un besoin de l’individu en quête de sens, un outil pour devenir l’artisan de sa propre vie. / In La Réunion fire-walking is an annual Hindu ritual which lasts for eighteen days. Rhythmed by prayers and representations, its acme is the spectacular barefoot walk across a pit filled with hot embers. The individuals choose deliberately to submit themselves to the trial by fire, they sacrifice themselves in honour of a divinity. Within the framework of the anthropology of the performance, by the analysis of the ritual and the words of the practitioners, this research analyses the motivations which exhort an individual to commit themselves to this practice in the Creole universe. It suggests exploring the modalities by which the individual abandons a secure space and faces risk. The leading idea of this thesis is that the implication in the rite is never without reserve, it is a choice confirmed by an underlying desire – more or less conscious – of changing a situation which the devout wishes to improve, or of a problem which the devout wants to solve. In preparation for the event, the devout dives deep into the intimate and scrutinises the inner self. The rite, in its efficacy, has an impact on the future life. Fire-walking is, in fine, an answer to a need for the individual who is in search of meaning and a tool to become the artisan of one’s own life.

La crise de l'ESB de 1996 semble avoir révélé un ensemble de dysfonctionnements de l'action publique (conflits d'intérêt au sein des institutions de l'Agriculture, expertise « confinée ») et été le prélude à une remise en ordre des secteurs de la sécurité sanitaire des aliments en Europe (notamment en France et en Grande-Bretagne) à travers les mêmes principes directeurs (agencification, division gestion/évaluation du risque, transparence, ouverture, etc.). En appréhendant cette histoire populaire de l'ESB comme un mythe d'action publique, en le restituant dans son historicité et en portant la focale sur les usages sociaux qui en sont faits, la thèse met à distance les discours fonctionnalistes et anhistoriques sur la réforme.<br />Adossée à une comparaison franco-britannique, elle a pour objectif de comprendre comment le changement est donné à voir dans un secteur d'action publique et contribue ce faisant à faire exister ce dernier en en rehaussant la légitimité administrative. Plus qu'un donné, le changement est appréhendé à travers sa dimension symbolique dont la mise en forme est constitutive des luttes pour la domination du secteur. Ce sont ces dernières qui construisent la crise, la temporalité de l'action publique (« la rupture ») et le caractère nécessaire du changement.<br />En développant une « comparaison transnationale », la thèse permet aussi de comprendre comment les processus réformateurs nationaux se synchronisent. Toutefois, plutôt que de postuler une conversion uniforme et top down à des « bonnes pratiques » internationales, elle rend compte de la « circulation circulaire » de biens symboliques relatifs au gouvernement des risques à travers les activités multiples et l'ubiquité sociale de « courtiers de l'international ». Importée dans les espaces domestiques, la référence étrangère est une arme et un enjeu des luttes sectorielles nationales. Sa traduction est sensiblement filtrée par les spécificités de l'espace d'appropriation, d'où le constat d'une convergence partielle entre les secteurs français et britannique.

Cette thèse propose une extension des méthodes classiques de chemins de «scan». On utilise des opérateurs combinatoires plus généraux à la place des multiplexeurs à une seule sortie. Ils peuvent comporter des entrées et des sorties multiples. Ils peuvent boucler sur eux-mêmes par l'intermédiaire d'une ou plusieurs bascules. Lorsqu'ils vérifient certaines propriétés de bijectivité et qu'ils forment une structure propageant de l'information, alors cette structure est aussi utile que les chaînes du «scan» complet et s'utilise de manière semblable. Elle permet aussi une approche hiérarchique du test des circuits. On montre comment tirer profit de cette méthode plus générale pour réduire l'impact de la méthode de «scan» complet sur les performances de circuits complexes implantant des fonctions mathématiques courantes ou des séquenceurs. Des résultats sont donnés pour le cas réel d'un circuit CMOS, très rapide, spécifique pour le réseau numérique large bande et pour lequel les contraintes en vitesse étaient primordiales

Cette thèse propose et analyse de nouvelles méthodes de synthèse logique. L'analyse concerne des outils de la "troisième génération" d'écriture de bases irrédondantes de fonctions booléennes, à savoir les minimiseurs dits symboliques. Cette génération de minimiseurs conduit à la solution optimale plus rapidement et avec moins d'espace mémoire que les heuristiques de la minimisation explicite. Elle permet également le calcul de la forme complémentée minimale sans être exposée à des problèmes d'explosion en complexité, ce qui permet d'aboutir à un choix efficace entre une fonction et son complément. Nous avons abordé ensuite les problèmes de granularité des expressions factorisées. Nous avons proposé une méthode originale de réinjection qui intègre d'une façon concurrente une phase de minimisation symbolique des expressions booléennes. Cette méthode a permis de "corriger" la granularité: d'une part, des expressions booléennes obtenues par la factorisation, d'autre part, des équations obtenues par une description de haut niveau de type VHDL. La méthode proposée peut être également appliquée en tant que minimiseur logique qui tient compte du partage de la logique entre les expressions booléennes, ce qui n'est pas possible avec un minimiseur logique local ou global. Les expériences pratiques et l'application sur les réseaux programmables de type CPLD sont concluantes. Enfin, nous avons proposé une méthode originale de l'exploration de l'espace des solutions des macro-générateurs de type additionneur. Cette méthode est fondée sur le filtrage des solutions générées et l'amélioration par dérivation d'une solution donnée. Cette approche peut être efficacement appliquée sur la macro-génération sous contraintes temporelles

This thesis studies the properties of finite automata recognizing sets of real vectors encoded in positional notation using an integer base. We consider both general infinite-word automata, and the restricted class of weak deterministic automata, used, in particular, as symbolic data structures for representing the sets of vectors definable in the first order additive theory of real and integer numbers. <br><br> In previous work, it has been established that all sets definable in the additive theory of reals and integers can be handled by weak deterministic automata regardless of the chosen numeration base. In this thesis, we address the reciprocal property, proving that the sets of vectors that are simultaneously recognizable in all bases, by either weak deterministic or Muller automata, are those definable in the additive theory of reals and integers. <br><br> Precisely, for weak deterministic automata, we establish that the sets of real vectors simultaneously recognizable in two multiplicatively independent bases are necessarily definable in the additive theory of reals and integers. For general automata, we show that the multiplicative independence is not sufficient, and we prove that, in this context, the sets of real vectors that are recognizable in two bases that do not share the same set of prime factors are exactly those definable in the additive theory of reals and integers. <br><br> Those results lead to a precise characterization of the sets of real vectors that are recognizable in multiple bases, and provide a theoretical justification to the use of weak automata as symbolic representations of sets. <br><br> As additional contribution, we also obtain valuable insight into the internal structure of automata recognizing sets of vectors definable in the additive theory of reals and integers.

Les systèmes embarqués sont de plus en plus intégrés dans les applications temps réel actuelles. Ils sont généralement constitués de composants matériels et logiciels profondément Intégrés mais hétérogènes. Ces composants sont développés sous des contraintes très strictes. En conséquence, le travail des ingénieurs de conception est devenu plus difficile. Pour répondre aux normes de haute qualité dans les systèmes embarqués de nos jours et pour satisfaire aux besoins quotidiens de l'industrie, l'automatisation du processus de développement de ces systèmes prend de plus en plus d'ampleur. Un défi majeur est de développer une approche automatisée qui peut être utilisée pour la vérification intégrée et la validation de systèmes complexes et hétérogènes.Dans le cadre de cette thèse, nous proposons une nouvelle approche compositionnelle pour la modélisation et la vérification des systèmes complexes décrits en langage SystemC. Cette approche est basée sur le modèle des SystemC Waiting State Automata (WSA). Les SystemC Waiting State Automata sont des automates permettant de modéliser le comportement abstrait des systèmes matériels et logiciels décrits en SystemC tout en préservant la sémantique de l'ordonnanceur SystemC au niveau des cycles temporels et au niveau des delta-cycles. Ce modèle permet de réduire la complexité de la modélisation des systèmes complexes due au problème de l'explosion combinatoire tout en restant fidèle au système initial. Ce modèle est compositionnel et supporte le rafinement. De plus, il est étendu par des paramètres temps ainsi que des compteurs afin de prendre en compte les aspects relatifs à la temporalité et aux propriétés fonctionnelles comme notamment la qualité de service. Nous proposons ensuite une chaîne de construction automatique des WSAs à partir de la description SystemC. Cette construction repose sur l'exécution symbolique et l'abstraction des prédicats. Nous proposons un ensemble d'algorithmes de composition et de réduction de ces automates afin de pouvoir étudier, analyser et vérifier les comportements concurrents des systèmes décrits ainsi que les échanges de données entre les différents composants. Nous proposons enfin d'appliquer notre approche dans le cadre de la modélisation et la simulation des systèmes complexes. Ensuite l'expérimenter pour donner une estimation du pire temps d'exécution (worst-case execution time (WCET)) en utilisant le modèle du Timed SystemC WSA. Enfin, on définit l'application des techniques du model checking pour prouver la correction de l'analyse abstraite de notre approche. / Embedded systems are increasingly integrated into existing real-time applications. They are usually composed of deeply integrated but heterogeneous hardware and software components. These components are developed under strict constraints. Accordingly, the work of design engineers became more tricky and challenging. To meet the high quality standards in nowadays embedded systems and to satisfy the rising industrial demands, the automatization of the developing process of those systems is gaining more and more importance. A major challenge is to develop an automated approach that can be used for the integrated verification and validation of complex and heterogeneous HW/SW systems.In this thesis, we propose a new compositional approach to model and verify hardware and software written in SystemC language. This approach is based on the SystemC Waiting State Automata (WSA). The SystemC Waiting State Automata are used to model the abstract behavior of hardware or software systems described in SystemC. They preserve the semantics of the SystemC scheduler at the temporal and the delta-cycle level. This model allows to reduce the complexity of the modeling process of complex systems due to the problem of state explosion during modeling while remaining faithful to the original system. The SystemC waiting state automaton is also compositional and supports refinement. In addition, this model is extended with parameters such as time and counters in order to take into account further aspects like temporality and other extra-functional properties such as QoS.In this thesis, we propose a stepwise approach on how to automatically extract the SystemC WSAs from SystemC descriptions. This construction is based on symbolic execution together with predicate abstraction. We propose a set of algorithms to symbolically compose and reduce the SystemC WSAs in order to study, analyze and verify concurrent behavior of systems as well as the data exchange between various components. We then propose to use the SystemC WSA to model and simulate hardware and software systems, and to compute the worst cas execution time (WCET) using the Timed SystemC WSA. Finally, we define how to apply model checking techniques to prove the correctness of the abstract analysis.