Dissertations / Theses on the topic 'Évaluation des logiciels'

La course aux technologies nouvelles pousse de plus en plus les concepteurs de systèmes à introduire de la logique programmée là où hier on trouvait de la logique câblée. La grande souplesse du logiciel a un revers : la complexité. Si elle n'est pas maitrisée, elle dégrade considérablement la sûreté de fonctionnement de l'ensemble du dispositif. L'objet de la thèse est double dans un cadre où les logiciels étudiés traitent essentiellement des fonctions de sécurité. Le but était, premièrement d'acquérir un maximum de renseignement sur l'état de l'art de la conception et de la validation des logiciels. Le second objectif était de mettre au point une méthodologie d'évaluation de l'intégrité des logiciels. La démarche que nous avons définie est basée sur l'analyse des risques et sur la maitrise du comportement du logiciel. Cette démarche propose une évaluation sous deux aspects : le produit logiciel, et son processus de développement. Les exigences de vérifications sont modulables en fonction de la criticité fonctionnelle et structurelle du logiciel. La criticité structurelle a été définie en terme d'immunité de la structure vis-à-vis des défaillances des modules logiciels. Des études de qualimétrie sont menées pour démontrer la maintenabilité et la robustesse du code. A partir d'analyses de dépendances basées sur le slicing, le comportement des fonctions de sécurité peut être appréhendé par l'intermédiaire d'un indicateur de vulnérabilité. Cet indicateur caractérise la sensibilité des sorties du système par rapport à ses entrées. Ces études ont été automatisées au travers d'un outil d'analyse de code, allégeant ainsi le travail de l'évaluateur. Un exemple d'application de la méthode d'évaluation a été réalisée sur un système assurant le contrôle du mouvement des véhicules en sécurité intrinsèque

On constate aujourd'hui un certain engouement de la part des institutions françaises et européennes et du grand public vers les Nouvelles Technologies pour I ‘éducation. Mais à y regarder de plus près, force est de constater qu'en pratique l'engouement n'est que virtuel et que les didacticiels sont fréquemment ignorés, oubliés, sous utilisés voire même rejetés. L'échec relatif des cd-rom aujourd'hui peut en grande partie être attribué à leur faible qualité devant un public très exigeant, et qui a toutes les raisons de l'être devant leur potentiel inexploité. Des défauts de conception, des contenus trop pauvres, des interfaces inefficaces, de mauvais usages du multimédia, des stratégies pédagogiques inadaptées, sont autant d'exemples d'erreurs courantes. Ainsi, à la croisée de l'évaluation des logiciels en 1HM et en EIAO, nous proposons un questionnaire articulé autour d'une critériologie étendue couvrant les problèmes techniques, ergonomiques jusqu'aux aspects éducatifs. Nous nous inscrivons dans une démarche orientée vers l'aide à l'évaluation, la méthode qui exploite ce questionnaire permet donc une adaptation dynamique du parcours, la capitalisation des impressions subjectives de I ‘évaluateur et la production de résultats contextualités grâce à l'application de calculs originaux : décomposition des questions en caractérisation/évaluation, application de notes exponentielles, pondérations des critères, confrontation des calculs et des impressions subjectives, etc. Enfin, nous proposons un prototype logiciel baptisé EMPI (Evaluation des logiciels Multimédias Pédagogiques Interactifs) qui instrumente notre méthode. Ces travaux ont été développés dans le cadre du pôle régional Nouvelles Technologies Educatives, soutenu financièrement par le Conseil Régional de Picardie.

L'augmentation de la duree du developpement, de la complexite et de la criticite des taches a automatiser pour la realisation de logiciels a rendu de plus en plus difficile la satisfaction de leur qualite. De ce constat est ne le besoin de mesurer les produits logiciels afin de comprendre comment leurs aspects internes (tels que la taille, le couplage ou encore la complexite) nuisent a leur qualite externe telle que leur fiabilite, leur maintenabilite ou leur productivite, et ce afin de pouvoir prendre les decisions pour les ameliorer. De nombreuses metriques ont ete definies mais un manque de rigueur dans leur definition et leur application n'a pas permis d'obtenir les resultats escomptes dans l'amelioration des logiciels. La definition des metriques manque souvent de precisions sur ce qui est mesure, empechant ainsi leur critique et leur reutilisation de maniere efficace. De plus, leur definition ne s'insere pas dans une demarche coherente prenant en compte un but initial. L'application des metriques, qui se refere a l'utilisation des techniques statistiques aux valeurs fournies par les metriques, est trop souvent bafouee. Les caracteristiques des donnees collectees sont peu souvent prises en compte pour le choix des techniques statistiques impliquant ainsi une interpretation des resultats qui entraine des prises de decision d'amelioration inadequates aux problemes rencontres. Nous presentons une demarche permettant l'evaluation d'attributs internes et externes d'entites logicielles du type produit, processus ou ressource. Cette demarche utilise et renforce le paradigme defini par la methode ami. Ce processus permet, etape par etape, de suivre le deroulement d'une activite de mesurage coherente et pertinente pour l'amelioration des artefacts logiciels. Il comprend quatre etapes principales: la definition du but d'amelioration qui est raffine en sous-buts puis en questions, la specification des metriques permettant de repondre a ces questions et ainsi d'aider a la realisation du but initial, la verification de la specification de chaque metrique et la determination du type d'echelle qu'elles permettent de definir, et enfin leur validation pour verifier leur caractere predictif envers une metrique qui evalue un attribut externe de la qualite. Un lien significatif entre un ensemble de metriques evaluant des attributs internes et une metrique evaluant un attribut externe est une condition necessaire a l'amelioration des logiciels. Cela permet de modifier ou de calibrer les attributs internes d'un logiciel en cours de developpement afin d'ameliorer un aspect de sa qualite externe

Le comportement du logiciel est modelise en fonction de differentes situations: correction immediate ou differee par lot, changements de specifications. Pour chacune des situations un modele de connaissance est etabli. Ces modeles sont ensuite approches par des modeles d'action. Une methode d'evaluation de la surete de fonctionnement des logiciels est proposee

La classification de paquets consiste à vérifier par rapport à un ensemble de règles prédéfinies le contenu des entêtes de paquets. Cette vérification permet d'appliquer à chaque paquet l'action adaptée en fonction de règles qu'il valide. La classification de paquets étant un élément clé du plan de données des équipements de traitements de paquets, elle est largement utilisée dans de nombreuses applications et services réseaux, comme les pare-feu, l'équilibrage de charge, les réseaux privés virtuels, etc. Au vu de son importance, la classification de paquet a été intensivement étudiée durant les vingt dernières années. La solution classique à ce problème a été l'utilisation de matériel dédiés et conçus pour cet usage. Néanmoins, l'émergence des centres de données, des réseaux définis en logiciel nécessite une flexibilité et un passage à l'échelle que les applications classiques ne nécessitaient pas. Afin de relever ces défis des plateformes de traitement multi-cœurs sont de plus en plus utilisés. Cette thèse étudie la classification de paquets suivant trois dimensions : la conception des algorithmes, les propriétés des règles de classification et la mise en place logicielle, matérielle et son optimisation. La thèse commence, par faire une rétrospective sur les diverses algorithmes fondés sur des arbres de décision développés pour résoudre le problème de classification de paquets. Nous proposons un cadre générique permettant de classifier ces différentes approches et de les décomposer en une séquence de « méta-méthodes ». Ce cadre nous a permis de monter la relation profonde qui existe ces différentes méthodes et en combinant de façon différentes celle-ci de construire deux nouveaux algorithmes de classification : HyperSplit-op et HiCuts-op. Nous montrons que ces deux algorithmes atteignent des gains de 2~200x en terme de taille de mémoire et 10%~30% moins d'accès mémoire que les meilleurs algorithmes existant. Ce cadre générique est obtenu grâce à l'analyse de la structure des ensembles de règles utilisés pour la classification des paquets. Cette analyse a permis de constater qu'une « couverture uniforme » dans l'ensemble de règle avait un impact significatif sur la vitesse de classification ainsi que l'existence de « structures orthogonales » avait un impact important sur la taille de la mémoire. Cette analyse nous a ainsi permis de développer un modèle de consommation mémoire qui permet de découper les ensembles de règles afin d'en construire les arbres de décision. Ce découpage permet jusqu'à un facteur de 2.9 d'augmentation de la vitesse de classification avec une réduction jusqu'à 10x de la mémoire occupé. La classification par ensemble de règle simple n'est pas le seul cas de classification de paquets. La recherche d'adresse IP par préfixe le plus long fourni un autre traitement de paquet stratégique à mettre en œuvre. Une troisième partie de cette thèse c'est donc intéressé à ce problème et plus particulièrement sur l'interaction entre la charge de mise à jour et la vitesse de classification. Nous avons observé que la mise à jour des préfixes longs demande plus d'accès mémoire que celle des préfixes court dans les structures de données d'arbre de champs de bits alors que l'inverse est vrai dans la structure de données DIR-24-8. En combinant ces deux approches, nous avons propose un algorithme hybride SplitLookup, qui nécessite deux ordres de grandeurs moins d'accès mémoire quand il met à jour les préfixes courts tout en gardant des performances de recherche de préfixe proche du DIR-24-8. Tous les algorithmes étudiés, conçus et implémentés dans cette thèse ont été optimisés à partir de nouvelles structures de données pour s'exécuter sur des plateformes multi-cœurs. Ainsi nous obtenons des débits de recherche de préfixe atteignant 40 Gbps sur une plateforme TILEPro64<br>Packet classification consists of matching packet headers against a set of pre-defined rules, and performing the action(s) associated with the matched rule(s). As a key technology in the data-plane of network devices, packet classification has been widely deployed in many network applications and services, such as firewalling, load balancing, VPNs etc. Packet classification has been extensively studied in the past two decades. Traditional packet classification methods are usually based on specific hardware. With the development of data center networking, software-defined networking, and application-aware networking technology, packet classification methods based on multi/many processor platform are becoming a new research interest. In this dissertation, packet classification has been studied mainly in three aspects: algorithm design framework, rule-set features analysis and algorithm implementation and optimization. In the dissertation, we review multiple proposed algorithms and present a decision tree based algorithm design framework. The framework decomposes various existing packet classification algorithms into a combination of different types of “meta-methods”, revealing the connection between different algorithms. Based on this framework, we combine different “meta-methods” from different algorithms, and propose two new algorithms, HyperSplit-op and HiCuts-op. The experiment results show that HiCuts-op achieves 2~20x less memory size, and 10% less memory accesses than HiCuts, while HyperSplit-op achieves 2~200x less memory size, and 10%~30% less memory accesses than HyperSplit. We also explore the connections between the rule-set features and the performance of various algorithms. We find that the “coverage uniformity” of the rule-set has a significant impact on the classification speed, and the size of “orthogonal structure” rules usually determines the memory size of algorithms. Based on these two observations, we propose a memory consumption model and a quantified method for coverage uniformity. Using the two tools, we propose a new multi-decision tree algorithm, SmartSplit and an algorithm policy framework, AutoPC. Compared to EffiCuts algorithm, SmartSplit achieves around 2.9x speedup and up to 10x memory size reduction. For a given rule-set, AutoPC can automatically recommend a “right” algorithm for the rule-set. Compared to using a single algorithm on all the rulesets, AutoPC achieves in average 3.8 times faster. We also analyze the connection between prefix length and the update overhead for IP lookup algorithms. We observe that long prefixes will always result in more memory accesses using Tree Bitmap algorithm while short prefixes will always result in large update overhead in DIR-24-8. Through combining two algorithms, a hybrid algorithm, SplitLookup, is proposed to reduce the update overhead. Experimental results show that, the hybrid algorithm achieves 2 orders of magnitudes less in memory accesses when performing short prefixes updating, but its lookup speed with DIR-24-8 is close. In the dissertation, we implement and optimize multiple algorithms on the multi/many core platform. For IP lookup, we implement two typical algorithms: DIR-24-8 and Tree Bitmap, and present several optimization tricks for these two algorithms. For multi-dimensional packet classification, we have implemented HyperCuts/HiCuts and the variants of these two algorithms, such as Adaptive Binary Cuttings, EffiCuts, HiCuts-op and HyperSplit-op. The SplitLookup algorithm has achieved up to 40Gbps throughput on TILEPro64 many-core processor. The HiCuts-op and HyperSplit-op have achieved up to 10 to 20Gbps throughput on a single core of Intel processors. In general, our study reveals the connections between the algorithmic tricks and rule-set features. Results in this dissertation provide insight for new algorithm design and the guidelines for efficient algorithm implementation

Cette thèse propose une nouvelle méthode de structuration des règles ergonomiques permettant l'évaluation des interfaces graphiques. Cette méthode réalisée dans le cadre d'un contrat d'étude passé entre le SRTP (Service de Recherche Technique de la Poste) et le laboratoire LIS a été définie en vue d'être utilisée par des informaticiens et d'être intégrée dans un outil d'évaluation automatique de la présentation statique des interfaces. Pour fournir des résultats directement utilisables lors de la modification de l'interface et pour pouvoir implémenter la méthode dans un outil d'évaluation automatique, les règles ergonomiques ont été reformulées pour qu'elles s'appliquent directement aux objets de présentation, les connaissances nécessaires à l'évaluation ont été structurées de la manière suivante : * l'interface est décomposée suivant les objets de présentation qui la constituent, * une structure intermédiaire entre les objets de présentation et les règles ergonomiques a été défini. Cette structure, appelée typologie, correspond à une hiérarchie de classes qui regroupe les objets graphiques concernés par les mêmes règles ergonomiques. À la place de porter sur les objets graphiques, ces règles sont rattachées aux classes de la typologie. Une maquette de l'outil ERGOVAL, sous la forme d'un système expert, a été réalisée pour valider cette structuration des connaissances et pour définir les spécifications de l'outil final. De manière à pouvoir déterminer le champ d'application de l'outil, nous avons étudié la dimension automatique de l'outil d'évaluation, notamment la récupération automatique de la description de l'interface, et la dimension qualitative de l'évaluation représentée par le nombre et le niveau des règles ergonomiques intégrées dans l'outil. Nous avons ainsi défini la qualité d'une évaluation qui serait réalisée de manière totalement automatique et la qualité d'une évaluation qui intégrerait des règles ergonomiques de plus haut niveau et notamment des règles ergonomiques liées à la tâche<br>The thesis introduces a new method for structuring ergonomic rules in order to evaluate graphical user interface. This method performed in collaboration with the SRTP (post office technical research unit) aims to be used by computer experts and to be integrated in an automatic user interface evaluation tool : ERGOVAL. In order to provide information to developers in a way they can handle it to modify the interface, ergonomic rules were reformulated to concern directly graphical objects of the user interface. Knowledge involved in the evaluation was structured in this way : * a representation of the UI in terms of the interaction objects of the norm CUA was built : this is the decomposition of graphical objects * all graphical objects concerned by the same set of ergonomic rules are grouped together into classes of objects : the typology of graphic objects. . The resulting typology consists in several levels of abstraction, the graphical objects being the leaves of this typology. The links of this typology are types of links which have hierarchical properties, i. E. Each type inherits attributes from the parent type and associated rules. A mock-up of the ERGOVAL tool was made to validate knowledge structuration and to define specifications of the final tool. In order to determine the scale application, the automatic and qualitative dimensions were studied especially the automatic retrieval of interface description and the number and level of ergonomic rules integrated in the mock-up. Consequently, the quality of an automatic evaluation and an evaluation of high level ergonomic rules were determined

Les travaux presentes dans ce memoire concernent l'utilisation du test statistique en tant que technique de verification pour les logiciels critiques, c'est-a-dire presentant des contraintes de surete elevee. Le test statistique consiste a executer un programme avec des entrees aleatoires, le profil de test et le nombre d'entrees a generer etant determines a partir de criteres bases sur l'analyse structurelle ou fonctionnelle de ce programme: ce mode de generation probabiliste permet de compenser l'imperfection des criteres actuels vis-a-vis des fautes recherchees, imperfection qui les rend d'autant plus insuffisants dans le cas de logiciels critiques. Le potentiel de l'approche proposee est justifie par une etude theorique sur les causes d'echec d'un test; sa faisabilite et son efficacite sont illustrees experimentalement sur un programme issu du domaine nucleaire. Pour le test unitaire, on montre l'efficacite d'une approche combinant le test statistique structurel avec un test deterministe des valeurs aux limites. Pour le test de composants logiciels complexes, la conception du test statistique s'effectue a partir d'une specification modulaire comprenant des modeles comportementaux. Des modeles classiques sont d'abord envisages (machines a etats finis et tables de decision); puis l'approche est affinee en considerant une specification basee sur des modeles plus sophistiques: les statecharts

Les applications temps reel a contraintes strictes sont des applications multitaches ou les contraintes temporelles (delais d'execution) doivent etre strictement satisfaites. La methodologie developpee permet la validation de ce type d'applications. L'environnement de conception integre la prise en compte des requetes periodiques et aperiodiques et des schemas de programmes exprimant des cooperations fixes ou variables entre les taches. Apres transformation de ce modele comportemental de l'application en un ensemble de taches sous forme normale associees a un graphe de precedence, la validation est basee sur une analyse d'ordonnancabilite. Cette validation est effectuee sur les comportements realistes de l'application et permet d'evaluer les performances temporelles de l'application. Une optimisation des caracteristiques temporelles est alors possible afin d'ameliorer ses performances

Le domaine du génie logiciel évolue rapidement, exposant les développeurs à collection d'outils, langages, framework et paradigmes en constante croissance.De plus, chacun de ces composant peut avoir sa propre configuration interne.Ainsi, concevoir un nouveau logiciel consiste à sélectionner des composants de cette collection, un processus similaire à la création d'une configuration.Le critère pour configurer de tels systèmes est trop souvent la facilité de développement, ce qui cause des obésiciels sur-dimensionnés et consommateur en énergie.Ce paradigme n'est pas aligné avec les considérations frugales et environnementales.Cette dissertation s'intéresse donc à la possibilité d'utiliser la configuration des logiciels pour optimiser leur performance.Une attention spécifique est portée à la consommation énergétique et la taille de ces logiciels.Un prérequis pour optimiser un système est de comprendre sa performance actuelle.Pour mieux comprendre ce sujet, le logiciel configurable JHipster a été analysé de façon empirique.L'analyse exhaustive de la performance de ses configuration, au travers de différents indicateurs, a montré à quel point la configuration impactent ses performances.Cette compréhension de la performance a permit de créer de configuration de JHipster à haute performance.Ces configuration à haute performance a été créees manuellement, ce qui n'est possible qu'avec un petit espace des configurations.Un algorithme a donc été créé pour automatiser ce processus, et ainsi l'adapter aux plus grands espaces de configuration.Cependant, optimiser une configuration en sélectionnant des options à haute performance n'est pas suffisant, car les options interagissent entre elles:par exemple, dans certaines situation, deux options à haute performance peuvent sous-performer quand elles sont assemblées.L'algorithme d'optimisation a donc été adapté pour tirer profit de ces comportements.L'application de cet algorithme a un large ensemble de configurations a montré que la plupart d'entre elles atteignent une performance presque optimale, avec seulement un nombre limité de modification.Cependant, les contraintes de performance ne se limitent pas à un seul indicateur.La consommation énergétique d'un logiciel n'est pas toujours l'indicateur le plus impactant à optimiser.L'algorithme d'optimisation a donc dû être généralisé pour supporter l'optimisation de plusieurs indicateurs simultanément.Cet algorithme généralisé a été validé sur un couple d'indicateurs de performance: le temps d'exécution et la taille d'un logiciel.Cette validation a montré que la moitié des configurations peut atteindre leur optimum local respectif en modifiant une seule option.De plus, en appliquant cet algorithme à l'exhaustivité d'un espace de configuration, il a été possible de suivre comment il navigue l'espace de configuration à la recherche de configurations optimales, ce qui a mit en lumière certaines limites de l'algorithme, qui peut donc être encore amélioré dans de futures travaux.Dans son état actuel, l'algorithme a été publié sous la forme d'un outil open-source sous le nom d'ICO<br>The field of software engineering evolves rapidly, exposing practitioners to an ever-increasing collection of tools, languages, frameworks, and paradigms.Each of these components can have its own, internal configuration.Thus, designing a new software system consist in selecting components from this collection, which is akin to creating a configuration.The criterion to configure such systems is too often the ease of development, which leads to oversized, power-hungry bloatware.This paradigm is not aligned with frugal or environmental concerns.Thus, this dissertation looks into the ability to leverage the configuration of a system to optimize its performance.A specific focus is made on energy consumption and the size of software systems.A prerequisite to optimizing a system is to understand its current performance.To gain insight into this subject, the configuration software JHipster was empirically analyzed.Exhaustively assessing the performances of configurations of JHipster, wrt several indicators, showed that different configurations have indeed different performances.Thus, relying on performance insight, it is possible to create high-performance configurations of JHipster.Furthermore, some performance indicators proved correlated across configurations.Therefore, the optimization goal can be simplified by ignoring redundant performance indicators.The process of creating optimized configurations of JHipster was performed manually, which is only possible in smaller configuration spaces.To tackle larger configuration spaces, an algorithm was created, defining how to assess the performance of each option, and then how to improve a given configuration using such performance data.However, optimizing a configuration by selecting high-performance options brought out limitations, as options can interact with each other:in some situations, pairing high-performance options may result in subpar performances.Similarly, low-performance options can prove unexpectedly efficient when paired together.Thus, the optimization algorithm has been designed to leverage such specific behaviors.Applying this algorithm to a large set of configurations showed that most of them can reach near-optimal performances, with only a limited set of modifications.However, performance constraints are not limited to a single performance indicator.Depending on the context, the energy consumption of a system may not be the single most impactful indicator to optimize.Thus, the optimization algorithm must be generalized to support several performance indicators.This generalized algorithm has been validated on a pair of performance indicators: the execution time and the size of the software.The main highlight of this validation is that half of all configurations can reach a local optimum by changing a single setting.Furthermore, by exhaustively applying the algorithm to the configuration space of a system, it was possible to follow how it navigates the configuration space to find optimal configurations.Analyzing this navigation highlighted current limitations in the algorithm, which can thus be further improved as future work.In its current state, the algorithm was published as an open-source tool under the name ICO

To cope with the complexity of large object-oriented software systems, developers organize classes into subsystems using the concepts of module or package. Such modular structure helps software systems to evolve when facing new requirements. The organization of classes into packages and/or subsystems represents the software modularization. the software modularization usually follows interrelationships between classes. Ideally, packages should to be loosely coupled and cohesive to a certain extent. However, Studies show that as software evolves to meet requirements and environment changes, the software modularization gradually drifts and looses quality. As a consequence, the software modularization must be maintained. It is thus important to understand, to assess and to optimize the organization of packages and their relationships. Our claim is that the maintenance of large and complex software modularizations needs approaches that help in: (1) understanding package shapes and relationships; (2) assessing the quality of a modularization, as well as the quality of a single package within a given modularization; (3) optimizing the quality of an existing modulariza- tion. In this thesis, we concentrate on three research fields: software visualizations, metrics and algorithms. At first, we define two visualizations that help maintainers: (1) to understand packages structure, usage and relationships; (2) to spot patterns; and (3) to identify misplaced classes and structural anomalies. In addition to visual- izations, we define a suite of metrics that help in assessing the package design quality (i.e., package cohesion and coupling). We also define metrics that assess the quality of a collection of inter-dependent packages from different view points, such as the degree of package coupling and cycles. Finally, we define a search-based algorithm that automatically reduces package coupling and cycles only by moving classes over existing packages. Our optimization approach takes explicitly into account the origi- nal class organization and package structure. It also allows maintainers to control the optimization process by specifying: (1) the maximal number of classes that may change their packages; (2) the classes that are candidate for moving and the classes that should not; (3) the packages that are candidate for restructuring and the packages that should not; and (4) the maximal number of classes that a given package can entail. The approaches presented in this thesis have been applied to real large object- oriented software systems. The results we obtained demonstrate the usefulness of our visualizations and metrics; and the effectiveness of our optimization algorithm.

Il est généralement admis que les modules réalisant plusieurs fonctions comportent des erreurs structurelles. De tels modules dits de cohésion non fonctionnelle, peuvent être détectés par des métriques fondées sur un nouveau modèle. Ce modèle peut de plus apporter une aide à la décomposition des modules d'un logiciel, et il prévoit les conséquences minimales sur les flux d'information du logiciel, de cette décomposition

Aujourd'hui, les systemes informatiques sont de plus en plus distribues, reactifs et temps reel, rendant leur developpement extremement complexe. La difficulte de developpement de ces systemes rend necessaire l'utilisation de methodes et outils permettant de gerer la complexite et de conduire des specifications non ambigues des comportements desires. Les environnements formels, bases par des outils de developpement ameliorent la qualite de ces systemes. Nous presentons un environnement original de specification de logiciels. Cet environnement est base sur le formalisme z et sur l'integration entre les methodes graphiques orientees objet et les techniques de specification formelle. L'environnement permet d'une part la prise en compte et la verification des proprietes fonctionnelles et non-fonctionnelles du systeme. Nous utilisons dans notre demarche une representation explicite du temps et permet une representation de la dynamique du systeme. D'autre part, cet environnement est base par un outil permettant le developpement et l'analyse de modeles graphiques et formels de la structure et du comportement des systemes etudies

Pour faire face à la complexité des grands systèmes logiciels orientés objets, les programmeurs organisent les classes en sous-systèmes en utilisant les concepts de module ou de package. Une telle structure modulaire permet aux systèmes logiciels d’évoluer face aux nouvelles exigences. L’organisation des classes dans des packages et / ou sous-systèmes, que nous appelons la modularisation du logiciel, suit habituellement les relations entre les classes. Il est d'usage de vouloir les packages faiblement couplés et assez cohésifs. Cependant, les études montrent que quand les systèmes logiciels s’adaptent aux exigences et aux modifications de l’environnement, leurs modularisations dérivent et perdent progressivement leur qualité. En conséquence, la modularisation des systèmes logiciels doit être maintenue. Il est donc important de comprendre, d’évaluer et d’optimiser l’organisation des packages et de leurs relations. Le point défendu dans la thèse est que le maintien des modularisations logiciels de grande taille et complexes requiert des approches qui contribuent à: (1) la compréhension des packages et de leurs relations; (2) l’évaluation de la qualité d’une modularisation, ainsi que la qualité d’un package dans le contexte d’une modularisation donnée; (3) l’optimisation de la qualité d’une modularisation existante. Dans cette thèse, nous nous concentrons sur trois domaines de recherche: visualisations de programmes, métriques et algorithmes. Dans un premier temps, nous définissons deux visualisations qui aident les mainteneurs à: (1) la compréhension de la structure des packages, et de leurs utilisations et leurs relations; (2) l’identification des modèles; et (3) l’identification des anomalies structurelles. En plus de visualisations, nous définissons un ensemble de métriques qui aident à évaluer la qualité d’un package (i.e., la cohésion et le couplage). Nous définissons également des métriques qui permettent d’évaluer la qualité d’une collection des packages inter-dépendants. Ceci en prenant en compte le degré de couplage et de cycles entre les packages. Enfin, nous définissons un algorithme de recherche qui réduit automatiquement le couplage et les cycles entre les packages, en déplaçant seulement les classes sur les packages existants. Notre approche d’optimisation prend explicitement en compte l’organisation des classes et la structure originale des packages. Il permet également aux mainteneurs de contrôler le processus d’optimisation en spécifiant: (1) le nombre maximal des classes qui peuvent changer leurs packages; (2) les classes qui sont candidates pour se déplacer et celles qui ne doivent pas changer leurs packages; (3) les packages qui sont candidates pour la restructuration et ceux qui ne doivent pas se changer; et (4) le nombre maximal des classes qu’un package donné peut contenir. Les approches présentées dans cette thèse ont été appliquées à des systèmes logiciels orienté objets, réels et de grand taille. Les résultats obtenus démontrent l’utilité de nos visualisations et métriques, et l’efficacité de notre algorithme d’optimisation<br>To cope with the complexity of large object-oriented software systems, developers organize classes into subsystems using the concepts of module or package. Such modular structure helps software systems to evolve when facing new requirements.The organization of classes into packages and/or subsystems represents the software modularization. the software modularization usually follows interrelationships between classes. Ideally, packages should to be loosely coupled and cohesive to a certain extent. However, Studies show that as software evolves to meet requirements and environment changes, the software modularization gradually drifts and looses quality. As a consequence, the software modularization must be maintained. It is thus important to understand, to assess and to optimize the organization of packages and their relationships. Our claim is that the maintenance of large and complex software modularizations needs approaches that help in: (1) understanding package shapes and relationships; (2) assessing the quality of a modularization, as well as the quality of a single package within a given modularization; (3) optimizing the quality of an existing modularization. In this thesis, we concentrate on three research fields: software visualizations, metrics and algorithms. At first, we define two visualizations that help maintainers: (1) to understand packages structure, usage and relationships; (2) to spot patterns; and (3) to identify misplaced classes and structural anomalies. In addition to visualizations, we define a suite of metrics that help in assessing the package design quality (i.e., package cohesion and coupling). We also define metrics that assess the quality of a collection of inter-dependent packages from different view points, such as the degree of package coupling and cycles. Finally, we define a search-based algorithm that automatically reduces package coupling and cycles only by moving classes over existing packages. Our optimization approach takes explicitly into account the original class organization and package structure. It also allows maintainers to control the optimization process by specifying: (1) the maximal number of classes that may change their packages; (2) the classes that are candidate for moving and the classes that should not; (3) the packages that are candidate for restructuring and the packages that should not; and (4) the maximal number of classes that a given package can entail.The approaches presented in this thesis have been applied to real large object-oriented software systems. The results we obtained demonstrate the usefulness of our visualizations and metrics; and the effectiveness of our optimization algorithm

Cette thèse présente une métrique de complexité des logiciels adaptée aux programmes écrits dans un langage de type flots de données. Dans un premier temps, on décrit l'environnement qui a servi de base à cette étude: il s'agit de l'atelier logiciel saga (spécification d'applications et génération automatisée) mis au point par l'entreprise Merlin Gerin, dans lequel les programmes produits sont de type flots de données synchrone, et sont construits grâce a un outil graphique. On décrit ensuite la métrique proposée: celle-ci vise a mesurer la complexité graphique des logiciels considérés. Une campagne de mesures a été conduite sur des applications réelles en cours de développement à Merlin Gerin (département systèmes et électronique de sûreté) pour étudier le comportement empirique de cette métrique. On observe les résultats obtenus conjointement avec d'autres métriques de complexité plus sobres

Les techniques de modelisation constituent un bon moyen d'evaluer les performances de systemes informatiques au cours du developpement. Leur utilisation pose cependant deux types de problemes: le premier est lie a la nature approximative de la modelisation, le deuxieme a l'integration de l'evaluation de performances dans le cycle de vie d'un systeme. La methode que nous avons definie propose d'une part, une nouvelle approche de la modelisation qui met bien en evidence l'importance de la communication entre l'equipe de conception du systeme et les specialistes en modelisation, et d'autre part, la mise en place de mecanismes d'integration entre les phases de developpement d'un systeme et l'evaluation de ses performances. Ces mecanismes ont ete appliques a un environnement de developpement integrant hood comme methode de conception. Ils permettent l'integration a differents niveaux: - lors de la specification, grace a une taxonomie des contraintes de performances qui fournit des regles de redaction de ces contraintes. - lors de la conception, grace a des techniques d'annotations de la methode de conception qui facilitent la capture des donnees relatives aux performances. - lors de la modelisation, grace a des techniques de generation automatique de modeles de performances a partir d'une conception annotee. La methode a ete experimentee sur un projet pilote du domaine spatial et a demontre tout son interet. Elle a permis d'ameliorer le dialogue entre les concepteurs et les specialistes en modelisation en maintenant la consistance entre le systeme et son modele. Elle a egalement reduit les temps de developpement du modele, permettant ainsi l'analyse de plusieurs configurations du systeme

La complexité grandissante des architectures modernes, rend de plus en plus difficile la tâche des programmeurs à comprendre le comportement des programmes s’exécutant sur ces machines. De plus, les compilateurs actuels génèrent des codes difficiles à comprendre, dû à l’application d’optimisations plus agressives. Cette complexité croissante, tant au niveau des architectures qu’au niveau des compilateurs, renforce le besoin d’une analyse de performance pour aider le programmeur. Différents outils et techniques existent mais aucun outil n’est suffisant, seul, pour résoudre tous les problèmes. Cette thèse propose deux outils, différents et complémentaires, pour l’évaluation de performances, de code binaire. Le premier outil, l’analyse statique de Maqao, effectue une évaluation statique des performances du code, et donne une estimation pour la qualité du code, par exemple, les ratios de vectorisation. Le second outil, Decan, est une nouvelle approche d’analyse de performances qui cible les instructions d’accès mémoire. L’objectif de Decan est de détecter le groupe d’instructions responsable des faibles performances. Les deux outils ont été combinés pour proposer une méthodologie semi-automatique pour l’évaluation de performances<br>Current hardware tends to increase pressure on programmers to optimize the codes. The complexity of modern architectures makes it more difficult to understand the behavior of the programs running on them. Moreover, the compilers apply aggressive optimizations which makes the compiled code more difficult to understand. This increasing complexity shows that there is still a need of performance analysis to help the programmers. Different tools and techniques exist, but no single tool is a panacea; instead, different tools have different strengths. This thesis proposes two different and complementary tools for performance analysis on binary code. The first tool, Maqao’s static analysis, performs a static evaluation of the performance of the code, and gives an estimate of the quality of the code, such as the vectorization ratios. The second tool, Decan, is a new approach of performance analysis that targets the memory instructions to pinpoint the set of instructions responsible of the poor performance. Both tools are combined to propose a semi-automated methodology for performance evaluation

Cette thèse étudie les techniques de vérification automatiques de propriétés d'accessibilité pour des programmes représentées symboliquement par des automates. Les ensembles de configurations des programmes sont représentés par des automates tandis que les instructions sont représentées par des transducteurs. Calculer l'ensemble des états accessibles est à la base de la vérification de propriétés de sûreté. C'est un problème indécidable, le calcul itératif naïf ne termine pas en général. Il faut alors utiliser des techniques permettant d'accélérer ce calcul. Une des techniques principalement étudiée consiste à sur-approximer les ensembles accessibles afin de forcer la convergence du calcul. Ces sur-approximations peuvent induire des comportements n'existant pas dans le programme réel pour lesquelles la propriété à vérifier serait fausse. Dans ce cas, nous testons, si les contre-exemples appartiennent au programme réel, et dans le cas où ces contre-exemples ne seraient dus qu'à la sur-approximation, nous automatisons des raffinements des abstractions. Partant de cette méthodologie, nous proposons des techniques afin de vérifier les programmes séquentiel, sans récursion, mais manipulant des listes chaînées. Nous développons alors des techniques permettant dans un premier temps d'exprimer les configurations mémoires de tels programmes sous forme d'automates, et les instructions sous formes de transducteurs. Nous développons ensuite des des techniques de sur-approximation adaptées à ce type particulier d'automates. Nous montrons ensuite que de tels programmes peuvent être vus comme des automates à compteurs, i. E. , que seuls quelques points des tas mémoires (qui sont en nombre finis) sont relevant et que des compteurs indiquant le nombre d'éléments entre ces points permettent de donner une représentation du comportement du programme. Nous développons ensuite des techniques de vérification d'automates à compteurs, en utilisant des techniques d'abstraction-vérificaiton-raffinement pour ce type d'automates. Nous avons développé un outil permettant la vérification de tels programmes. Dans un second temps, nous étudions le problème de la taille des contre-exemples sur des automates de Bùchi représentant le produitentre une formule de logique temporelle linéaire et un automate fini. Les contre-exemples permettent la correction des programmes, et il est important de pouvoir travailler sur des contre-exemples les plus petits possibles. De tels algorithmes nécessitent de d'optimiser l'espace mémoire utilisé pour le stockage des éléments tout en essayant de garder une complexité en temps acceptable<br>This thesis studies automatic verification techniques where programs are represented symbolically by automata. The set of configurations of such programs are represented by automata whereas instructions are represented by transducers. Computing the set of reachable states of such programs is an important ingredient for the verification of safety properties. This problem is undecidable, since the naive iterative computation does not terminate in general. Therefore, one has to use techniques to accelerate the computation. One of the techniques mainly studied consists to over-approximate the set of reachable states to enforce the convergence of the computation. These over-approximation techniques can introduce behaviours that do not exist in the program and for which the property i false. In that case, we check if the counterexamples is present in real program or due to the upper approximation. In the latter case, we use refinement techniques in order to eliminate the spurious counterexample from our abstraction and restart the computation. Using this abstract-check-refine loop, we propose techniques in order to verify sequential, non-recursive programs manipulating linked lists. We develop methods allowing to represent memory configurations as automata, and instructions as transducers. We then propose specific abstraction and refinement techniques for such representations. Then, we show that this kind of programs can also be represented like counter automata, i. E. , only few special cells of the heap (and their number is finite) are relevant and counters indicating the number of elements between this points allows to represent the heap of the program. We develop then methods for counter automata verification using the abstract-check-refine loop for this special kind of automata. We have tested our methods with a tool that supports the automaton described previously. In an other part of the thesis, we study the size of the counterexamples for Buchi automaton that represent the product between a linear temporal logic formula and a finite automaton. These counterexamples allow to correct the program and it is important to have as small as possible counterexamples to improve the time needed for the correction. Using SPIN's memory representation for a state, such algorithms have to optimize memory usage while keeping time complexity as small as possible

Cette thèse porte sur la vérification des programmes concurrents, en nous intéressant en particulier à l'étude la décidabilité et la complexité des problèmes d'accessibilité. Dans la plus grande partie de cette thèse, nous considérons des programmes concurrents où les processus séquentiels correspondent à des threads pouvant faire des appels de procédures (potentiellement récursives). La difficulté vient de l'interaction entre la récursivité et de la concurrence qui rend le problème de l'accessibilité indécidable en général. Nous étudions alors les conditions sous lesquelles ce problème devient décidable. Ces conditions peuvent être vues comme des contraintes à poser sur l'ordonnancement des actions le long des exécutions du programme analysé. Ainsi, les résultats de décidabilité peuvent être utilisés pour définir des procédures d'analyse sous-approchée permettant de détecter de manière efficace des comportements illicites des programmes. Dans un second temps, nous nous intéressons aux programmes s'exécutant selon un modèle faible de la mémoire partagée (weak memory model). Dans de tels programmes, l'ordre entre les actions d'un même processus est relâché pour des besoins de performance en permettant la permutation entre certains types d'actions. Cela rend alors le conception des programmes concurrents encore plus difficile du fait que la sémantique de la concurrence devient hautement complexe et contre-intuitive. Nos travaux montrent qu'en effet selon le type des relaxations d'ordre entre actions, le problème de l'accessibilité peut être décidable mais hautement complexe dans certains cas, et il peut même être indécidable dans d'autres<br>This thesis addresses the verification problems in both, concurrent and recursive Systems as well as concurrent Systems with store buffers. We establish the required theoretical basis for automated analyses: decidability and complexity results for reachability problems. In a first time, we are interested in verifying concurrent programs where each process corresponds to a sequential program with (recursive) procedure calls. The difficulty in analyzing such programs cornes from the interaction between recursion and concurrency which makes the reachability problems undecidable in general. However, in practice programs obey additional constraints that can be exploited to turn the reachability problem decidable. Their study is subject of this thesis. These conditions may be seen as constraints to impose on the order between the actions of the analyzed programs. Moreover, these decidability results can be used to perform an under-approximation analysis to effectively detect bad behaviors of the analyzed programs. In a second time, we study concurrent programs running under weak memory models. In such kind of programs, the order between actions of the same process is relaxed (for performance reasons) by allowing the permutation between certain types of memory operations. This makes reasoning about the behaviors of concurrent programs much more difficult. Moreover, it is not clear how to apply standard reasoning techniques. Our works show that indeed according to the type of relaxation, the reachability problem becomes décidable (but with a highly complexity) in other cases, it even turns out undecidability

Cette these propose un modele de caracterisation de l'activite des programmes. Tout programme est decrit selon l'ensemble des calculs qu'il effectue, ceux-ci etant classes en six categories admettant plusieurs variations. Actuellement, ce modele s'applique aux programmes integrant une seule boucle. La caracterisation d'un programme au travers du modele, ou schema, constitue l'explication globale de ce programme, celle-ci revelant sa structure algorithmique et permettant de le rattacher a un ensemble de stereotypes que les programmeurs experimentes connaissent bien. Le schema est egalement la specification abstraite d'un probleme a implementer, celle-ci etant alors representee sous une forme particulierement concise. La description conceptuelle est l'equivalent du programme resume par un schema dont elle est l'explication ou la specification complete. Sur la base des descriptions conceptuelles, trois systemes ont ete implementes: 1. Prisme calcule le schema et la description conceptuelle d'un programme ; il fournit donc une explication de ce programme qui aide a sa comprehension, 2. Signedit genere un programme a partir d'une description conceptuelle ; de ce fait, il introduit un style de programmation qui minimise les interventions du programmeur, 3. Acl est un langage de programmation qui propose d'utiliser les schemas comme primitives ; il integre ainsi des constructions de haut niveau d'abstraction qui favorisent le paradigme de la programmation conceptuelle. Ces systemes ont permis la validation du modele. En effet, pour environ cent cinquante programmes, le programme genere par signedit a partir de la description conceptuelle calculee par prisme est equivalent, en terme de calculs effectues, au programme original. Actuellement, ils sont intensivement utilises pour effectuer les experimentations necessaires a l'extension du modele, notamment vers un modele conceptualisant des programmes comportant plusieurs boucles.

Les travaux de cette thèse s'inscrivent dans une collaboration avec l'entreprise Berger-Levrault, acteur majeur du développement de logiciels de gestion administrative pour les services publics. Ces travaux s'appuient sur deux constats. D'une part, la politique de numérisation des services publics induit la nécessité de disposer de logiciels adaptés aux métiers de l'ensemble des établissements publics. Ces logiciels sont complexes et particulièrement riches comparativement aux logiciels de bureautique classiquement utilisés. D'autre part, on observe que les dispositifs utilisés pour interagir avec ces logiciels n'évoluent que très peu. Depuis plusieurs décennies, la souris et le clavier restent la norme dans un environnement fixe. Or, ces dispositifs ne possèdent que peu de degrés de libertés en entrée. La manipulation de données multidimensionnelles avec ceux-ci induit un plus grand nombre d'étapes pour réaliser une tâche, rallongeant ainsi le chemin d'interaction. Dans ce contexte, l'objectif de ces travaux de thèse est de contribuer à la fluidification de l'interaction avec des données multidimensionnelles, contenues dans les logiciels du service public, au travers de l'augmentation des degrés de libertés en entrée proposés par les dispositifs. En effet, une plus grande quantité de degrés de libertés en entrée réduirait le nombre d'étapes nécessaires à la réalisation d'une tâche donnée, fluidifiant ainsi l'interaction. Nous proposons 3 contributions majeures : un dispositif à multiples degrés de libertés, la Roly-Poly Mouse ; un espace de conception, DECO ; ainsi qu'un ensemble de techniques d'interaction avec dispositifs mobiles basées sur le principe du stacking. Une première contribution de nos travaux consiste en la conception d'un nouveau dispositif à multiples degrés de liberté : la Roly-Poly Mouse (RPM). Ce dispositif, dont la base est arrondie, vise à remplacer la souris traditionnelle. Il possède 6 degrés de libertés (3 translations dont 2 exploitées et 3 rotations). Nous avons évalué ses performances et l'avons comparé à d'autres dispositifs pour une tâche nécessitant 6 degrés de libertés (manipulation d'objet 3D). Une seconde contribution de nos travaux consiste en la définition d'un espace de conception se focalisant sur l'aspect physique de la composition de dispositifs : DECO. DECO s'appuie sur deux axes : l'arrangement physique et la manipulation physique. À partir de cet espace de conception, nous avons conçu un dispositif composé : la Roly-Poly Mouse 2, un dispositif composé d'une Roly-Poly Mouse et d'une souris traditionnelle. Nous avons évalué ses performances et l'avons comparé à d'autres dispositifs au travers d'une tâche de RST (Rotate-Scale-Translate, tâche 5D). [...]<br>The work of this thesis is part of a collaboration with the company Berger-Levrault, a major actor in the development of administrative management software for public services. This work is based on two observations. On the first hand, the policy of digitization of public services induces the need for software adapted to the professions of all public institutions. These software are complex and particularly rich compared to classically used office software (Office, mailbox, etc.). On the other hand, we observe that the devices used to interact with these software did not evolve. Since several decades, the mouse and the keyboard remain the norm in a fixed environment. However, these devices have only few input degrees of freedom. The manipulation of multidimensional data with these devices induces a greater number of steps to perform a task, thus lengthening the interaction path. In this context, the objective of these thesis work is to improve the interaction flow with multidimensional data contained in the software of the public service through the increase of the input degrees of freedom proposed by the devices. Indeed, a larger amount of input degrees of freedom would reduce the number of steps necessary to the accomplishment of a given task, thus improving the interaction flow. We propose three major contributions: a device with multiple degrees of freedom, the Roly-Poly Mouse; a design space, DECO; as well as a set of interaction techniques with mobile devices based on the principle of stacking. A first contribution of our work is the design of a new device with multiple degrees of freedom: the Roly-Poly Mouse (RPM). This device, whose base is rounded, aims to replace the traditional mouse. It has 6 degrees of freedom (3 translations of which 2 exploited and 3 rotations). We evaluated its performance and compared it to other devices for a task requiring 6 degrees of freedom (3D object manipulation). A second contribution of our work is the definition of a design space focusing on the physical aspect of the composition of devices: DECO. DECO relies on two axes: physical arrangement and physical manipulation. From this design space, we designed a compound device: the Roly-Poly Mouse 2, a device consisting of the combination of a Roly-Poly Mouse and a traditional mouse. We evaluated its performance and compared it to other devices through a RST task (Rotate-Scale-Translate, 5D task). [...]

Le travail réalisé est relatif au développement et à l'utilisation de modèles élémentaires de raisonnement sur l'élimination de déchets industriels, en vue de disposer-d'un outil d'aide à la décision. La démarche suivie est décomposée en trois étapes : • La première étape consiste à identifier, interpréter et enchaîner les principales informations concernant les filières d'élimination de déchets (filières thermique, biologique, physico-chimique et enfouissement technique), ainsi que leurs interactions. Elle consiste en l'acquisition des connaissances nécessaires sur les différents traitements pour constituer des modèles de raisonnement. • La deuxième étape est consacrée à la formalisation des connaissances sous la forme de règles de production et à leur automatisation. Cette procédure est à l'origine de DECHAIDE, Système à Base de Connaissances (SBC) qui permet, à partir d'un nombre restreint de paramètres d'un déchet, d'orienter celui-ci vers les filières d'élimination techniquement les plus adaptées. • Enfin, dans la dernière étape, DECHAIDE est évalué à la fois sur le plan technique, pragmatique et subjectif. Cette évaluation a permis de dégager la cohérence, l'influence sur la performance de l'utilisateur et certaines faiblesses de ce système. L'analyse du comportement de DECHAIDE face à des situations réelles d'élimination de déchets a permis de valider et démontrer l'utilité pédagogique et technique des SBC dans un domaine multidisciplinaire comme celui de la gestion de déchets<br>The present work deals with the development and utilisation of elementary industrial waste treatment models, in order to provide a decision support system. The approach consists in three main steps : First the major informations concerning waste treatment strategies (Thermal biological, physical, chemical and land-filling), and their interactions, were identified, interpreted and chained up. This first step consist in the collection of the knowledge required to model the global approach. Second, the knowledge was formalised into « production rules » and these were automated. From this procedure originated DECHAIDE (WAST'AID), a Knowledge Based System (KBS) which allows the user to orientate a waste, by referring to a limited number of parameters, throught the most technically adjusted strategies. Finally, DECHAIDE was evaluated on a technical, pragmatical and subjective basis. This assessment drew our attention on the consistency of this system and some of its weaknesses, as well as the influence on the user's performance. DECHAIDE's responses to real waste treatment scenarios was analysed. Educational and technical utility of KBS in a multidisciplinary field such as waste management was demonstrated and validated

Le travail de cette thèse porte sur l'élaboration d'un référentiel pour le développement d'un système de pilotage de la performance cohérent et réactif, interface entre plusieurs méthodes distinctes et complémentaires. Le référentiel proposé intègre des principes clés de pilotage par la performance et propose une alternative améliorée et prometteuse par rapport aux systèmes de mesures de la performance traditionnels. Un système de pilotage de la performance est un outil indispensable pour une organisation. Sa conception demeure par ailleurs une démarche complexe étant donné les différents aspects et éléments que l'organisation doit intégrer dans son processus d'évaluation et d'amélioration de la performance, en particulier les événements perturbateurs, souvent négligés dans la littérature et très difficile à intégrer dans l'élaboration d'un mécanisme de pilotage de la performance. En effet, le choix de la variable de décision pour contrecarrer les effets d'un évènement perturbateur n'est pas toujours immédiate, il possède une certaine inertie qui peut entraîner une perte de la performance globale. Également, les décideurs ne disposent pas souvent des mécanismes et des outils susceptibles de vérifier que les composantes clés de pilotage de la performance (Objectifs-Variables de décision-Indicateurs de performance) engagées par chacun d'eux soient cohérentes et aident à faire évoluer l'organisation vers l'atteinte de ses objectifs escomptés. De ce fait, l'organisation évolue dans un contexte souvent incertain et doivent faire preuve d'adaptabilité pour garantir leur viabilité. Ce projet de recherche est motivé par un besoin criant soulevé suite à une revue de littérature soulignant la nécessité de développer un système de pilotage de la performance qui répond aux défis actuels en terme de pilotage, à savoir : la cohérence entre les composantes clés de pilotage de la performance et la réactivité pour faire face aux évènements perturbateurs. De ce fait, notre volonté dans ce travail a été de proposer un référentiel pour le développement d'un système de pilotage de la performance cohérent et réactif. Les contributions de cette thèse sont présentées en quatre phases. Dans une première phase, à partir du constat réalisé durant la revue de littérature, nous avons souligné la nécessité de proposer une démarche structurale SIPCo (Système d'Indicateurs de Performance Cohérent) pour identifier les composantes clés de pilotage de la performance et assurer leur cohérence à travers deux démarches. Une démarche logique basée sur (1) une approche de modélisation de système décisionnel afin d'identifier les centres de décision et (2) une approche de modélisation de système informationnel afin de d'établir une représentation de la part interactive des composantes clés de pilotage de la performance de chaque centre de décision. La méthode SIPCo repose aussi sur une démarche participative pour accompagner la démarche logique afin de définir les différentes composantes clés de pilotage de la performance auprès des futurs utilisateurs. Dans une deuxième phase, nous avons proposé une démarche procédurale SYPCo-R (Système de Pilotage de la Performance Cohérent et Réactif) en intégrant un élément jamais intégré par les autres systèmes d'évaluation de la performance, à savoir "évènement potentiel". En effet, la plupart des systèmes de pilotage par la performance sont basés sur le triplet "Objectif – Variable de Décision – Indicateur de performance". Alors que, SYPCoR que nous proposons est basé sur le quadruplet "Objectif – Évènement potentiel – Variable de Décision – Indicateur de performance". L'objectif de SYPCo-R est d'apporter une cohérence globale dans l'exploitation des composantes clés de pilotage de la performance et une réactivité en intégrant la notion d'évènement potentiel dans la prise de décision à travers une méthodologie de classement des variables de décision qui permettent de contrecarrer les évènements potentiels susceptibles d'entraver l'atteinte des objectifs. Dans une troisième phase, nous avons proposé un modèle conceptuel MCR (Modèle Conceptuel de Réactivité) qui reprend les propriétés fondamentales de la notion de réactivité sous forme d'algorithme composé d'un ensemble des règles opératoires pour identifier les défaillances de performance en terme de réactivité et leurs origines afin d'ajuster et consolider SYPCo-R. Dans une quatrième phase, nous avons proposé une démarche prédictive basée sur la simulation pour évaluer et apprécier l'impact des valeurs fixées aux alternatives associées à chaque variable de décision choisie parmi le classement résultant de la démarche SYPCo-R. Cette démarche vise aussi à anticiper les défaillances de performance pour ajuster les paramètres de MCR et SYPCo-R. Les décideurs pourront ainsi disposer d'un outil supplémentaire pour garantir la cohérence, la réactivité basée sur l'anticipation et la prédiction. Les travaux de cette thèse apportent des solutions innovantes dans la démarche de l'élaboration d'un système de pilotage de la performance en proposant un référentiel interface entre plusieurs méthodes distinctes et complémentaires qui répond efficacement aux préoccupations des décideurs. Le référentiel proposé permet de cerner la complexité d'un système et de la rendre intelligible par les décideurs. De plus, il s'apprête bien à des extensions futures basées sur une exploitation optimisée des données en temps réel.<br>This thesis aims at elaborating a framework for the development of a coherent and responsive performance management system, interface between several distinct and complementary methods. The proposed framework integrates key performance management principle s and offers an improved and promising alternative to traditional performance measurement systems. A performance management system is an essential tool for an organization. Otherwise, the conception of this system remains a complex process given the several aspects and elements that the organization must integrate into its process of evaluating and improving performance, in particular disruptive events, often neglected in the literature and very difficult to take into account in the development of a performance management mechanism. Decision-making to cover the effects of a disruptive event is not immediate as it has an inertia which can lead to a loss of overall performance. Also, decision-makers rarely have the necessary tools to verify that the used key performance management components (Objectives-Decision variables-Performance indicators) are coherent and help to move the organization towards achievement of its expected objectives. Hence, the organization operates in an uncertain environment and must be adaptable to ensure its viability. This research is motivated by a strong need raised by the achieved literature review highlighting the need to develop a performance management system that responds to current management challenges, namely : consistency between the key management components performance and responsiveness to deal with disruptive events. As a result, the main objective of this thesis is to propose a framework for the development of a coherent and responsive performance management system. The contributions of this thesis are presented in four phases. In a first phase, based on the findings of the literature review, we underlined the need to propose a structural approach SIPCo (Consistent Performance Indicator System) to identify the key components of performance management and to ensure their consistency through two methods. A logical method based on (1) a decision-making system modeling approach in order to identify the decision-making centers and (2) an informational system modeling approach in order to establish a representation of the interactive part of the key components of the performance management of each of the decision-making centers. The SIPCo method is also based on a participatory method to support the logical approach in order to define the various key components of performance management with future users. In a second phase, we proposed a procedural approach SYPCo-R (Coherent and Responsive Performance Management System) by integrating "potential event", an essential element nowadays never integrated by other performance evaluation systems. Most performance management systems are based on the triplet "Objective – Decision variable - Performance indicator" while the proposed SYPCo-R is based on the quadruplet "Objective - Potential event - Decision variable - Performance indicator". The objective of SYPCo-R is to provide overall consistency in the use of the key performance management components, and responsiveness by integrating the notion of potential event into decision-making through a methodology for classifying decision variables allowing to thwart potential events that may hinder the achievement of objectives. In a third phase, we proposed a conceptual model MCR (Conceptual Model of Reactivity) which uses the fundamental properties of the notion of reactivity in the form of an algorithm composed of a set of operating rules to identify performance failures in terms of reactivity and their origins in order to adjust and consolidate SYPCo-R. In a fourth phase, we proposed a predictive approach based on simulation to evaluate and assess the impact of the values fixed on the alternatives associated with each decision variable chosen from the ranking resulting from the SYPCo-R approach. Furthermore, this approach aims to anticipate performance failures to adjust the parameters of MCR and SYPCo-R. This will provide decision-makers with an additional tool to ensure consistency and responsiveness based on anticipation and prediction. This thesis provides innovative solutions in the process of developing a performance management system by proposing an interface by proposing an interface framework between several distinct and complementary methods that effectively responds to the concerns of decision-makers. The proposed framework allows to identify the complexity of a system and to make it intelligible to decision-makers. Moreover, this framework accepts future extensions based on an optimized exploitation of real-time data.

Le développement de techniques rigoureuses et automatiques pour la vérification des systèmes logiciels est une tâche importante. Cette thèse porte sur la vérification des propriétés de sûreté pour des programmes avec mémoire dynamique et données infinies. Elle développe un cadre basé sur la logique où les spécifications des programmes sont données par des formules. Premièrement, nous considérons l'automatisation du raisonnement pré/post-condition. Nous définissons une logique, appelée CSL, pour la spécification des structures chaînées ou des tableaux, ainsi que des compositions de ces structures. Les formules CSL décrivent des relations d'accessibilité entre les cellules de mémoire, la taille du tas et les données scalaires. Nous prouvons que le problème de la satisfiabilité pour CSL est décidable et que CSL est fermée par le calcul de la post-condition. Ensuite, nous considérons la synthèse automatique d'assertions pour des programmes avec des listes simplement chaînées. Un cadre basé sur l'interprétation abstraite est défini qui combine une abstraction finie sur la forme du tas avec une abstraction sur des séquences de données. Les abstractions sur les séquences permettent de raisonner sur leurs tailles, les multi-ensembles de leurs éléments, ou les relations entre leurs données à des différentes positions. Nous définissons une analyse inter-procédurale qui calcule l'effet de chaque procédure de façon locale sur la partie du tas accessible à partir de ses paramètres. Ces techniques sont implantées dans un outil qui montre que notre approche est assez puissante pour la génération automatique de résumés de procédure non-triviales et le raisonnement pré/post-condition<br>In this thesis, we focus on the verification of safety properties for sequential programs manipulating dynamic data structures carrying unbounded data. We develop a logic-based framework where program specifications are given by formulas. First, we address the issue of automatizing pre/post-condition reasoning. We define a logic, called CSL, for the specification of linked structures or arrays, as well as compositions of these structures. The formulas in CSL can describe reachability relations between cells in the heap following some pointer fields, the size of the heap, and the scalar data, We prove that the satisfiability problem of CSL is decidable and that CSL is closed under the computation of the strongest post-condition. Second, we address the issue of automatic synthesis of assertions for programs with singly-linked lists. We define an abstract interpretation based framework which combines a specific finite-range abstraction on the shape of the heap with an abstract domain on sequences of data. Different abstractions on sequences are considered allowing to reason about their sizes, the multisets of their elements, or relations on their data at different positions. We define an interprocedural analysis that computes the effect of each procedure in a local manner, by considering only the part of the heap reachable from its actual parameters. We have implemented our techniques in a tool which shows that our approach is powerful enough for automatic generation of non-trivial procedure summaries and pre/post-condition reasoning

Avec l'expansion des dispositifs mobiles, l'efficacité de la saisie de texte est un défi de plus en plus important pour l'interaction homme-machine. Or, nous observons que, bien que les claviers type AZERTY ou téléphone, traditionnellement utilisés sur ces supports, soient évalués comme sous-optimaux, et, bien que de nombreuses alternatives évaluées comme plus performantes soient proposées dans la littérature, ces nouvelles alternatives restent très marginalement utilisées. Sur la base de cette observation, nous argumentons que la finalité des évaluations ne tient compte que d'un aspect du clavier, aspect qui n'est pas représentatif de la capacité d'un utilisateur à intégrer les concepts proposés dans son quotidien. Nous proposons en conséquence une stratégie complémentaire d'évaluation sur la base d'une évaluation heuristique des claviers logiciels. Par ailleurs, de manière à faciliter la mise en œuvre des évaluations et simplifier le design de nouveaux claviers, nous proposons une nouvelle version (E-Assist II) de la plate-forme E-Assiste. Elle permet, en premier lieu, de facilité le design et le déroulement des expérimentations, et plus largement d'encadrer les évaluations théoriques, expérimentales et heuristiques des claviers. Une version TinyEAssist permet également de déployer des expérimentations sur des supports mobiles (téléphones portables notamment). En second lieu, sur la base de l'étude de la structure des claviers logiciels, nous avons de plus proposé un langage de spécification des claviers permettant de générer des claviers logiciels complexes (interagissant potentiellement avec des systèmes de prédiction) à des fins d'expérimentation ou de simple usage. Enfin, sur la base des critères de performance mis en évidence par les évaluations heuristiques, nous proposons quatre nouveaux paradigmes de claviers. Parmi ces paradigmes deux ont offert des perspectives particulièrement intéressantes : en premier lieu le clavier multi-layer consistant à conduire progressivement, au cours d'une période transitoire, un utilisateur d'une distribution de touches type AZERTY vers une distribution de touches optimisée ; Le second consistant à faciliter l'accès aux caractères type accents, majuscules ou ponctuation, souvent déconsidérés dans l'optimisation des claviers logiciels<br>The expansion of mobile devices turn text input performances a major challenge for Human-Machine Interaction. We observed that, even if traditional QWERTY soft keyboards or telephone based soft keyboard were evaluated as poorly efficient, and, even if several alternatives evaluated as more efficient were proposed in the research field, these new alternatives are rarely used. Based on this observation, we argue that the goal of soft keyboard evaluation focus on long term performances whereas does not take into account the perspective for a user to use it in his quotidian. Consequently, we propose a complementary evaluation strategy base on heuristic evaluation methodology. In order to ease the evaluation and design of new soft keyboards, we proposed a new version (E-Assist II) of the E-Assiste plate-form. This plate-form aims, at first, to facilitate the design and procedure of experimentations and, more generally, to guide the theoretical, experimental and heuristic evaluations. A compact version (TinyEAssist) enables to perform experimentation on mobile environment such as mobile phone. At second, based on soft keyboard structure study, we proposed a keyboard specification language enabling to generate complex keyboard (including soft keyboard interacting with prediction systems). The generated soft keyboards may be used into the experimentation plate-form or interacting with the exploration system. At last, based on the criteria highlighted by the heuristic evaluation, we proposed four new soft keyboard paradigms. Among them two paradigms showed interesting perspectives: at first the multilayer keyboard consist in accompanying the user from a standard QWERTY layout to an optimized layout during a transition period; the second consist in accelerating the access to the characters such as accents, upper-case, punctuation, etc. , frequently ignored in the keyboard optimizations

Les Logiciels Tuteurs Fermés, ou LTF, sont utilisés dans les classes dans de nombreux collèges en mathématiques. Pour analyser leur place potentielle dans l'École, nous avons construit un modèle centré sur la notion d'institution, centrale dans la Théorie Anthropologique du Didactique, définie, par nous, à partir des critères suivants : la réalité sociale, la légitimité, la stabilité et la spécificité. Pour comprendre si un LTF peut être utilisé en tant qu'institution d'enseignement et d'apprentissage, chacun des quatre logiciels de notre étude a été inspecté entièrement par un expert dont les captures vidéos nous ont permis des comparaisons avec le travail des élèves de notre expérimentation. Le décryptage de l'ensemble de ces données a été conduit grâce à un logiciel d'analyse du comportement, The Observer de chez Noldus. Plus spécifiquement, en ce qui concerne l'apprentissage des mathématiques, nous avons choisi d'analyser la façon dont les quatre LTF proposent un apprentissage du calcul, qu'il soit arithmétique, numérique ou algébrique. Nous avons pour cela étendu au numérique le cadre théorique conçu par Houdement et Kuzniak pour l'apprentissage de la géométrie, et notamment les notions de paradigme et d'espace de travail. Les analyses que nous avons conduites nous ont permis de montrer que les LTF de notre étude ne peuvent que difficilement être utilisés en tant qu'institution autonome de l'institution principale qu'est la classe ordinaire. Mais leur usage peut être valorisé pour l'apprentissage des élèves en créant des institutions parallèles adaptées<br>Closed Tutors Software or CTS are used in classrooms in many schools in mathematics. To analyze their potential role in the school, we have built a model based on the notion of institution, central to the Anthropological Theory of Didactics, defined by us, based on criteria of social reality, legitimacy, stability and specificity. To understand whether CTS can be used as an institution of teaching and learning, each of four software in our study has been fully inspected by an expert whose captures videos allow us some comparisons with the work of students our experiment. The decryption of all data was conducted using a software analysis of behavior, the Observer from Noldus. More specifically, with regard to mathematics learning, we chose to analyze how the four CTS offer numeracy, whether arithmetic, numerical or algebraic. For this, the theoretical framework developed by Houdement and Kuzniak for learning geometry has been extended including the notions of paradigm and workspace. The tests we conducted we have shown that CTS of our study can hardly be used as an autonomous institution of the regular classroom which is the primary institution. But their use can be valued for student learning by creating parallel institutions adapted

Apprendre à lire est une activité complexe qui s'appuie sur différentes capacités cognitives, dont l'attention visuelle. Absente des programmes scolaires, le rôle de l'attention visuelle pour l'apprentissage de la lecture est pourtant largement documenté dans la littérature scientifique. Dans cette thèse, nous avons donc conçu un logiciel éducatif original d'entraînement de l'attention visuelle, Evasion, et évalué l'impact de son utilisation au sein de la classe.Pour ce faire, une revue de littérature a été menée pour identifier plus précisément quelles sont les dimensions de l'attention visuelle impliquées en lecture et comment les entraîner au mieux. Un cadre conceptuel théorique que nous avons développé permet d'interpréter ces éléments et suggère que les dimensions à cibler sont la quantité totale d'attention visuelle et sa dispersion dans l'espace. Ces deux dimensions semblent particulièrement bien entraînées par les jeux vidéo d'action, dont l'effet sur l'attention visuelle a été lui aussi expliqué dans le cadre de notre modèle.Pour les entraîner au mieux au sein d'Evasion, nous avons mêlé les tâches, dont l'effet sur ces dimensions a été validé, avec les propriétés des jeux vidéo d'action. Notre logiciel prend la forme de quatre mini-jeux, dont les propriétés s'ajustent au niveau de l'élève grâce à un algorithme d'adaptation de la difficulté développé par notre équipe. Evasion devait être utilisé en classe pendant 10~h au total, à raison de 3 sessions hebdomadaires de 20 minutes. L'expérimentation a porté sur 730 élèves de CP répartis en deux groupes d’entraînement. Les deux groupes étaient appariés quant à leurs compétences cognitives avant entraînement. En post-entraînement, les performances du groupe Evasion ont été comparées à celles du groupe contrôle, qui recevait un entraînement de la compréhension orale en anglais.Les résultats de cette expérience écologique montrent que les capacités d'attention visuelle et de lecture ne progressent pas davantage suite à l'utilisation d'Evasion que suite à l'utilisation d'un entraînement contrôle. Des analyses supplémentaires révèlent que le protocole a été peu suivi en classe, et que le temps d'entraînement est un facteur expliquant l'amplitude de l'amélioration des dimensions attentionnelles ciblées. Par ailleurs, il semblerait que les entraînements proposés aient été trop faciles. Ces résultats ouvrent de nouvelles perspectives sur les améliorations à apporter à notre logiciel et, plus généralement, sur les conditions de mise en oeuvre d'expériences écologiques dont les besoins sont spécifiques<br>Learning to read is a complex activity that relies on different cognitive abilities, including visual attention. The role of visual attention in learning to read is widely documented in the scientific literature but absent from school curricula. In this thesis work, we designed an original educational software, called Evasion, for visual attention training in the classroom and we evaluated its impact on beginning readers' performance.A literature review was first conducted to identify the dimensions of visual attention that are involved in reading and how best to train them. We then propose a conceptual framework which allows us to interpret these results. We conclude that the dimensions to be targeted are the total amount of visual attention resources and attention spatial dispersion. These two facets of attention seem to be particularly well driven by action video games, whose effect on visual attention has also been characterized in our model.To train visual attention resources and dispersion as well as possible within Evasion, we have mixed the tasks known to improve these attentional dimensions with the properties of action video games. Our software includes four training mini-games and an adaptive difficulty algorithm developed by our team to adjust the game properties online to the child needs. The training program was provided in classroom over a period of ten weeks at a rate of three 20-minute sessions a week. It was proposed to a large sample of 730 beggining readers for reading difficulty prevention.The impact of Evasion was assessed before and after training as compared to a control group that used an intervention program conceived to improve oral comprehension in English. The results of this ecological experiment show that visual attention and reading did not improve more following Evasion than control training. Additional analyses revealed that training time was poorly respected while this factor relates to the magnitude of improvement in the attentional dimensions we targeted. The analyses further suggest a problem in the level of difficulty of the mini-games. Overall, our work opens up new perspectives on the improvements to be made to our software and, above all, on the conditions for successful implementation of ecological experiments

Les claviers logiciels se sont démocratisés pour rendre possible la saisie de textes en mobilité sur des dispositifs dépourvus de claviers physiques tels que les téléphones portables nouvelle génération. Cependant, ces claviers présentent plusieurs inconvénients comme la lenteur de la saisie et la fatigue engendrées pour les utilisateurs déficients moteurs. La solution intuitive était d'allier ces logiciels à des listes contenant les mots susceptibles de continuer la saisie d'un mot initié par l'utilisateur. Bien que ces listes, dites listes de prédiction, réduisent le nombre de clics et le nombre d'opérations, la vitesse de saisie de l'utilisateur a diminué. Une expérimentation outillée d'un système de suivi du regard a ainsi permis de déterminer des " stratégies " de fonctionnement de l'utilisateur face à une liste de mots. Ces résultats ont ainsi permis d'affiner les modèles de prédiction de manière à réduire l'écart séparant les performances prédites des performances réellement enregistrées. A partir des constats effectués lors de la première expérimentation, nous proposons deux variantes de l'utilisation des listes de prédiction de mots. La première propose un nouveau moyen d'interagir avec la liste de mots et permet ainsi de maximiser l'utilisation de celle-ci. La seconde évalue un repositionnement de la liste de mots de manière à réduire le nombre de mouvements oculaires vers la liste. Ces deux évolutions, évaluées théoriquement puis au moyen d'une expérimentation utilisateur, permettent ainsi d'améliorer les performances de saisie par rapport à une liste de prédiction de mots classique<br>Predictive model and simulation tool for a best evaluation of soft keyboard augmented by words prediction list The software keyboards are used to enable text input in mobility and for devices without physical keyboards, such as the new generation of mobile phones. However, these keyboards have several drawbacks such as slowness text entry and fatigue generated for motor impaired users. The solution was to combine software keyboard to lists containing the words likely to continue the word introduced by the user. While these lists, so-called prediction lists, reduce the number of clicks and the number of operations, the speed of user input has decreased. An experiment with an eye tracking system has identified the "strategies" of the user while using and searching a list of words. These results were helpful to refine the prediction models in order to reduce the gap between the performance predicted and the performance actually recorded. Based on observations made during the first experiment, we propose two variants of the use of word prediction list. The first proposes a new way to interact with the list of words and allows maximum use of it. The second evaluates a repositioning of the list of words in order to reduce the number of eye movements to the list. These two propositions were theoretically and experimentally evaluated by users. These software can improve the input performances compared with a classic word prediction list

Cette thèse a pour sujet la mobilité faible des applications et en particulier la communication entre entités mobiles. Nous nous sommes tout d'abord intéressés aux relations existant entre le paradigme des objets actifs et celui des applications mobiles. De nombreux protocoles pour assurer les communications entre objets mobiles ont été décrits dans la littérature mais leurs performances n'ont jamais été étudiées formellement. Nous avons isolé des propriétés permettant de les classer en trois familles~: la poste restante, la recherche et le routage. Après avoir choisi deux protocoles utilisés dans des bibliothèques Java, nous avons entrepris leur étude à l'aide de chaînes de Markov, le but étant de pouvoir déterminer le temps moyen nécessaire pour communiquer avec un agent mobile. Le mécanisme des répéteurs est représenté à l'aide d'une chaîne à espace d'états infini. Nous avons pu exprimer deux métriques: le temps moyen de réponse du système et le nombre moyen de répéteurs. Le cas du serveur nécessite l'analyse d'une chaîne à espace d'états fini qui est résolue numériquement. Pour valider nos modèles nous avons utilisé un simulateur à événements discrets puis, nous avons mené des expérimentations sur un réseau local et sur un réseau régional. Les résultats ont été comparés à ceux obtenus théoriquement ce qui nous a permis de montrer que les performances de nos modèles sont tout à fait acceptables. Il est donc possible de les utiliser pour prédire les performances. Enfin, nous terminons ce travail par la présentation d'un nouveau protocole de communications utilisant des répéteurs à durée de vie limitée et un serveur. Nous montrons qu'il est possible d'obtenir de bonnes performances sans les aspects négatifs des deux protocoles précédents.

Notre premier objectif est de proposer des méthodes et des outils de vérification du respect des contraintes temporelles d'une application temps réel. Le principal cadre d'application de nos travaux est celui des applications embarquées dans l'automobile distribuées autour d'un réseau CAN. La validation est menée en couplant les techniques de vérification : simulation, analyse et observation sur prototypes. L’apport principal de cette thèse réside en la conception de modèles analytiques qui fournissent des bornes sur les métriques de performance considérées (temps de réponse, probabilité de non-respect des échéances) ou permettant d'évaluer l'occurrence d'événements rares (temps d'atteinte de l'état bus-off d'une station CAN). Nous proposons également une analyse d'ordonnancabilité des applications s'exécutant sur des systèmes d'exploitation se conformant au standard posix1003. 1b. Ensuite, considérant qu'il existe généralement plusieurs solutions d'ordonnancement faisables à un même problème, nous avons défini des critères de choix et avons expérimenté une approche, utilisant un algorithme génétique, pour parcourir l'espace des solutions. Notre second objectif est d'étudier des mécanismes d'ordonnancement qui garantissent le respect des échéances du trafic a contraintes strictes tout en minimisant les temps de réponse du trafic a contraintes souples. Nous évaluons les performances de la politique dual-priority pour l'ordonnancement de messages. Pour son utilisation dans des environnements bruites, nous proposons un mécanisme simple donnant des garanties sur la qualité de service exprimée en termes de probabilité de respect des échéances et s'adaptant en-ligne a des conditions de perturbations variables. Nous proposons également une politique concurrente, basée sur une technique de lissage de flux, qui est d'une mise en oeuvre plus aisée. Cette politique préserve la faisabilité du système et sa faible complexité algorithmique permet son utilisation en-ligne.

L’utilisation d’un processus de conception ‘Agile’, orienté métier et indépendant de la plateforme de développement (BRDF, Business Rule Developement Framework) rejoint les objectifs stratégiques et les recommandations du U. S. Roadmap for national action on clinical decision support et ce en prenant en considération trois critères représentants un véritable défi pour les concepteurs de systèmes : 1)- la modélisation des processus métiers du domaine d’application, 2)- la modélisation des connaissances du domaine d’application et 3)- l’Agilité des différentes étapes de conception. L’utilisation de ce processus à l’Hôpital Européen Georges Pompidou (HEGP) dans le contexte métier de la validation pharmaceutique a permis d’incorporer l’utilisateur final (pharmacien) dans 5 des 8 étapes de conception et de développement. Il a également permis de dériver 427 règles de décision. 140 règles ont été implémentées pour le contrôle et l’adaptation de la posologie des prescriptions de médicaments nephrotoxiques et ont déclenché 5824 alertes pour 71413 prescriptions médicamenteuses analysées (8,16%). L’utilisation d’un processus de test et d’affinement des alertes cliniques basé sur l’utilisation d’un entrepôt de données clinique (Clinical Data Warhouse, CDW) facilite l’optimisation des alertes dans l’optique de minimiser l’impact des effets du ”alert fatigue syndrom” et de maximiser la sécurité des patients. L’utilisation de ce processus sur les alertes développées pour le contrôle et l’adaptation posologique des prescriptions de médicaments nephrotoxiques à l’HEGP a montré qu’après plusieurs itérations du processus, 45 (16,07%) alertes testées ont été supprimées, 105 (37,5%) alertes ont subi des modifications et 136 nouvelles alertes ont été rajoutées à la base de règles du système d’alerte. La comparaison prospective entre le système d’alerte et les pharmaciens valideurs à l’HEGP durant une étude de 7 mois a montré la supériorité du système d’alerte sur les pharmaciens valideurs<br>Using an ‘Agile’, business oriented and development platform-independent software design process (BRDF, Business Rule Developement Framework) meets one of the strategic objectives of the U. S. Roadmap for national action on clinical decision support by taking into consideration three important criteria posing a particular challenge to software designers: 1) business processes, 2) knowledge modeling of the context of application, and 3) the agility of the various design steps. Using BRDF at the Georges Pompidou University Hospital (HEGP) in the business context of pharmaceutical validation allows to include the end user (the pharmacists) in 5 of the 8 design steps of BRDF, we have also been able to derive 427 clinical decision rules. 140 clinical decision rules have been implemented as clinical alerts to control and adapt nephrotoxic medication orders; these rules checked 71,413 medication orders and fired 5824 (8. 16%) alerts. Using a clinical data warehouse-based process for refining medication orders alerts facilitates alert optimization toward the goal of maximizing the safety of the patient and minimizing overridden alerts. Using this process on the alerts implemented with BRDF to control and adapt nephrotoxic medication orders prescribed at the HEGP showed that after several iterations of this process, 45 (16. 07%) decision rules were removed, 105 (37. 5%) were changed and 136 new rules were introduced. Prospective validation of the alert system at the HEGP hospital during 7 months study period showed the superiority of the alert system in comparison with the daily pharmacist’s practice of the medication orders validation activity

La dispersion atmosphérique intentionnelle ou accidentelle de substances toxiques d'origine nucléaire, radiologique, biologique ou chimique (NRBC) peut avoir des conséquences sanitaires graves. Pour les estimer, l'évaluation de risque NRBC s'appuie, entre autres, sur des modèles d'écoulement/dispersion atmosphérique. En calculant l'évolution spatio-temporelle de la concentration en polluant, ces modèles permettent de quantifier l'effet toxique potentiel sur l'homme. Les évaluer suppose de comparer leurs résultats à des données expérimentales. Or, les méthodologies existantes de comparaison modèle/expérience ont deux défauts : d'une part elles sont inadaptées au contexte d'évaluation de risque NRBC, et d'autre part elles sont biaisées car elles reposent sur des comparaisons directes modèle/expérience. La turbulence dans la couche limite atmosphérique introduit une composante aléatoire importante dans les observations, donc un écart inévitable au résultat de modèle, fût-il « parfait ». Dans cette thèse, deux outils sont construits pour combler ces lacunes. Le premier est une méthodologie de comparaison modèle/expérience spécifiquement adaptée à l'évaluation de risque. Le second est un modèle statistique empirique de calcul de l'incertitude des résultats de simulation. Associé à un modèle de dispersion probabiliste, le modèle statistique proposé permet de calculer une enveloppe de réponse plutôt qu'un résultat « moyen » unique, celui-ci étant peu exploitable malgré son omniprésence dans les évaluations de risques actuelles. Utilisés conjointement, les deux outils développés dans cette thèse donnent à la comparaison modèle/expérience l'objectivité souhaitée<br>Atmospheric dispersion of contaminated clouds following deliberate or accidental releases of CBRN (chemical, biological, radiological, nuclear) toxic substances may have serious health impacts. In order to estimate them, CBRN risk assessment activities rely, among other things, on atmospheric dispersion models. These models compute the concentration field of pollutant in order to quantify potential adverse effects on human population. They need to be evaluated, which means their outputs have to be compared to experimental data within an appropriate methodology. Now, existing evaluation methodologies have two flaws: firstly they are not suited to risk assessment, and secondly their results may be somewhat arbitrary because they are based on direct comparisons between observations and model results. Turbulence in the atmospheric boundary layer introduces a large random component in the observations, and thus an inevitable gap between observations and model results, be the latter "perfect". In this thesis two tools have been built to fix these issues. The first one is an evaluation methodology suitable for the risk assessment context. The second one is an empirical statistical model meant to estimate the uncertainty in the simulation results. It can be associated to an atmospheric dispersion model with probabilistic capabilities in order to produce an envelop of the answer rather than a unique "average" result, the latter being of little use despite its omnipresence in current risk assessment studies. When used jointly, the two tools developed in this thesis enable model/experiment comparisons to be more objective and less subject to experimental randomness

Bien que les outils d'édition graphique semblent rendre aisée la création de pages Web, le développement d'applications sur le Word Wide Web est une activité complexe. Cette complexité découle de la nature sans cesse évolutive de ces applications, la complexité des besoins utilisateurs et des temps de développement souvent très courts. Pour pouvoir gérer cette complexité, des modèles deviennent fondamentaux. Même si la navigation est considérée comme l'un des éléments critiques pour la spécification des applications Web, les méthodes dont nous disposons aujourd'hui ne permettent pas de représenter tous les aspects liés à la navigation d'une façon complète et non ambigue͏̈. Cette thèse répond à ce besoin de méthodes efficaces permettant de décrire la navigation des applications Web en proposant une technique de description formelle dénommée StateWebCharts (SWC) et un environnement de conception qui supporte l'édition et la simulation des modèles décrits dans ce formalisme<br>In spite of the apparent facility of build Web pages given by current visual environments, the development over the World Wide Web is complex due to many factors such as the evolving nature of applications, the multidisciplinary nature of development team, the competitive points of views for the application and complexity of user requirements, and the unrealistic and narrow schedules for the development. To deal with such as complexity, modelling support is essential. Currently modelling methods provide little support to describe in complete and unambiguous manner navigation in web applications even though navigation is considered as a critical element. The present work proposes a formal description technique namely StateWebCharts (SWC), which extends StateCharts models to model the navigation of Web applications and a design environment supporting the edition and simulation of models described in the formalism

Les systemes temps reel sont des dispositifs constitues de materiels et de logiciels soumis a des contraintes a la fois fonctionnelles et temporelles pour realiser des traitements, et agir sur leur environnement. Des exemples de domaines o u on rencontre de tels systemes sont les telecommunications, le nucl eaire, l'avionique ou le medical. Ces systemes sont souvent critiques a cause d'enjeux humains et economiques importants. Leur developpement exige donc des methodes tres ables. L'approche synchrone a et e proposee dans le but de repondre a cette attente. Ses fondements mathematiques o rent un cadre formel propice a la description et la validation des systemes temps reel. Parmi les modeles de specification synchrone, le modele multi-horloge ou polychrone se distingue par le fait qu'il permet de decrire des systemes o u chaque composant peut avoir sa propre horloge d'activation. Outre la validation formelle, il favorise des approches orientees composants et le d eveloppement modulaire de systemes a grande echelle. Cette these propose une m ethodologie de conception de syst emes temps reel en utilisant comme formalisme de description le langage synchrone Signal fond e sur le mod ele polychrone. Elle utilise les outils et techniques formels bas es sur ce modele pour verifier des proprietes comportementales portant sur des aspects tant fonctionnels que non fonctionnels. Cette demarche facilite l' evaluation des choix de conception. La methodologie propos ee permet de concevoir des systemes comportant des m ecanismes asynchrones a l'aide de l'approche synchrone. Elle illustre la caracterisation de comportements temps r eel dans le modele polychrone. L'avionique est le domaine d'application privilegie par la these. Cette derniere s'inscrit dans le cadre du projet europ een IST SafeAir (Advanced Design Tools for Aircraft Systems and Airborne Software), regroupant plusieurs industriels. Nous nous sommes particulierement interesses a la conception d'applications suivant le mod ele d'architecture IMA (Integrated Modular Avionics) sur lequel repose la norme avionique ARINC. Cela a conduit a la r ealisation d'une bibliotheque Signal de composants, constituee en majeure partie de services d'un ex ecutif temps reel d e nis par ARINC.

Pour réduire l’impact environnemental d’un bâtiment, l’intégration de l’analyse du cycle de vie (ACV) en phase de conception peut s’effectuer selon deux approches : par l’utilisation d’un outil simplifié, tel qu’Athena, par les professionnels de la construction, ou par la collaboration d’un analyste en ACV en utilisant un outil plus complexe, tel que SimaPro. L'objectif du projet est d'évaluer les forces et les limites de ces outils pour l’analyse de bâtiments en bois innovants au Canada. Les résultats sont basés sur une étude de cas : un immeuble à bureaux de six étages avec une structure en bois lamellé-collé hors norme au moment de la construction. Pour Athena, plus de flexibilité est souhaitable, incluant un contrôle des cycles d’entretien des matériaux et l’ajout du degré d’incertitude des résultats. SimaPro offre plus de flexibilité et de transparence, mais une meilleure représentation des matériaux de construction dans le contexte canadien serait nécessaire.<br>To reduce the environmental impact of a building, integration of life cycle assessment (LCA) during design phase can follow two approaches: use of a simplified tool, such as Athena, by construction professionals, or use of a more complex tool, such as SimaPro, in collaboration with an LCA analyst. The objective of the project is to evaluate the strengths and limitations of these tools when analysing innovative timber buildings in Canada. The results are based on a case study: a six-storey office building with glulam structure that was outside prescriptive standard at time of construction. For Athena, possible improvements include more flexibility, including a better control over the maintenance cycles of materials, as well as more information regarding the uncertainty of the results. SimaPro offers more flexibility and transparency. However, more processes representing building materials in the Canadian context would be necessary.

Les examens de biologie ne sont pas toujours prescrits à juste titre. Des documents de bonnes pratiques sont élaborés pour rationaliser la prescription et maximiser la pertinence des actes de biologie médicale. Malheureusement ces documents sont peu consultés par les prescripteurs. Dans un premier temps, nous avons développé un système facilitant la consultation de ces documents. Le langage UML a été utilisé pour modéliser les catégories d’éléments d’information contenus dans ces documents et leurs relations. Nous avons utilisé ce modèle pour mettre en œuvre une interface homme-machine. L évaluation de l’interface a montré que celle-ci reçoit un bon accueil de la part des médecins et infirmiers. Dans un deuxième temps, nous sommes allés plus loin pour implémenter les règles de juste prescription dans un système d’information hospitalier (ORBIS) afin d’afficher automatiquement des informations pertinentes selon le contexte patient. Nous avons d’abord évalué l’implémentabilité des règles de juste prescription selon les facteurs intrinsèques et extrinsèques aux recommandations. Nous avons pu transformer le contenu des documents de bonnes pratiques en format exécutable grâce à une modélisation conceptuelle et par la suite, nous avons implémenté une trentaine de règles de juste prescription dans le système ORBIS. Notre première approche a conduit à une application facilitant l’accès à ces documents ainsi qu'au développement d’un guide de rédaction des documents de juste prescription. Notre deuxième travail a permis de clarifier les problèmes face à l’implémentation et d’intégrer les règles dans la pratique quotidienne en les implémentant dans le système ORBIS<br>Laboratory tests are not always prescribed appropriately. Guidelines have been developed to rationalize the test-ordering behavior and maximizing the appropriateness of laboratory medicine. However; these guidelines are not frequently consulted by physicians. We decided to develop a system facilitating the consultation of these guidelines. Unified Modeling Language was used to represent the categories of information elements contained in these documents and their relationships to each other. We used the model generated to implement a computerized interface. The interface was found to be rapid and easy to use. In the next step, we went further to implement the test-ordering rules in a HIS (hospital information system) to automatically display relevant recommendations according to the patient context. Therefore, we analyzed the aspects related to the integration of test-ordering recommendations in HISs. Firstly, we evaluated the implementability of test-ordering rules according to intrinsic and extrinsic factors to the recommendations. We then transformed the content of the guidelines in an executable format using a conceptual modeling and subsequently, we have implemented thirty two test-ordering rules in our HIS named ORBIS. Our guideline modeling led to an application for facilitating access to these documents. It also led to the development of a manual for writing harmonized laboratory guidelines. The modeling of test-ordering rules and the evaluation of their implementability, have clarified the gaps against the implementation. We finally implemented a selection of test-ordering rules in the hospital information system to integrate them into daily practice

Les outils de simulation sont des moyens pour faciliter la mise en place d'une production sur les Machines Outil à Commande Numérique, ces outils sont devenus très courants dans l'industrie et, par conséquent, dans l'éducation. Plusieurs problèmes importants émergent, telles que des questions d’ordre pédagogique, des aspects liés à l’ergonomie des interfaces, le coût d'acquisition de l'équipement et d'adaptabilité des étudiants aux multitudes de logiciels de fabrication assistée par ordinateur, de ce fait le problème de la sélection du logiciel est soulevé dans l'éducation afin d'assurer une efficacité des processus d'enseignement et d'apprentissage des étudiants.Cette thèse est conduite dans l’objectif d’étudier une méthodologie pour sélectionner un logiciel de FAO qui pourrait être efficace en tant que support d’apprentissage de la FAO en premier cycle des universités techniques, des écoles d’ingénieurs et autres établissements similaires. Les facteurs déterminants l’efficacité des étudiants utilisant un logiciel dans leurs apprentissages de la FAO ont été déduits du cadre théorique de la thèse qui s’est basé sur la théorie de l’activité. Cette théorie prend en considération le contexte global de cette activité d’enseignement-apprentissage de la FAO à savoir l’étudiant, l’artefact, le professeur, l’établissement et la communauté des éditeurs de logiciels.Le traitement statistique des données recueillies à travers les réponses d’un échantillon de 50 étudiants ont été élaboré dans le but de confirmer nos hypothèses sur les principaux critères d'évaluation de logiciel de simulation en éducation<br>Simulation tools as means to facilitate setting up a production have become very common in industry and, therefore, in education. Among several significant problems, like pedagogical issues, the cost of equipment acquisition and the adaptability of students to the multitude of Computer-Aided Manufacturing, it is raise in education the problem of selecting software in order to ensure maximum effectiveness of teaching process and students learning.This research study was designed to investigate a methodology to select CAM software that could be effective as a support of CAM learning in university, taking into account different features of CAM learning. We determine the student effectiveness in learning factors of CAM software and further, determine the relationship between the different main factors. The research was conducted using a questionnaire submitted to 50 students attending the second academic year of Mechanical Design and Production. The study provides results from empirical test of these relationships and provides criteria for evaluation simulation of software in education

La gestion des données réparties en environnement de grille de données pose de nouveaux problèmes et présente un réel défi : la découverte de ressources, l'allocation de ressources, la réplication, les services de monitoring pour l'optimisation de requêtes. . . Etc. Les systèmes de grille diffèrent principalement des systèmes parallèles et distribués par la grande échelle et l'instabilité (i. E. La dynamicité des nœuds). Dans cette thèse, nous nous intéressons à la phase de découverte de ressources pour l'évaluation efficace de requêtes réparties en environnement de grille de données. Nous effectuons d'abord un état de l'art sur les principaux travaux de recherche portant sur la découverte de ressources en se focalisant sur les critères importants (e. G. Passage à l'échelle, découverte fiable, faible coût de maintenance) pour la découverte de sources de données qui est spécifique à un environnement de grille de données. Dans cette perspective, nous proposons ensuite une méthode de découverte de sources de données, basée sur l'utilisation des Tables de Hachage Distribuées (THDs), permettant un accès permanent en présence de la dynamicité des nœuds de n'importe quel nœud d'une Organisation Virtuelle OVlocale à toute autre OVi (i [différent de]locale) dans le système, avec un faible coût de maintenance entre les THDs. Après la découverte de ressources, il est très important d'observer l'état actuel de ressources surtout que ces dernières sont partagées à une grande échelle, afin de prendre des décisions sur le choix du nœud d'exécution d'une jointure (ou d'une partie d'une jointure) par exemple. L'observation ou le monitoring de ressources peut être effectué pendant l'allocation initiale ou l'exécution. Dans ce contexte, nous proposons une méthode permettant la prise en compte de la variation des valeurs des paramètres hôtes et réseaux, pendant l'exécution, dans le calcul du temps de réponse d'une opération relationnelle. L'idée est alors d'intégrer les informations de monitoring dans un modèle d'exécution à base d'agents mobiles développé au sein de notre équipe. Enfin, nous validons nos propositions par une évaluation des performances<br>The distributed data management in grid systems raises new problems and presents real challenges: resource discovery, resource allocation, replication, monitoring services for query optimization. . . Etc. Grid systems differ mainly from parallel and distributed systems by the two characteristics: the large scale and the system instability (i. E. The dynamicity of nodes). In this thesis, we are interested in the resource discovery phase for an efficient query evaluation in data grid environments. First, we present a state of the art on the main research works of resource discovery by focusing on the important criteria (e. G. Scaling, reliable discovery, maintenance cost) for data source discovery which is specific to data grid environments. In this perspective, we propose a new method of data source discovery based on Distributed Hash Tables (DHT) allowing a permanent access -in the presence of the dynamicity of nodes- from any node of a Virtual Organization VOlocal towards all other VOi (i [different from]local) in the system with a minimum maintenance cost between the DHT. After the resource discovery phase, it is very important to monitor the current state of resources especially that these last ones are shared on very large scale environments. The resource monitoring can be made during the initial allocation or the execution phase, in order to take decisions on the choice of the execution node of a join (or of a part of a join) for example. In this context, we propose a method considering the variation of host and network parameter values, at runtime, in the calculation of the response time of a relational operation. The proposed method integrates monitoring information into an execution model based on mobile agents developed in the Pyramid team. Finally, we validate our proposals by a performance evaluation

Les objectifs que je devais atteindre dans le cadre de cette Thèse étaient de réaliser un démonstrateur de surveillance en temps réel au sein des forces armées et de pratiquer son évaluation, afin de répondre à la question qui m’était posée de la faisabilité et de l’intérêt de ce type de surveillance en milieu militaire. A partir de ce travail, je devais fournir des propositions pour la généralisation du concept à l’ensemble des forces projetées. J’ai imaginé et participé au développement du système de surveillance spatiale des épidémies au sein des forces armées en Guyane « 2SE FAG », avec l’IMTSSA et différents partenaires depuis 2002, ce qui permettait de répondre à un nouvel objectif de l’Etat-Major des Armées, fixé après un sommet de Défense de l’OTAN. J’ai pris en compte des aspects médicaux, technologiques, humains et organisationnels pour développer ce prototype. 2SE FAG a été conçu comme un procédé de surveillance épidémiologique mis en oeuvre à l’aide d’une communauté de services réseaux basés en Guyane et en métropole. Son développement s’inscrivait dans le cadre d’un arrangement technique franco-britannique, auquel j’ai participé en effectuant entre autres un séjour de 6 mois dans les armées britanniques. J’ai réalisé le déploiement de 2SE FAG en Guyane en octobre 2004 et le système a fonctionné sans discontinuité depuis. La juxtaposition des réseaux a permis de produire des données épidémiologiques opérationnelles qui ont fait la preuve de leur utilité, en particulier au moment de l’épidémie de dengue du premier semestre 2006. L’alerte précoce déclenchée à cette occasion plusieurs semaines avant le système de surveillance réglementaire des forces armées a certainement joué un rôle dans le contrôle de l’épidémie en milieu militaire alors que celle-ci explosait en milieu civil. L’évaluation représentait un travail fondamental pour fournir un retour d’expérience utile et j’ai réalisé différentes études en collaboration avec des organismes extérieurs (SACT de Norfolk, ISPED de Bordeaux, LSTM de Liverpool, Cire Antilles Guyane). Cette démarche permettait à la fois d’apporter des modifications à 2SE FAG mais aussi de faire évoluer positivement l’ensemble des projets du type 2SE du système ASTER. A partir de ces travaux, j’ai pu développer et proposer une nouvelle méthode d’évaluation des systèmes de surveillance militaires destinés à l’alerte précoce pour les forces en opérations extérieures. J’ai identifié des améliorations qui sont encore à apporter au système, mais les différents objectifs ont été considérés comme atteints, à savoir la preuve de la faisabilité de la surveillance en temps réel dans les armées, du bénéfice apporté par un tel système et de son caractère interopérable. L’intérêt de ces travaux a déjà été souligné par des hautes instances nationales et internationales. J’ai réalisé avec les autres co-inventeurs du système une demande de dépôt de brevet au niveau de l’INPI le 25 août 2006. La surveillance épidémiologique en temps réel reste un défi d’avenir pour les armées modernes. Les enseignements acquis grâce à 2SE FAG constituent déjà un retour d’expérience unique au sein des armées de l’OTAN. Mais je pense que l’effort de recherche et de développement doit rester important, dans une dynamique internationale maîtrisée afin de déboucher sur la production d’un système opérationnel et interopérable, adapté aux contraintes actuelles de déploiement des forces et en particulier aux missions multinationales. C’est à ce prix que la surveillance en temps réel pourra participer activement en tous temps et en tous lieux à la préservation de la capacité opérationnelle des forces armées.

La consommation énergétique augmente dans les technologies informatiques, notamment à cause de l'augmentation de l'utilisation des services web et distribuée, l'informatique dans les nuages, ou les appareils mobiles. Par conséquent, des approches de gestion de l'énergie ont été développées, de l'optimisation du code des logiciels, à des stratégies d'adaptation basées sur l'utilisation des ressources matérielles. Afin de répondre à ces lacunes, nous présentons dans cette thèse, des modèles énergétiques, approches et outils pour estimer fidèlement la consommation énergétique des logiciels, au niveau de l'application, et au niveau du code, et pour inférer le modèle d'évolution énergétique des méthodes basé sur leurs paramètres d'entrées. Nous proposons aussi Jalen et Jalen Unit, des frameworks énergétiques pour estimer la consommation énergétique de chaque portion de code de l'application, et pour inférer le modèle d'évolution énergétique des méthodes en se basant sur des études et expériences empiriques. En utilisant des modèles énergétiques et d’outils d'estimations logicielles, nous pouvons proposer des informations énergétiques précises sans avoir besoin de wattmètres ou d'investissement de matériels de mesures énergétiques. Les informations énergétiques que nous proposons, offrent aussi aux approches de gestion énergétique des mesures directes et précises pour leurs approches d'adaptations et d'optimisations énergétiques. Ces informations énergétiques établissent aussi un modèle d'évolution énergétique des logiciels en se basant sur leurs paramètres d'entrées. Cela offre aux développeurs une connaissance plus profonde sur l'efficacité énergétique dans les logiciels<br>With the rise of the usage of computers and mobile devices, and the higher price of electricity, energy management of software has become a necessity for sustainable software, devices and IT services. Energy consumption in IT is rising through the rise of web and distributed services, cloud computing, or mobile devices. However, these approaches do not use proper energy information for their adaptations rendering themselves limited and not energy-aware. They do not provide an energy feedback of software, and limited information is available on how and where energy is spend in software code. To address these shortcomings, we present, in this thesis, energy models, approaches and tools in order to accurately estimate the energy consumption of software at the application level, at the code level, and for inferring energy evolution models based on the method's own input parameters. We also propose Jalen and Jalen Unit, energy frameworks for estimating how much energy each portion of code consumes, and for inferring energy evolution models based on empirical benchmarking of software methods. By using software estimations and energy models, we are able to provide accurate energy information without the need of power meters or hardware energy investment. The energy information we provide also gives energy management approaches direct and accurate energy measurements for their adaptations and optimizations. Provided energy information also draws a model of energy consumption evolution of software based on the values of their input parameters. This gives developers knowledge on energy efficiency in software leading to choose some code over others based on their energy performance

Les schémas de récursion modélisent les programmes fonctionnels dans le sens qu'il décrivent les définitions récursives des fonctions créées par l'utilisateur sans interpréter les fonctions de base du langage. La sémantique d'un schémas est donc l'arbre potentiellement infini décrivant les exécutions d'un programme. Cette thèse s'intéresse à des problèmes de vérification. Le problème de décider si un schémas satisfait une formule de la logique monadique du second-ordre (MSO), a été résolu par Ong en 2006. En 2010, Broadbent, Carayol, Ong et Serre ont étendu ce résultat en montrant que l'on peut transformer un schémas de telle sorte que les noeuds de l'arbre associé satisfaisant une formule MSO donnée sont marqués, ce problème est appelé le problème de réflexion. Finalement, en 2012 Carayol et Serre ont résolu le problème de sélection : si l'arbre associé à un schéma donné satisfait une formule de la forme « il existe un ensemble de noeuds tels que. . . », alors on peut transformer le schéma tel qu'un ensemble témoin de la propriété est marqué dans l'arbre associé. Dans cette thèse, nous suivons une approche sémantique pour étudier des problèmes de transformation de schémas. Notre objectif est de proposer des solutions qui conservent la structure du schémas donné en entrée. Dans cette idée, nous établissons un algorithme permettant de simuler une politique d'évaluation avec une autre. Ensuite nous donnons de nouvelles preuves de la réflexion et la sélection, sans passer par les automates à pile avec effondrement, qui conservent aussi la structure du schéma donné en entrée<br>Higher-order recursion scheme model functional programs in the sense that they describe the recursive definitions of the user-defined functions of a pro-gram, without interpreting the built-in functions. Therefore the semantics of a higher-order recursion scheme is the (possibly infinite) tree of executions of a program. This thesis focus on verification related problems. The MSO model- checking problem, i. E. The problem of knowing whether the tree generated by a scheme satisfy an monadic second order logic (MSO) formula, has been solved by Ong in 2006. In 2010 Broadbent Carayol Ong and Serre extended this result by showing that one can transform a scheme such that the nodes in the tree satisfying a given MSO formula are marked, this problem is called the reflection problem. Finally in 2012 Carayol and Serre have solved the selection problem: if the tree of a given scheme satisfies a formula of the form "There exist a set of node such that. . . ", one can transforrn the scheme such that a set witnessing the property is marked. In this thesis, we use a semantics approach to study scheme-transformation related problems. Our goal is to give shape-preserving solutions to such problems, i. E. Solutions where the output scheme has the same structure as the input one. In this idea, we establish a simulation algorithm that takes a scheme G and an evaluation policy r E {0I,I0} and outputs a scheme G' such that the value tree of G' under the policy Tif= is equal to the value tree of G under Then we give new proofs of the reflection and selection, that do not involve collapsible pushdown automata, and are again shape-preserving

Cette thèse introduit une nouvelle approche a la vérification de programmes, basée sur des formules caractéristiques. La formule caractéristique d'un programme est une formule de la logique d'ordre supérieur qui décrit le comportement d'un programme d'une manière correcte et complète vis-à-vis de la sémantique. Cette formule peut être exploitée dans un assistant de preuve pour établir de manière interactive qu'un programme satisfait une spécification de correction totale exprimée dans le style de la logique de séparation. La formule caractéristique d'un programme est automatiquement générée à partir de son code source il n'est pas nécessaire d'annoter ce code par des spécifications ou des invariants de boucle vu que ces informations peuvent être fournies dans le script de preuve. Un aspect essentiel des formules caractéristiques est qu'elles sont de taille linéaire et qu'elles peuvent être affichées comme le code source qu'elles décrivent, bien qu'elles ne fassent pas référence à la syntaxe du langage de programmation. Ces formules caractéristiques sont au coeur d'un outil, dénomme CFML, qui permet de vérifier des programmes CAML à l'aide de l'assistant de preuve coq. CFML a été utilisé pour vérifier la moitie du contenu du livre de Chris Okasaki sur les structures de données purement fonctionnelles, ainsi que pour vérifier plusieurs structures de données impératives telles que les listes mutables, les tableaux creux, ou encore la structure d'union-find. CFML supporte également le raisonnement sur les fonctions impératives d'ordre supérieur, comme les fonctions en forme CPS ou les itérateurs d'ordre supérieur<br>This dissertation describes a new approach to program verification, based on characteristic formulae the characteristic formula of a program is a higher-order logic formula that describes the behavior of that program, in the sense that it is sound and complete with respect to the semantics. This formula can be exploited in an interactive theorem prover to establish that the program satisfies a specification expressed in the style of separation logic, with respect to total correctness. The characteristic formula of a program is automatically generated from its source code alone. In particular, there is no need to annotate the source code with specifications or loop invariants, as such information can be given in interactive proof scripts. One key feature of characteristic formulae is that they are of linear size and that they can be pretty-printed in a way that closely resemble the source code they describe, even though they do not refer to the syntax of the programming language Characteristic formulae serve as a basis for a tool, called CFML, that supports the verification of CAML programs using the coq proof assistant. CFML has been employed to verify about half of the content of okasaki's book on purely functional data structures, and to verify several imperative data structures such as mutable lists, sparse arrays and union-find. Cfml also supports reasoning on higher-order imperative functions, such as functions in cps form and higher-order iterators

Nous cherchons à apporter une aide à la spécification des systèmes modulaires. Nous fournissons un contexte théorique utilisant la théorie des graphes, la modélisation probabiliste et la géométrie euclidienne pour fonder nos propositions. Celles-ci sont de trois ordres : - réflexion sur ce qu'est la qualité globale de la spécification d'un système modulaire. Ces réflexions conduisent à la définition d'un indice quantifiant le niveau de qualité. - proposition d'outils graphiques représentant à la fois un modèle de structure et un modèle de communication. Ces outils se prêtent à intégration dans des environnements de spécification. - définition d'algorithmes efficaces permettant de suggérer et d'évaluer des transformations visant à améliorer la qualité de la spécification étudiée. L’ensemble est illustré par un exemple spécifiant en LDS un Benchmark de la spécification formelle.

L'arithmétique à virgule flottante est l'approche la plus utilisée pour réaliser des calculs mathématiques reposant sur les nombres réels avec un ordinateur. Cependant, elle souffre d'un défaut : chaque opération peut introduire une erreur, c'est-à-dire une différence avec le résultat que nous aurions obtenu en utilisant des réels. Bien que ces erreurs soient très faibles, elles peuvent s'accumuler et provoquer des bugs ayant parfois des conséquences graves, en particulier dans des domaines critiques comme l'aéronautique ou le nucléaire. Il est donc nécessaire de pouvoir garantir que les erreurs introduites par l'utilisation de l'arithmétique flottante ne causent pas de problème, ou, dit autrement, qu'elles soient suffisamment faibles pour que le programme se comporte comme attendu. Pour répondre à ce besoin, nous proposons une analyse statique par interprétation abstraite, reposant sur un nouveau domaine abstrait, et calculant une sur-approximation des erreurs introduites par l'arithmétique flottante. Cette analyse repose sur l'interaction, au travers d'un produit réduit, entre deux conceptions de la notion d'erreur: l'erreur absolue, intuitive et permettant de mieux comprendre le programme analysé, et l'erreur relative, plus proche du fonctionnement de l'arithmétique flottante. Notre analyse repose sur la combinaison des arithmétiques affines et d'intervalles, et dispose de capacités de raisonnements relationnels. Cette combinaison a cependant des difficultés à traiter les opérations non linéaires, dont la précision impacte fortement l'évaluation des erreurs relatives. Nous proposons donc deux approches pour répondre à ce problème. La première consiste en différentes améliorations de cette combinaison, permettant d'évaluer plus précisément multiplications et divisions sans impacter significativement les performances. La seconde consiste en la définition d'une nouvelle arithmétique relationnelle, spécifiquement conçue pour représenter l'erreur relative. Par ailleurs, nous avons implémenté un prototype de notre analyse au sein de l'outil Frama-C/Eva. Les premiers résultats expérimentaux montrent l'intérêt de notre analyse par rapport à l'état de l'art<br>Floating point arithmetic is the most used approach to perform mathematical computations using real numbers with a computer. However, this approach has a default : each operation can introduce an error, that is, a difference with the result we would have obtained using real numbers. Even if those errors are very small, they can accumulate et provoke serious bugs, particularly in critical domains like aeronautics or nuclear energy production for example. Thus, we have to be able to guarantee that the errors introduced by the use of floating point arithmetic do not cause problems, in other words, that they are small enough for the program to behave as expected. To answer this need, we propose an abstract interpretation based static analysis, along with a new abstract domain, that computes an overapproximation of the errors introduced by floating point arithmetic. This analysis is based on the interaction, performed through a reduced product, between two conceptions of the concept of error : absolute error, intuitive and helpful to understand the analyzed program, and relative error, closer of floating point arithmetic functioning. Our analysis relies on the combination of affine and intervals arithmetics, and thus have relational reasoning capacities. However, this combination has difficulties dealing with non linear operations, whose precision has a huge impact on relative errors evaluations. Thus, we propose two approaches to tackle this problem. The first one consists of several improvements of this combination that help evaluating multiplications and divisions more precisely without impacting performances significantly. The second one consists of the definition of a new relational arithmetic, specifically designed to represent relative errors. Besides, we have implemented a prototype of our analysis within the Frama-C/Eva tool. The first experimental results enlighten the advantages of our analysis against state of the art tools

Les logiciels d'aide au diagnostic sont, aujourd'hui, intégrés dans la pratique quotidienne. Ils sont également des éléments clefs de la recherche médicale. Définis comme dispositifs médicaux, une évolution récente de la règlementation impose des évaluations cliniques aux fabricants. L'industrie pharmaceutique bénéficie d'une méthode éprouvée pour l'évaluation des médicaments. Elle n'est pas totalement transposable aux dispositifs médicaux, encore moins pour les logiciels. L'objectif de cette thèse est de proposer une méthodologie d'évaluation et de validation cliniques de ces dispositifs. Dans un premier temps, le cadre règlementaire et normatif est présenté ainsi que des méthodologies émanant de différents domaines. La synthèse de ces données permet la présentation d'un premier item de la méthode permettant l'évaluation clinique des performances logicielles. Afin d'aller plus loin dans l'analyse, une seconde partie de la méthode est consacrée à l'évaluation/validation de l'ergonomie logicielle, sujet sensible pour les logiciels médicaux. Enfin, et afin de rendre à ces dispositifs leur vraie place dans le parcours de soins, le dernier item propose de mettre en évidence leur intérêt dans la pratique clinique, ainsi que dans la prise en charge du patient, via leur implication dans la recherche de nouveaux biomarqueurs en imagerie. Ces différentes méthodes respectent et dépassent le cadre règlementaire afin de répondre aux attentes de tous les acteurs du cycle de vie des logiciels d'aide au diagnostic en imagerie. Un exemple d'application est finalement présenté via la démonstration de l'impact d'un logiciel dédié sur l'évaluation de la réponse oncologique en imagerie<br>Aided-diagnosis software in imaging are now integrated to radiological workflow but they are also key elements in medical research. Defined as medical devices, recent regulatory changes now impose clinical evaluations on manufacturers. The pharmaceutical industry benefits from a proven method in drug evaluation. Yet, transposition to medical devices is not fully effective and even more complex in the case of software. The aim of this thesis is to propose a clinical evaluation and validation methodology for these devices. The first part introduces the normative and regulatory framework as well as methodologies from various areas. The synthesis of these data allows the presentation of the first methodology item enabling the clinical evaluation of software performance. In order to further the analysis, the second part of the methodology is dedicated to evaluation/validation of software ergonomics, a sensitive issue in medical software. Finally, to restore these devices to their true place in health care, the last item proposes to highlight their impact in clinical practice and in patient management, through their implication in the search for new biomarkers in imaging. These various methods comply with and go beyond the regulatory framework in order to meet the expectations of all the stakeholders involved in the life cycle of aided-diagnosis software in imaging. To conclude, an example of its application is presented showing the impact of a dedicated software in the evaluation of oncology response in imaging

De multiples algorithmes ont été proposés pour traiter de l’ordonnancement de tâchestemps réel dans un contexte multiprocesseur. Encore très récemment de nouvelles politiquesont été définies. Ainsi, sans garantie d’exhaustivité, nous en avons recensé plusd’une cinquantaine. Cette grande diversité rend difficile une analyse comparée de leurscomportements et performances. L’objectif de ce travail de thèse est de permettre l’étudeet l’évaluation des principales politiques d’ordonnancement existantes. La première contributionest SimSo, un nouvel outil de simulation dédié à l’évaluation des politiques. Grâceà cet outil, nous avons pu comparer les performances d’une vingtaine d’algorithmes. Laseconde contribution est la prise en compte, dans la simulation, des surcoûts temporelsliés à l’exécution du code de l’ordonnanceur et à l’influence des mémoires caches sur la duréed’exécution des travaux par l’introduction de modèles statistiques évaluant les échecsd’accès à ces mémoires<br>Numerous algorithms have been proposed to address the scheduling of real-time tasksfor multiprocessor architectures. Yet, new scheduling algorithms have been defined veryrecently. Therefore, and without any guarantee of completeness, we have identified morethan fifty of them. This large diversity makes the comparison of their behavior and performancedifficult. This research aims at allowing the study and the evaluation of keyscheduling algorithms. The first contribution is SimSo, a new simulation tool dedicatedto the evaluation of scheduling algorithms. Using this tool, we were able to compare theperformance of twenty algorithms. The second contribution is the consideration, in the simulation,of temporal overheads related to the execution of the scheduler and the impactof memory caches on the computation time of the jobs. This is done by the introductionof statistical models evaluating the cache miss ratios

Les objectifs de ce travail sont donc, dans un premier temps, de mieux comprendre les effets de l’espacement initial sur les caractéristiques des arbres de pin gris et d’épinette blanche ainsi que sur les propriétés mécaniques de leur bois. Il sera également possible de développer un facteur de correction du volume des sciages obtenus en fonction des déformations naturelles présentes sur les tiges pour ces deux essences, et ce, dans le but d’estimer de manière plus précise le volume de sciage disponible à partir des données d’inventaires forestiers. Dans un deuxième temps, le travail consiste à modéliser la présence des nœuds et à percevoir leurs impacts sur le rendement en sciage à l’aide d’Optitek, un logiciel de simulation du procédé du sciage. Pour réaliser cette étape, un certain nombre de billes ont été traitées dans un CT Scanner et un nouveau logiciel a été mis au point afin d’extraire l’information désirée des images tomodensitométriques (CT) pour ensuite la rendre compatible au logiciel Optitek. Le but de cette étape est d’être en mesure d’effectuer des simulations du procédé de débitage en tenant compte de la dimension et de l’emplacement des nœuds de façon à maximiser la valeur de chaque bille. Les arbres proviennent d’une plantation d’épinette blanche (Picea glauca (Moench) Voss) et de pin gris (Pinus banksiana Lamb.) de type Nelder (1962). Ce type de plantation se caractérise par une forme circulaire qui fait en sorte que la densité de peuplement diminue graduellement du centre vers la périphérie du cercle. Ce site a permis l’étude de deux essences différentes ayant grandi dans des conditions de croissance similaires. Premièrement, les résultats démontrent que les caractéristiques des arbres sont fortement influencées par la densité de peuplement. En effet, le DHP, la hauteur totale, le défilement, la longueur et la largeur de la cime vivante, le diamètre des cinq plus grosses branches mortes et vivantes ont généralement augmenté avec l’accroissement de la distance entre les arbres, autant chez le pin gris que chez l’épinette blanche. L’optimisation du débitage primaire en fonction de l’emplacement spatial réel des nœuds internes dans les arbres a généré un volume de sciage significativement plus élevé et de plus grande valeur que les simulations du débitage uniquement basées sur la géométrie des tiges. En effet, la prise en compte de la distribution des nœuds lors des simulations du sciage a permis d’augmenter le nombre de pièces de qualité No.2 &amp; meilleur produites de 15% pour l’épinette blanche et de 40% pour le pin gris. L’augmentation de la valeur des sciages associée à la connaissance de la distribution interne des nœuds a varié de 9,5% à 15,1% pour l’épinette blanche et de 15,2% à 23,0% pour le pin gris. Encore une fois, l’augmentation du rendement en valeur a été plus forte chez le pin gris que chez l’épinette blanche en raison de la présence de nœuds de plus fortes dimensions qui augmentent le potentiel d’optimisation.<br>The first objective of this work is to characterize the properties of jack pine and white spruce and develop a lumber volume correction factor due to stem shape for both species. The purpose of this section is to more precisely predict lumber volume from forest inventory data. The second objective is to model the presence of knots and evaluate their impact on lumber yield using Optitek, a sawing simulation software. To achieve this goal, a new software had to be developed in order to extract CT image information and make it compatible with the Optitek software. Hence, the second objective is simulate lumber sawing while taking into account the knot dimension and location. The trees come from a Nelder (1962) type plantation of white spruce (Picea glauca (Moench) Voss) and jack pine (Pinus banksiana Lamb.). This type of plantation is characterized by a circular shape which makes the stand density vary from the center to the periphery of the circle. This site makes possible the study of two different species growing in similar conditions. Several field data were analyzed such as diameter at breast height (DBH), curvature, taper, total tree length, live crown size. First, the results show that tree characteristics are strongly influenced by the stand density. Indeed, DBH, total height, taper, length and width of the live crown, diameter of the five largest branches dead and alive generally increased with greater distance between the trees, both for jack pine and white spruce. The results obtained with the simulation using the knot information gave a lumber sawing volume and value significantly higher. Both jack pine and white spruce have produced more No.2 &amp; better pieces when knots have been considered in the sawing simulations (15% for white spruce and 40% for jack pine). As for lumber value, the increase varied from 9.5% to 15.1% for white spruce and 15.2% to 23.0% for jack pine. Again, the larger jack pine knot size could explain this greater potential for improvement.

La complexité de plus en plus croissante des applications distribuées et embarquées innovantes implique de spécifier, de concevoir et de développer des architectures logicielles capables de réagir aux événements et d'exécuter des changements architecturaux de façon autonome. Le processus d’adaptation pour reconfigurer une architecture doit d’une part, utiliser un certain nombre de techniques, qui peuvent être fortement spécialisées et d’autre part, assurer que les propriétés de qualité de l'architecture sont maintenues. Dans notre thèse, l’idée novatrice consiste à introduire des composants intelligents particuliers ou agents dans une plate-forme de contrôle de l’architecture d’un logiciel. Ces agents, de manière autonome, surveillent l'architecture, exécutent la reconfiguration et l'adaptent aux changements structurels du contexte de l’application. Cette plate-forme contrôle les différents composants et connecteurs de l’architecture et peut ainsi la reconfigurer, l’adapter et la faire évoluer à partir de stratégies spécifiques prés sauvegardés dans la base de connaissances de la plate-forme<br>A dynamic change to architecture is an active area of research within the software architecture community. The objective of all architecture reconfiguration, adaptation and evolution is the improvement of the quality attributes of the software architecture. Only recently the reconfiguration of software architecture at runtime has grown up considerably for the construction of reliable evolutionary systems. The structure of these systems is dynamic and continuously changing. Consequently, architectures must have the ability to react to events and perform architectural changes autonomously. In this thesis, we provide a new approach based on software multi-agent platform. Such agents are used to supervise the architecture, gather information from it and its environment, capture dynamic changes, and manage them. They monitor the components dynamically and adapt them to structural changes in the architecture. They evaluate dynamically the quality attributes of the architecture. This evaluation will ensure the correctness, robustness, security, availability, etc. As the changes take place so that the system conforms to its architecture and remains in conformance throughout its lifetime

Dans le cadre de cette thèse, nous nous intéressons à la vérification de systèmes réactifs critiques et temps réel développés a l'aide de langages flots de données synchrones. Plus particulièrement nous avons considéré les propriétés de sureté pour les applications réalisées dans un des deux langages, saga produit de Merlin Gerin/ses, ou lustre crée au LGI. La méthode de vérification, pour laquelle un prototype a été réalise, est l'évaluation de propriétés sur un modèle des programmes. Un langage de spécification adapte au contexte des systèmes réactifs temps réel, avec sa sémantique formelle, est défini; ce langage comprend plusieurs opérateurs temporels. Le désir d'automatiser la vérification a nécessité la définition de la sémantique formelle de saga. Plusieurs modèles pour les programmes ont alors été étudiés: les arbres des exécutions comme base d'expression commune des sémantiques, les graphes d'états et automates de contrôle pour la mise en œuvre de la vérification. L'utilisation de moyens existants de vérification, fondée sur l'évaluation de propriétés sur un modèle des programmes, a été étudiée et évaluée. Ces moyens sont relatifs a des logiques temporelles arborescentes et des mu-calculs propositionnels. Une nouvelle approche pour la spécification et la vérification de propriétés de sureté, mettant en œuvre les caractéristiques du langage lustre, est développée. Elle s'appuie sur l'utilisation de lustre lui-même comme langage de spécification et présente les avantages suivants: formalisme commun pour la programmation et la spécification, utilisation du compilateur pour la vérification, possibilité de preuves modulaires