Dissertations / Theses on the topic 'Essais (technologie) – Informatique'

Les travaux présentés s'inscrivent dans l'étude globale de la compréhension et la simulation des dégradations occasionnées par irridiation au Co-60 des composants électroniques embarqués. Un programmed'extraction de paramètres élaboré au laboratoire ainsi que l'utilisation du logiciel SPICE ont permis la simulation de l'effet de dose sur des TMOS. Simultanément, une étude expériementale des effets en dose cumulée et des effets post-irridiation a été réalisée sur des inverseurs CMOS. Elle montre l'applicabilité de la théorie linéaire dans une large gamme en débit de dose. L'utilisation de guérisons thermiques doit permettre de prédire la dégradation à long terme d'un circuit CMOS soumis aux débits de dose de l'environnement spatial.

L'intérêt des méthodes formelles est de permettre le développement rigoureux de systèmes informatiques critiques. Pour des systèmes complexes, elles peuvent être complétées par des formalismes de structuration et de modularité. Nous proposons ici une démarche pour la génération et l'évaluation de jeux de test fonctionnel à partir de spécifications formelles structurées ou modulaires. Nous nous appuyons sur un formalisme de spécification modulaire Moka-TRIO basé d'une part sur la théorie des catégories et le calcul des modèles défini par Ehrig et Mahr (qui permettent de structurer une modélisation et éventuellement d'encapsuler des données) et d'autre part sur la logique temporelle métrique TRIO (pour décrire des comportements réactifs). Des outils associés à ce formalisme permettent de définir et valider une spécification complexe. Nous montrons comment la structure d'une spécification Moka-TRIO permet de mettre en avant différents niveaux d'abstraction pour le test : unitaire, intégration, agrégat et système. Pour chacun de ces niveaux, nous décrivons un mécanisme de génération de jeux de test à partir d'une spécification complexe en s'appuyant sur la sémantique de celle-ci. Enfin, nous reprenons le cadre théorique d'évaluation défini par Bernot, Gaudel et Marre qui détermine la pertinence d'un jeu de test. En étendant la définition d'institution pour prendre en compte des catégories de cas de test, nous montrons comment nos mécanismes de génération permettent de définir des jeux pertinents. L'outil Moka-TRIO implémente les différents mécanismes de génération. L'approche a été appliquée à un système de contrôle de commandes électriques de vol.

Le test de logiciel temps réel tend à mettre en évidence des erreurs de traitement, le non respect de spécifications fonctionnelles ou de contraintes liées au code. Dans une optique « analyse de sûreté », ce test doit pouvoir être effectué indépendamment du matériel cible (dont l’acquisition n’est pas envisageable) mais doit cependant permettre d’étudier le comportement du logiciel testé en présence de défaillances simulées du matériel. Le test est utile au long des phases de développement, de validation et de maintenance d’un produit. Nous présentons ici un outil, appelé OST, qui simule l’exécution du code et le comportement de son environnement logiciel et matériel. L’exécution du test est surveillée et de nombreuses informations sont collectées automatiquement. Dans ce mémoire, nous présentons les mécanismes et objets internes qui régissent le fonctionnement de l’outil. Ensuite nous décrivons les moyens dont dispose l’utilisateur pour construire les jeux d’essais et l’environnement du logiciel sous-test. Nous définissons les moyens interactifs mis à sa disposition. Enfin la réalisation d’un prototype de l’outil est présentée ainsi que les essais d’utilisation qui ont été faits.

Nos travaux étudient la conception du test en complément de preuves : l'objectif est de définir des critères de sélection de test qui ciblent les lacunes de ces preuves. Le champ d'application proposé est la vérification d'algorithmes de tolérance aux fautes. Les preuves considérées peuvent être des démonstrations informelles, publiées dans la littérature, ou des preuves formelles inachevées. Dans le premier cas, nous définissons une méthode basée sur une reformulation du discours informel sous forme d'un arbre de preuve. L'arbre offre une représentation de l'articulation logique de la démonstration, ainsi qu'un support pour son analyse pas à pas. La faisabilité et l'efficacité du test guidé par la preuve sont évaluées expérimentalement sur deux exemples d'algorithmes incorrects : un algorithme d'ordonnancement de tâches, et un algorithme d'appartenance de groupe. Les résultats montrent que l'identification des lacunes de la preuve peut s'avérer efficace pour guider le test, sous réserve que l'analyse de l'arbre ne mette pas en évidence un manque de rigueur affectant l'ensemble de la démonstration. Dans le cas de preuves formelles, nous reprenons le principe d'un test basé sur l'arbre de preuve. L'établissement d'un lien entre les lemmes non prouvés et des sous-espaces d'entrée de test peut alors être plus problématique que précédemment. L'étude expérimentale d'un autre algorithme d'appartenance de groupe, partiellement prouvé avec le système PVS, montre néanmoins que, lorsqu'un lien est possible, cette information peut s'avérer pertinente pour guider le test
Our work studies the design of testing to supplement correctness proofs: the goal is to define test selection criteria which focus on the weak parts of the proof. The proposed field of application is the verification of fault-tolerance algorithms. The target proofs can be informal demonstrations, published in the literature, or partial formal proofs. In the first case, we define a method based on the reformulation of the informal discourse as a proof tree. This tree offers a representation of the logical structure of the demonstration, and a support for its step by step analysis. The feasibility and efficiency of proof guided testing are experimentally assessed using two examples of flawed algorithms: a task scheduling algorithm, and a group membership algorithm. The results show that identification of the weak parts of the proof can be effective to guide testing, provided that the tree analysis does not reveal a lack of rigor affecting the whole demonstration. In the case of formal proofs, we retain the principle of testing based on the proof tree. Establishing a link between unproved lemmas and subspaces of the test input domain can be more difficult than previously. Still, the experimental study of another group membership algorithm, partially proved with the PVS system, shows that, if a link can be established, this information can be relevant to guide testing

Ce memoire concerne l'etude et le developpement de techniques d'analyse de testabilite de descriptions comportementales de circuits. Ces techniques ont pour objectif de reduire le cout du processus de generation de sequences de test comportemental. Ce cout etant directement lie a la complexite des descriptions comportementales et a la complexite de la strategie de generation des sequences de test comportemental, les techniques presentees ont ete adaptees des domaines du test du logiciel et du test du materiel. Elles ont ete developpees au sein d'un environnement de testabilite comportementale nomme betie. Ce dernier contient les trois outils suivants: un outil de mesure de complexite de descriptions comportementales, un outil d'identification de fragments de descriptions a ameliorer et un outil de mesure de testabilite de descriptions comportementales

Cette etude se situe dans le cadre de la generation automatique de vecteurs de test pour circuits digitaux c. M. O. S. Elle a pour but le test de pannes realistes au niveau transistors. L'approche proposee s'appuie sur les concepts algorithmiques developpes pour les pannes de collages au niveau portes. Les techniques d'intelligence artificielle utilisees sont la hierarchie et l'apprentissage. La hierarchisation structurelle autorise la description de cellules complexes et l'injection de pannes au niveau transistors. La hierarchisation fonctionnelle permet de conserver, voire meme augmenter les vitesses traditionnelles d'execution. Enfin, les techniques d'apprentissage, basees sur le processus d'injection, etablissent un compromis espace memoire/temps de calcul favorable a leur exploitation. Elles sont de plus compatibles avec les techniques d'apprentissage existantes

Les travaux présentés dans ce mémoire ont pour objectif de définir une stratégie appropriée pour le test de logiciels critiques orientés-objet. La stratégie de test que nous préconisons s'appuie sur la complémentarité de données de test statistique et déterministe. Les entrées de test statistiques sont générées automatiquement à partir de l'information présente dans les diagrammes d'état UML; en complément, les entrées de test déterministes ciblent des points singuliers du domaine d'entrée. Cette stratégie mixte s'intègre dans un environnement commercial de modélisation (Rose RealTime) permettant ainsi la génération automatique à la fois des entrées de test statistiques et des sorties attendues. Le pouvoir d'efficacité de cette stratégie mixte est évalué par une technique d'injection de fautes logicielles, analyse de mutation. Dans ce cadre, un outil d'analyse de mutation pour programmes Java a été développé sur les bases d'une idée originale, associant analyse syntaxique et réflexivité pour l'injection de différents types de fautes (traditionnelles et orientées-objet). Ces travaux théoriques sont illustrés sur une étude de cas industrielle du domaine avionique. Les résultats expérimentaux confirment la pertinence de l'approche élaborée et montrent son efficacité prometteuse vis-à-vis de la recherche de fautes. Ces mesures d'efficacité sont complétées par une étude comparative de l'approche proposée avec une approche déterministe utilisée expérimentalement chez Rockwell-Collins.

Cette these a pour objet la conception en vue du test et le test integre de machines d'etats finis (mef) implantees sous forme de plas cmos dynamiques avec registres d'etats. L'etude est menee jusqu'a la definition d'un outil de cao pour la generation atomatique des mef self-testables. A partir du graphe de la machine a realiser, l'outil genere les masques de l'implantation physique dans la technologie choisie. Apres une presentation detaillee des differentes methodes de test des plas, une etude particuliere concernant la conception en vue du test des plas cmos dynamiques est proposee. Des modeles de fautes specifiques sont definis permettant ensuite une formalisation precise des vecteurs de test. Des modules de generation de cette sequence et d'analyse des reponses sont elabores comme partie integrante de la machine. Enfin, un outil de generation automatique est valide par differents exemples d'application

L'objet de cette these est le developpement d'une methodologie de diagnostic des pannes temporelles dans les circuits digitaux. Nous avons propose une alternative a l'utilisation de la simulation de fautes, basee sur l'analyse de chemins critiques. Les resultats obtenus ont permis de mettre en evidence la surete et la precision du processus de diagnostic

Cette these s'inscrit dans un contexte de test et de caracterisation de circuits integres. Elle propose une contribution au developpement d'un systeme d'inspection visuelle en microelectronique par le biais de la vision par ordinateur. L'auteur en decrit les outils et les methodes, et presente la morphologie mathematique en tant que technique d'analyse d'images. Cette etude porte sur la mise en uvre de methodes de reconnaissance d'un circuit integre a partir d'images de microscopie optique. Les concepts de la morphologie mathematique sont appliques a la segmentation du circuit en ses differentes composantes (niveaux de fabrication, interconnexions), puis a sa description geometrique (contours des pistes). Les algorithmes proposes contribuent a la detection de defauts de localisation et de caracterisation par comparaison a une base de connaissances a priori, et de defauts geometriques par reference a des dessins de masques de conception

Dans le domaine des circuits digitaux complexes, les concepteurs utilisent souvent les langages de description des systemes materiels (hdls) pour decrire la structure ou le comportement des circuits. Ces descriptions ne sont pas facilement manipulables par les outils de cao, dans la mesure ou ils n'explicitent pas directement les concepts de haut niveau inherents a tout hdl. Dans ce memoire, nous proposons un modele interne developpe a partir de la description comportementale hdl, qui se caracterise par la separation entre le flux de donnees et le flux de controle et par l'interaction explicite entre ces deux flux. Ces derniers sont representes respectivement par un modele de donnees et un modele de controle. Le modele de donnees est represente par un graphe et le modele de controle par un reseau de petri hierarchise, temporise et interprete. La modelisation des elements de base du modele interne utilise les concepts de demot: un environnement de modelisation hierarchise/multi-vues. La realisation informatique utilise une approche orientee objet

Worldline, une importante société d’informatique, doit améliorer la qualité de ses projets. Nous avons réalisé un audit sur plusieurs projets de l’entreprise afin d’identifier comment éviter l’échec des projets: aucune conclusion définitive n'en a été tirée. Cependant, il a mis en lumière le besoin d’améliorer l’utilisation des tests. Effectivement, tester chaque partie du code est requis pour éviter l’échec du projet. Dans l’industrie, notamment à Worldline, l’automatisation des tests a commencé dans le but de maîtriser le comportement des applications. Mais, exécuter tous les tests après un changement peut être une coûter plusieurs heures. Le retour sur le code changé est retardé et le développeur perd du temps pour découvrir les potentiels bogues. La solution généralement proposée dans la littérature consiste à réduire le nombre de tests à lancer en sélectionnant seulement ceux relatifs aux derniers changements effectués. L’approche sélectionne un jeu de tests réduit et approprié qui détectera de potentielles régressions dans l’application. Chaque approche de sélection de tests a besoin d’être étudiée dans le contexte de Worldline et adaptée en conséquence pour convenir aux habitudes des développeurs. Avant d’intégrer une telle approche, une étude a été faite pour connaître les habitudes actuelles des développeurs vis-à-vis de la sélection de tests. Grâce à cette étude, nous avons développé un outil pour les développeurs visant à effectuer la sélection des tests. Le but est aussi d’étudier l’impact de cet outil sur leur comportement. Nous espérons que cette approche de sélection de tests apportera des changements dans leur processus de développement
Worldline, a major IT company, has to increase the quality of its projects. We performed an audit of several projects of the company to identify how to avoid project failure: no final conclusion has been drawn. However, it highlighted a need to enhance testing usage. To test every piece of code is compulsory to avoid project failure. In industry and more specifically in Worldline, automation of tests has begun to ensure the proper behavior of their applications. But, ensuring the execution of all tests after a change can be a costly operation requiring several hours. Feedback on the changed code is delayed and developer has to spent time to discover the potential bugs. The solution generally proposed in literature consists in reducing the number of tests to run by selecting only the ones related to the last changes made by the developer. The approach selects a suitable and small set of tests to detect potential regression in the application behavior.These approaches need to be studied in the context of Worldline and consequently adapted to suit developers’ habits. Before integrating such an adapted test selection approach, a study of the testing behavior of the developers has been done to get their current test selection usage. Based on the study of the Worldline environment, we developed a tool for the developers aiming to perform test selection.The goal is also to study the impact of this tool on their behavior. We hope that the test selection approach that is packaged in a tool adapted to the Worldline developers will bring a change in their developmentprocess

Conformance testing is the process of checking that a system possesses a set of desired properties and behaves in accordance with some predefined requirements. In this context, passive testing techniques are used when the system under test cannot be interrupted or access to the system's interfaces is unavailable. Passive testing relies on the observation of the implementation during runtime, and the comparison of the observation with the expected behavior, defined through conformance properties. The objective of this thesis is to define a novel methodology to validate communicating protocols by passive testing. Existing approaches are derived from works with finite-state and labelled transition specifications and as such, they presume there exists a causality relation between the events observed in the implementation (the trace). When dealing with message-based protocols, such as the Session Initiation Protocol (fundamental for IMS services), such causality does not necessarily exist and furthermore, it may only be determined through data parts. Since existing techniques are optimized for dealing with control parts, they present limitations for testing based on data parts: reduced expressibility and succinctness of conformance properties, as well as problems to deal with satisfaction of properties including future conditions. In this work we present a message-based/data-centric approach for dealing with these issues. Observations in a trace are in the form of messages. Expected behavior is defined in a bottom-up fashion, starting from expected criteria that must be fulfilled by one or more messages, defined as constraints between the message data fields. Temporal relations by quantification over the criteria, e.g. a property may require that certain criteria "must be held for all messages in the trace". Our approach allows to express formulas about the future and past of the trace, allowing to define more general criteria than through control parts alone. Issues related to satisfaction of properties and declaration of conformance verdicts are also discussed here. Although observation of a behavior defined as a property is indication of conformance, lack of observation is not necessarily indicative of a fault. Several solutions to this issue have been proposed and implemented in this work. Finally, our work presents interesting perspectives, in terms of extensibility for online detection or improved expressiveness, but also since a message-based approach provides an alternative view to traditional testing techniques

Le travail presente dans cette these propose, dans un cadre utilisant la theorie des testeurs canoniques, deux aspects (complementaires): 1) une approche pour augmenter la pertinence des tests par integration des contraintes de temps physique: la necessite d'inclure les contraintes de temps dans les criteres de (test) de conformite est soutenue, et le modele de tiosm (imed input output state machine) est propose pour specifier ces contraintes. Une formalisation (du test) de conformite incluant les contraintes de temps physique, et des methodes de calcul de testeurs canoniques temporises sont proposees. Enfin, il est montre que ces contraintes permettent d'ameliorer le cout, la couverture generale des tests; 2) une methodologie formelle pour le test d'interoperabilite: la notion (de test) d'interoperabilite est formalisee, et un systeme de testeurs concurrents (stc) est propose pour l'interoperabilite. Ces testeurs generent les tests au vol, ce qui evite de calculer le graphe decrivant la communication globale des entites a tester. Il est montre que le stc est un testeur canonique d'interoperabilite. La technique de description formelle estelle est ensuite utilisee pour proposer une description operationnelle du stc. Une telle description permet ensuite d'experimenter le stc avec le simulateur veda

Les techniques de description formelle (tdf) pour la specification de systemes communicants sont utilisees pour valider et tester des implementations de ces systemes. Dans le cas de systemes constitues de modules, il est interessant de savoir evaluer la testabilite de chacun des composants a travers l'environnement de test que constitue les autres composants interconnectes. Cette these presente deux contributions principales aux approches de validation et de test dans le cadre des tdf: 1) une caracterisation operationnelle des relations de conformite, avec derivation automatique de tests de conformite; 2) une approche d'analyse de la testabilite des systemes partiellement observables et commandables. Les deux contributions sont basees sur une structure de graphe doublement etiquete: le graphe de refus. La verification automatique de conformite est basee sur un calcul de bissimulation adapte a cette structure. L'analyse de testabilite est basee sur l'ordonnancement de modeles d'implementations erronees. La definition des operateurs de composition et restriction sur les graphes de refus permet d'ameliorer l'efficacite de la recherche des limites de testabilite. Un environnement logiciel a ete developpe sous environnement unix pour (1) la verification des relations de conformite dans le cas des systemes a etats finis; 2) la generation de tests de conformite, et pour; 3) la mise en uvre de l'analyse de testabilite d'un systeme a travers un environnement

En ce début de millénaire, la prise en compte des interêts économico-financiers et l'évolution technologique semblent avoir fait des lois du marché les véritables clés de voûte de la législation sur le droit d'auteur. Tour à tour causes et conséquences du mouvement de dépersonnalisation de la propriété litteraire et artistique, les nouvelles technologies (logiciels, bases de données, numérisation des oeuvres, Internet) et la pénétration du capital financier dans le domaine de la création (accroissement du rôle des producteurs dans le PAF,transformation des producteurs de phonogrammes et de vidéogrammes en titulaires quasi exclusifs des droits sur les oeuvres ont progressivement transformé le rôle et l'importance des entreprises du secteur culturel. .
At the beginning of the millenium, the taking into account of economic and financial interest and the evolution of technology seem to have made market laws the true keystone to authors'rights legislation. .

Le développement de l'électronique dans les systèmes embarqués à application aéronautique, spatial, ou encore automobile est alimenté par des performances croissantes, une intégration poussée et des coûts attractifs, permettant aux industriels d'offrir des solutions techniques et économiques concurrentielles. Néanmoins, cette évolution rapide nécessite une remise en cause permanente des méthodes de conception des systèmes embarqués, dont on doit garantir la maîtrise du comportement dans des environnements sévères. En particulier, la maîtrise de la compatibilité électromagnétique (CEM) est un élément clé de la réussite des challenges d'intégration et d'évolution technologique. Cette étude décrit les différentes phases de modélisation de l’immunité d’un circuit intégré analogique, basée sur les informations techniques non confidentielles données par le fabricant du circuit intégré et l’extraction des modèles électriques des éléments du circuit imprimé. Notre travail apporte un cas d’étude dans le cadre d’une proposition de norme "IEC" (International Electrotechnical Commission) sous la référence IEC-62433. De plus, dans ce mémoire, nous mettons en évidence l’impact du vieillissement des composants électroniques sur les performances CEM. Différentes technologies et types de circuits intégrés sont étudiés pour apporter une analyse qualitative sur l’évolution des paramètres CEM après une certaine durée de vie. Nous proposons une méthodologie de qualification pour apprécier l’évolution des marges CEM sous la dénomination « fiabilité électromagnétique ». Cette méthode, basée sur des procédés expérimentaux et statistiques, permet de caractériser l’impact du vieillissement des composants électroniques sur les paramètres CEM. Ces travaux mettent en évidence l’intérêt d’introduire le facteur « effet du temps » dans nos modèles d’immunité afin de garantir la compatibilité électromagnétique de nos systèmes électroniques embarqués tout au long de leur profil de mission
The development of electronic embedded systems in aerospace application, spatial, or automotive is powered by increased performance, advanced integration and attractive prices, enabling manufacturers to offer technical solutions and economic competitiveness. However, this rapid evolution necessitates a questioning of permanent methods of designing embedded systems that must guarantee the control of behavior in severe environments. In particular, the control of electromagnetic compatibility "EMC" is importante of successful challenges of integration and evolution technology. This study describes the various stages of immunity modeling an analog integrated circuit, based on non-confidential technical information given by the manufacturer of the integrated circuit and models extraction of electrical printed circuit board. Our work provides a case study in the context of standard proposal "IEC" (International Electrotechnical Commission) under reference IEC-62433. Moreover, in this repport we show the impact of aging electronic components on EMC performance. Different types of technologies and integrated circuits are designed to provide a qualitative analysis on the evolution of EMC parameters after a period lifetime. We propose a methodology for qualification of the evolution of EMC margins under the name "electromagnetic reliability". This method, based on experimental methods and statistics, used to characterize the impact of the aging of electronics components on the EMC parameters. These works demonstrate the interest of introducing the factor "time effect" in our immunity models to ensure the electromagnetic compatibility of our electronics systems throughout their mission profile

De nos jours, les mémoires embarquées sont les composants les plus denses dans les "System-On-Chips" (SOCs), représentant actuellement plus que 90% de leur superficie totale. Parmi les différents types de mémoires, les SRAMs sont très largement utilisées dans la conception des SOCs, particulièrement en raison de leur haute performance et haute densité d'intégration. En revanche, les SRAMs conçues en utilisant des technologies submicroniques sont devenus les principaux contributeurs de la consommation d'énergie globale des SOCs. Par conséquent, un effort élevé est actuellement consacré à la conception des SRAMs à faible consommation. En plus, en raison de leur structure dense, les SRAMs sont devenus de plus en plus susceptibles aux défauts physiques comparativement aux autres blocs du circuit, notamment dans les technologies les plus récentes. Par conséquent, les SRAMs se posent actuellement comme le principal détracteur du rendement des SOCs, ce qui cause la nécessité de développer des solutions de test efficaces ciblant ces dispositifs.Dans cette thèse, des simulations électriques ont été réalisées pour prédire les comportements fautifs causés par des défauts réalistes affectant les blocs de circuits spécifiques aux technologies SRAM faible consommation. Selon les comportements fautifs identifiés, différents tests fonctionnels, ainsi que des solutions de tests matériels, ont été proposés pour détecter les défauts étudiés. Par ailleurs, ce travail démontre que les circuits d'écriture et lecture, couramment incorporés dans les SRAMs faible consommation, peuvent être réutilisés pour augmenter le stress dans les SRAMs lors du test, ce qui permet d'améliorer la détection des défauts affectant la mémoire
Nowadays, embedded memories are the densest components within System-On-Chips (SOCs), accounting for more than 90% of the overall SOC area. Among different types of memories, SRAMs are still widely used for realizing complex SOCs, especially because they allow high access performance, high density and fast integration in CMOS designs. On the other hand, high density SRAMs designed with deep-submicrometer technologies have become the main contributor to the overall SOC power consumption. Hence, there is an increasing need to design low-power SRAMs, which embed mechanisms to reduce their power consumption. Moreover, due to their dense structure, SRAMs are more are more prone to defects compared to other circuit blocks, especially in recent technologies. Hence, SRAMs are arising as the main SOC yield detractor, which raises the need to develop efficient test solutions targeting such devices.In this thesis, failure analysis based on electrical simulations has been exploited to predict faulty behaviors caused by realistic defects affecting circuit blocks that are specific to low-power SRAMs, such as power gating mechanisms and voltage regulation systems. Based on identified faulty behaviors, efficient March tests and low area overhead design for testability schemes have been proposed to detect studied defects. Moreover, the reuse of read and write assist circuits, which are commonly embedded in low-power SRAMs, has been evaluated as an alternative to increase stress in the SRAM during test phase and then improve the defect coverage

De Kheops à Internet, des nanotechnologies à la téléportation, les nouvelles technologies rythment la vie des hommes. Fruits de leur intelligence, outils de grands travaux, moteurs de diffusion des savoirs, elles sont cause et effet des progrès de l’humanité. Innervant les relations de travail subordonnées comme tous les compartiments de la société, elles retiennent l’attention du juriste tant elles sont susceptibles de remodeler l’organisation de l’entreprise, de provoquer l’exclusion de la communauté de travail (au moins autant que de rapprocher ceux qui la composent), de provoquer l’entremêlement des vies personnelle et professionnelle. Nul compartiment du droit des relations de travail n’échappe à la pression des nouvelles technologies : au recrutement des salariés elles peuvent donner un nouveau visage ; à la conclusion du contrat de travail elles peuvent offrir instantanéité et dématérialisation ; au temps de son exécution elles imposent normes de sécurité (pour que, de chacun, le corps soit préservé) et normes de vie (pour que, de chacun, l’âme et l’esprit demeurent hors du champ de lecture de l’employeur). Et que dire du jeu de relations collectives remodelées à coup de communications syndicales dématérialisées, de vote électronique, de réunions virtuelles d’instance de représentation du personnel ? Le paysage se transforme. Le corpus normatif, parfois, peine à suivre. Le temps des diseurs de droit n’est pas celui de la science. Mais la science ne peut aller sans que le législateur et le juge, un jour, s’en saisissent. D’intérêts contradictoires où s’entremêlent impératif d’évolution (de l’entreprise) et de protection (du salarié), il leur appartient d’assurer la conciliation
Over the centuries, from Cheops to the Internet and from nanotechnology to teleportation, new technologies have constantly been at the centre of individuals’ lives. Produced by human intelligence, they appear to be a key to innovation, a tool for the dissemination of knowledge and they enable the progress and evolution of mankind. These new technologies obviously drew lawyers’ attention as they have a direct impact on society as a whole, but also more specifically on the relationship between employers and employees. Moreover, they tend to reshape the organisation of corporations and lead to the entanglement of professional and private life. As a matter of fact, labour law is under pressure: recruitment procedures can be altered by new technologies, the conclusion of employment contracts is nowadays electronic and instantaneous, and security and privacy rules have been established (not to mention electronic trade union communications, e-voting or e-meetings for staff representative bodies). In short, the whole framework is changing. Unfortunately, lawmakers are usually overtaken by events as science and law evolve at a very different pace. However, sooner or later, legal boundaries are set. Currently, courts’ main challenge is to try to make technological progress and protection of employees compatible

Le contentieux prud'homal est le point d'entrée le plus significatif pour observer la réception judiciaire de la preuve électronique. Le pragmatisme et la lexibilité de la juridiction prud'homale offre un terrain d'étude propice à la confrontation axiologique des TIC et du droit du travail et à l'étude pratique des conséquences de l'insertion d'une telle preuve dans l'argumentation des plaideurs. La présente étude s’attache à démontrer qu’à l’invocation d’une preuve électronique, lejuge du contrat de travail offre une réponse mitigée. Il adopte en effet, un comportement paradoxal : d’un côté ; il fait preuve d’audace et prend part à la reconnaissance de la preuve électronique lors de la phase d’administration de la preuve, d’un autre côté, il adopte une position de défiance et la rendinopérante. Le bilan de la recherche est proche de la désillusion : le crédit alloué à la preuve électronique n’est pas à la hauteur de son utilité processuelle, elle mérite une approche plus ambitieuse et doit faire l’objet d’une réflexion générale et approfondie
Procedure in labour contentious matters is the most significant place to observe the judicial reception of e-proof. Pragmatism and flexibility of the elected industrial tribunal offers a field of study which is suitable to observe the axiological confrontation between ICT and labour law and to observe the practicalconsequences of the inclusion of such proof in the litigants’ argumentation. This research endeavours to demonstrate that the use of e-proof receives a mixed appreciation from the Judge of the contract of employment. Indeed, he adopts a paradoxical behaviour: on the one hand, he shows boldness and takes part in the recognition of the e-proof during the phase of producing evidence; but on the other hand, he seems to be reluctant to make use of it in an effective manner. The result of this study is disappointing when considering the credibility given to e-proof is not equal to its procedural utility; it deserves to be the subjectof a more ambitious approach and of a general and more in-depth reflexion

Les progrès des technologies de l'information et de la communication, des MEMS, des capteurs, actionneurs, etc. ont permis l’émergence de différents dispositifs biomédicaux. Ces nouveaux dispositifs, souvent embarqués, contribuent considérablement à l'amélioration du diagnostic et du traitement de certaines maladies, comme le diabète par exemple. Des dispositifs embarqués encore plus complexes sont en cours d’élaboration, leur mise en œuvre nécessite des années de recherche et beaucoup d’expérimentation. Le cœur artificiel, encore en phase de réalisation, est un exemple concret de ces systèmes complexes. La question de la fiabilité, du test de fonctionnement et de sureté de ces dispositifs reste problématique et difficile à résoudre. Plusieurs paramètres (patient, évolution de la maladie, alimentation, activité, traitement, etc.) sont en effet à prendre en compte et la conséquence d’une erreur de fonctionnement peut être catastrophique pour le patient. L'objectif de cette thèse est de développer des outils et des approches méthodologiques permettant la validation et le test au niveau système de ce type de dispositifs. Il s’agit précisément d’étudier la possibilité de modéliser et simuler d’une manière conjointe un dispositif médical ainsi que son interaction avec le corps humain, du moins la partie du corps humain concernée par le dispositif médical, afin de mesurer les performances et la qualité de services (QoS) du dispositif considéré. Pour atteindre cet objectif notre étude a porté sur plusieurs points. Nous avons d’abord mis en évidence une architecture simplifiée d’un modèle de corps humain permettant de représenter et de mieux comprendre les différents mécanismes du corps humain. Nous avons ensuite exploré un ensemble de métriques et une approche méthodologique générique permettant de qualifier la qualité de service d’un dispositif médical donné en interaction avec le corps humain. Afin de valider notre approche, nous l’avons appliquée à un dispositif destiné à la régulation du taux de sucre pour des patients atteints du diabète. La partie du corps humain concernée par cette pathologie à savoir le pancréas a été simulé par un modèle simplifié que nous avons implémenté sur un microcontrôleur. Le dispositif de régulation de l’insuline quant à lui a été simulé par un modèle informatique écrit en C. Afin de rendre les mesures de performances observées indépendantes d’un patient donné, nous avons étudiés différentes stratégies de tests sur différentes catégories de patients. Nous avons pour cette partie mis en œuvre un générateur de modèles capable de reproduire différents états physiologiques de patients diabétiques. L’analyse et l’exploitation des résultats observés peut aider les médecins à considérablement limités les essais cliniques sur des vrai patients et les focaliser uniquement sur les cas les plus pertinent
A Biomedical research seeks good reasoning for solving medical problems, based on intensive work and great debate. It often deals with beliefs or theories that can be proven, disproven or often refined after observations or experiments. The problem is how to make tests without risks for patients, including variability and uncertainty on a number of parameters (patients, evolution of disease, treatments …). Nowadays, medical treatment uses more and more embedded devices such as sensors, actuators, and controllers. Treatment depends on the availability and well-functioning of complex electronic systems, comprising thousands of lines of codes. A mathematical representation of patient or device is presented by a number of variables which are defined to represent the inputs, the outputs and a set of equations describing the interaction of these variables. The objective of this research is to develop tools and methodologies for the development of embedded systems for medical fields. The goal is to be able to model and jointly simulate the medical device as well the human body, at least the part of the body involved in the medical device, to analyze the performance and quality of service (QoS) of the interaction of the device with the human body. To achieve this goal our study focused on several points described below. After starting by defining a prototype of a new global and flexible architecture of mathematical model of human body, which is able to contain required data, we begin by proposing a new global methodology for modeling and simulation human body and medical systems, in order to better understand the best way to model and simulate these systems and for detecting performance and the quality of services of all system components. We use two techniques that help to evaluate the calculated QoS value. The first one calculates an index of severity which indicates the severity of the case studied. The second one using a normalization function that represents the simulation as a point in order to construct a new error grid and use it to evaluate the accuracy of value measured by patients. Using Keil development tools designed for ARM processors, we have declared a new framework in the objective to create a new tester model for the glucose-insulin system, and to define the basic rules for the tester which has the ability to satisfy well-established medical decision criteria. The framework begins by simulating a mathematical model of the human body, and this model was developed to operate in the closed loop of the glucose insulin. Then, the model of artificial pancreas has been implemented to control the mathematical model of human body. Finally a new tester model was created in order to analyze the performance of all the components of the glucose-insulin system.. We have used the suitability of partially observable Markov decision processes to formalize the planning of clinical management

Dans les années 90, la commission européenne a sollicité la mise au point d'un système de contrôle commande et de signalisation ferroviaire commun à tous les réseaux des états membres : le système ERTMS " European Railway Traffic Management System ". Il s'agit d'un système réparti complexe dont le déploiement complet est long et coûteux. L'objectif global consiste à diminuer les coûts de validation et de certification liés à la mise en œuvre de ce nouveau système en Europe. La problématique scientifique réside dans la modélisation formelle de la spécification afin de permettre la génération automatique des scénarios de test. Les verrous scientifiques, traités dans cette thèse, sont liés d'une part à la transformation de modèle semi-formel en modèle formel en préservant les propriétés structurelles et fonctionnelles des constituants réactifs du système réparti, et d'autre part à la couverture des tests générés automatiquement. Les constituants sont sous la forme de boîte noire. L'objectif consiste à tester ces derniers à travers la spécification ERTMS. Nous avons développé une approche de modélisation basée sur le couplage de modèles semi-formels (UML) et de modèles formels (Réseaux de Petri). Ce couplage se fait à travers une technique de transformation de modèles. Nous avons développé ensuite une méthode de génération automatique de scénarios de test de conformité à partir des modèles en réseaux de Petri. Les scénarios de test ont été considérés comme une séquence de franchissement filtrée puis réduite du réseau de Petri interprété représentant la spécification. Ces scénarios ont été exécutés sur notre plateforme de simulation ERTMS