The evaluation of the gloss of human hair, following wet/dry chemical treatments such as bleaching, dyeing and perming, has received much scientific and commercial attention. Current gloss analysis techniques use constrained viewing conditions where the hair tresses are observed under directional lighting, within a calibrated presentation environment. The hair tresses are classified by applying computational models of the fibres' physical and optical attributes and evaluated by either a panel of human observers, or the computational modelling of gloss intensity distributions processed from captured digital images. The most popular technique used in industry for automatically assessing hair gloss is to digitally capture images of the hair tresses and produce a classification based upon the average gloss intensity distribution. Unfortunately, the results from current computational modelling techniques are often found to be inconsistent when compared to the panel discriminations of human observers. In order to develop a Gloss Evaluation System that produces the same judgements as those produced from both computational models and human psychophysical panel assessments, the human visual system has to be considered. An image based Gloss Evaluation System with gonio-capture capability has been developed, characterised and tested. A new interpretation of the interaction between reflection bands has been identified on the hair tress images and a novel method was developed to segment the diffuse, chroma and specular regions from the image of the hair tress. A new model has been developed, based on Hunter's contrast gloss approach, to quantify the gloss of the human hair tress. Furthermore, a large number of hair tresses have been treated with a range of hair products to simulate different levels of hair shine. The Tresses have been treated with different commercial products. To conduct a psychophysical experiment, one-dimensional scaling paired comparison test, a MATLAB GUI (Graphical user interface) was developed to display images of the hair tress on calibrated screen. Participants were asked to select the image that demonstrated the greatest gloss. To understand what users were attending to and how they used the different reflection bands in their quantification of the gloss of the human hair tress, the GUI was run on an Eye-Tracking System. The results of several gloss evaluation models were compared with the participants' choices from the psychophysical experiment. The novel gloss assessment models developed during this research correlated more closely with the participants' choices and were more sensitive to changes in gloss than the conventional models used in the study.

La programmation synchrone a ete proposee pour faciliter la conception et la programmation des systemes reactifs (systemes dont le role est de reagir continument a leur environnement physique, celui-ci etant incapable de se synchroniser avec le systeme). Ces systemes sont tres souvent repartis, que ce soit pour des raisons d'implantation physique, d'amelioration des performances ou de tolerance aux pannes. En outre, les travaux sur la compilation des langages synchrones ont conduit a utiliser une representation interne des programmes sous forme d'un automate d'etats fini : c'est le format OC. Ce travail porte donc sur la repartition automatique des programmes OC. La principale difficulte est d'assurer l'equivalence fonctionnelle et temporelle entre le programme centralise initial et le programme reparti, et de prouver cette equivalence, ce qui est indispensable dans le domaine du temps reel critique. Nous nous attachons egalement a minimiser localement la structure de controle de chaque programme reparti. Pour cela nous developpons un algorithme original de reduction des tests ``a la volee'' utilisant des techniques de bisimulation. D'autre part nous definissons completement l'environnement d'execution des programmes repartis. Ici notre principal souci est de fournir une solution la plus proche possible de l'execution centralisee. Enfin dans le but d'expliquer les desynchronisations introduites par la repartition, nous proposons une semantique originale du langage synchrone Lustre, semantique definie par des ordres partiels.

Le travail décrit dans cette thèse fait partie d'un effort de recherche au laboratoire VERIMAG pour créer une chaîne d'outils basée sur modèles (model-based) pour la conception et l'implantation des systèmes embarquées. Nous utilisons une approche en trois couches, qui séparent le niveau d'application du niveau implantation/architecture. L'application est décrite dans un langage de haut niveau qui est indépendante des détails d'implantation. L'application est ensuite transférée à l'architecture d'exécution en utilisant des techniques spécifiques pour que les propriétés demandées soient bien préservées.<br />Dans cette thèse, l'application est décrite en Simulink/Stateflow, un langage de modélisation très répandu dans le milieu de l'industrie, comme celui de l'automobile. Au niveau de l'architecture, nous considérons des implantation sur une plate-forme "mono-processeur" et "multi-tâches". Multi-tâches signifie que l'application est répartie en un nombre des tâches qui sont ordonnées par un système d'exploitation temps-réel (RTOS) en fonction d'une politique d'ordonnancement préemptive comme par exemple la priorité statique (static-priority SP) ou la date-limite la plus proche en priorité (earliest deadline first EDF).<br />Entre ces deux couches, on rajoute une couche de représentation intermédiaire basée sur le langage de programmation synchrone Lustre, développé à VERIMAG durant les 25 dernières années. Cette représentation intermédiaire permet de profiter des nombreux outils également développés à VERIMAG tels que des simulateurs, des générateurs de tests, des outils de vérification et des générateurs de code.<br />Dans la première partie de cette thèse, on étudie comment réaliser une traduction automatique de modèle Simulink/Stateflow en modèles Lustre. Coté Simulink, le problème est relativement simple mais nécessite néanmoins l'utilisation d'algorithmes sophistiqués pour inférer correctement les informations de temps et de types (de signaux) avant de générer les variables correspondantes dans le programme Lustre. La traduction de Stateflow est plus difficile à cause d'un certain nombre de raisons ; d'abord Stateflow présent un certain nombre de comportements "non-sûr" tels que la non-terminaison d'un cycle synchrone ou des sémantiques qui dépendent de la disposition graphique des composants sur un modèle. De plus Stateflow est un langage impératif, tandis que Lustre un langage de flots de données. Pour le premier problème nous proposons un ensemble de conditions vérifiables statiquement servant à définir un sous-ensemble "sûr" de Stateflow. Pour le deuxième type de problèmes nous proposons un ensemble de techniques pour encoder des automates et du code séquentiel en équations de flots de données.<br />Dans la deuxième partie de la thèse, on étudie le problème de l'implantation de programmes synchrones dans l'architecture mono-processeur et multi-tâche décrite plus haut. Ici, l'aspect le plus important est comment implanter les communications entre tâches de manière à ce que la sémantique synchrone du système soit préservée. Des implantations standards, utilisant des buffers de taille un, protégés par des sémaphores pour assurer l'atomicité, ou d'autres protocoles "lock-free" proposés dans la littérature ne préservent pas la sémantique synchrone. Nous proposons un nouveau schéma de buffers, qui préserve la sémantique synchrone tout en étant également "lock-free". Nous montrons de plus que ce schéma est optimal en terme d'utilisation des buffers.

Les travaux présentés dans ce document portent sur la vérification<br />de modèles de systèmes sur puce, au niveau transactionnel (TLM).<br />Nous présentons le niveau transactionnel et ses variantes, et<br />rappelons en quoi ce nouveau niveau d'abstraction est aujourd'hui<br />nécessaire en plus du niveau de transfert de registre (RTL) pour<br />répondre aux contraintes de productivités et de qualités de plus en<br />plus fortes, et comment il s'intègre dans le flot de conception.<br /><br />Nous présentons un nouvel outil, LusSy, permettant la vérification<br />formelle de modèles transactionnels écrits en SystemC. Sa structure<br />interne s'apparente à celle d'un compilateur: Une partie frontale,<br />Pinapa, qui lit le programme source, une extraction de la<br />sémantique, Bise, dans notre formalisme intermédiaire \hpiom, une<br />série d'optimisations dans le composant Birth, et des générateurs<br />de code pour les outils de preuves pour Lustre et SMV.<br /><br />Lussy est conçu et écrit de manière à avoir aussi peu de limitation<br />que possible sur la forme du code SystemC accepté en entrée. \pinapa<br />utilise une approche innovante qui lui permet de s'affranchir de la<br />plupart des limitations dont souffrent les outils similaires.<br />L'extraction de la sémantique implémente plusieurs constructions TLM<br />qu'aucun autre outil disponible aujourd'hui ne gère. Il ne demande<br />pas d'annotation manuelle du code source, toute la chaîne étant<br />entièrement automatisée.<br /><br />Lussy est capable de prouver formellement des propriétés sur des<br />modèles de petites taille, et ses composants sont réutilisables pour<br />des outils de preuve compositionnelle, ou d'analyse de code autre<br />que le model-checking qui passeront mieux à l'échelle que l'approche<br />actuelle.<br /><br />Nous présentons les principes de chaque étape de la transformation,<br />ainsi que notre implémentation. Les résultats sont donnés pour des<br />exemples simples et petits, et pour une étude de cas de taille<br />moyenne, EASY. Les expérimentations avec Lussy nous ont permis de<br />comparer les différents outils de preuves que nous avons utilisés,<br />et d'évaluer l'efficacité des optimisations que nous avons<br />implémentées.

Este trabalho apresenta-se como um exercício de leitura da ficção da escritora brasileira Clarice Lispector e tem por objetivos identificar, em contos e romances de sua autoria, a presença de questões relativas à História, à cultura e à sociedade brasileiras e examinar o modo como tais questões são representadas. Propõe-se, assim, uma leitura da obra de Lispector em que se realiza o cruzamento de uma forma de evidente caráter intimista com temas de natureza social, histórica e cultural, dando-se especial relevo à cidade e à constituição da experiência urbana no Brasil. Para tanto, são examinados, com maior detalhamento, os romances Perto do coração selvagem, O lustre, A cidade sitiada, A paixão segundo G.H. e A hora da estrela, além de vários contos da autora, publicados em diferentes coletâneas. Na construção dos argumentos que sustentam as análises dos textos literários, procurou-se colocar em confronto os textos da escritora com estudos de importantes pensadores do Brasil. / This study is a reading task of the fictional work by Brazilian writer Clarice Lispector and aims to identify, in her short stories and novels, issues concerning Brailian history, culture and society and the way in which such issues were portrayed. This study proposes the reading of the work by Brazilian novelist Clarice Lispector in which the crossing of introspective style with social, historical and cultural issues is suggested. The city and the construction of urban experience in Brazil are highlighted in this study. Thus, the novels Perto do coração selvagem, A cidade sitiada, A paixão segundo G.H. and A hora da estrela, as well as a number of short stories by Clarice Lispector, will be analysed in detail. In order to draw the arguments that support the analysis of the work by Lispector, her texts were compared with studies by some important Brazilian scholars.

Este trabalho apresenta-se como um exercício de leitura da ficção da escritora brasileira Clarice Lispector e tem por objetivos identificar, em contos e romances de sua autoria, a presença de questões relativas à História, à cultura e à sociedade brasileiras e examinar o modo como tais questões são representadas. Propõe-se, assim, uma leitura da obra de Lispector em que se realiza o cruzamento de uma forma de evidente caráter intimista com temas de natureza social, histórica e cultural, dando-se especial relevo à cidade e à constituição da experiência urbana no Brasil. Para tanto, são examinados, com maior detalhamento, os romances Perto do coração selvagem, O lustre, A cidade sitiada, A paixão segundo G.H. e A hora da estrela, além de vários contos da autora, publicados em diferentes coletâneas. Na construção dos argumentos que sustentam as análises dos textos literários, procurou-se colocar em confronto os textos da escritora com estudos de importantes pensadores do Brasil. / This study is a reading task of the fictional work by Brazilian writer Clarice Lispector and aims to identify, in her short stories and novels, issues concerning Brailian history, culture and society and the way in which such issues were portrayed. This study proposes the reading of the work by Brazilian novelist Clarice Lispector in which the crossing of introspective style with social, historical and cultural issues is suggested. The city and the construction of urban experience in Brazil are highlighted in this study. Thus, the novels Perto do coração selvagem, A cidade sitiada, A paixão segundo G.H. and A hora da estrela, as well as a number of short stories by Clarice Lispector, will be analysed in detail. In order to draw the arguments that support the analysis of the work by Lispector, her texts were compared with studies by some important Brazilian scholars.

Este trabalho apresenta-se como um exercício de leitura da ficção da escritora brasileira Clarice Lispector e tem por objetivos identificar, em contos e romances de sua autoria, a presença de questões relativas à História, à cultura e à sociedade brasileiras e examinar o modo como tais questões são representadas. Propõe-se, assim, uma leitura da obra de Lispector em que se realiza o cruzamento de uma forma de evidente caráter intimista com temas de natureza social, histórica e cultural, dando-se especial relevo à cidade e à constituição da experiência urbana no Brasil. Para tanto, são examinados, com maior detalhamento, os romances Perto do coração selvagem, O lustre, A cidade sitiada, A paixão segundo G.H. e A hora da estrela, além de vários contos da autora, publicados em diferentes coletâneas. Na construção dos argumentos que sustentam as análises dos textos literários, procurou-se colocar em confronto os textos da escritora com estudos de importantes pensadores do Brasil. / This study is a reading task of the fictional work by Brazilian writer Clarice Lispector and aims to identify, in her short stories and novels, issues concerning Brailian history, culture and society and the way in which such issues were portrayed. This study proposes the reading of the work by Brazilian novelist Clarice Lispector in which the crossing of introspective style with social, historical and cultural issues is suggested. The city and the construction of urban experience in Brazil are highlighted in this study. Thus, the novels Perto do coração selvagem, A cidade sitiada, A paixão segundo G.H. and A hora da estrela, as well as a number of short stories by Clarice Lispector, will be analysed in detail. In order to draw the arguments that support the analysis of the work by Lispector, her texts were compared with studies by some important Brazilian scholars.

Les systèmes embarqués modernes ont atteint un niveau de complexité qui fait qu'il n'est plus possible d'attendre les premiers prototypes physiques pour valider les décisions sur l'intégration des composants matériels et logiciels. Il est donc nécessaire d'utiliser des modèles, tôt dans le flot de conception. Les travaux présentés dans ce document contribuent à l'état de l'art dans plusieurs domaines. Nous présentons dans un premier temps de nouvelles techniques de vérification de programmes écrits dans des langages généralistes comme C, C++ ou Java. Dans un second temps, nous utilisons des outils de vérification formelle sur des modèles écrits en SystemC au niveau transaction (TLM). Plusieurs approches sont présentées, la plupart d'entre elles utilisent des techniques de compilations spécifiques à SystemC pour transformer le programme SystemC en un format utilisable par les outils. La seconde partie du document s'intéresse aux propriétés non-fonctionnelles des modèles~: performances temporelles, consommation électrique et température. Dans le contexte de la modélisation TLM, nous proposons plusieurs techniques pour enrichir des modèles fonctionnels avec des informations non-fonctionnelles. Enfin, nous présentons les contributions faites à l'analyse de performance modulaire (MPA) avec le calcul temps-réel (RTC). Nous proposons plusieurs connections entre ces modèles analytiques et des formalismes plus expressifs comme les automates temporisés et le langage de programmation Lustre. Ces connexion posent le problème théorique de la causalité, qui est formellement défini et résolu avec un algorithme nouveau dit de " fermeture causale ".