Spelling suggestions: "subject:"embarqués"" "subject:"embarqué""
41 |
Analysis of ultrathin gate-oxide breakdown mechanisms and applications to antifuse memories fabricated in advanced CMOS processes / Contribution à l'analyse des mécanismes de claquage d’oxyde ultra mince et applications aux mémoires antifusibles en technologies avancéesDeloge, Matthieu 15 December 2011 (has links)
Les mémoires non-volatiles programmables une fois sont en plein essor dans le monde de l’électronique embarquée. La traçabilité, la configuration ou encore la réparation de systèmes sur puce avancés font partis des applications adressées par ce type de mémoire. Plus particulièrement, la technologie antifusible présente des propriétés de sécurité autorisant le stockage d’information sensible.Ce travail de thèse est orienté vers la compréhension des mécanismes de claquage d’oxydes minces sollicités pour la programmation des cellules antifusibles ainsi que l’intégration au niveau système de moyens de détections. Une première étape fut d’étudier les phénomènes de claquage de diélectrique type SiO2 et à haute permittivité sous l’application d’un fort champ ́électrique. Des techniques de mesures dédiées ont été développées afin de réaliser des caractérisations dans les conditions de programmation des mémoires antifusible sollicitant des temps au claquage inférieurs à la micro-seconde. Ces mesures ont ensuite permis l’étude statistique du claquage des diélectriques ainsi que la modélisation sous de hautes tensions ; hors des gammes étudiées traditionnellement dans le domaine de la fiabilité. Le modèle proposé permet l’optimisation des dimensions d’une cellule élémentaire en fonction d’un temps au claquage défini au préalable. Un mécanisme inattendu occasionnant un sur courant substrat a également été mis en évidence pendant la phase de programmation. L’étude de ce phénomène a été réalisée par des caractérisations électriques et des simulations afin de conclure sur l’hypothèse d’un déclenchement d’un transistor bipolaire parasite de type PNP dans la cellule antifusible. L’impact des conditions de programmation sur le courant de lecture mesuré sous une basse tension a également été analysé. Des structures de tests analogiques dédiés ont été conçues afin de contrôler l’amplitude du courant de programmation. Le contrôle du temps de programmation est quant à lui accompli par un système de détection de courant et de temporisation. Finalement, ces solutions sont validées par un démonstrateur d’une capacité de 1-kb conçu et fabriqué sur une technologie CMOS standard avancée 32nm. / Non-volatile one-time programmable memories are gaining an ever growing interest in embedded electronics. Chip ID, chip configuration or system repairing are among the numerous applications addressed by this type of semiconductor memories. In addition, the antifuse technology enables the storage of secured information with respect to cryptography or else. The thesis focuses on the understanding of ultrathin gate-oxide breakdown physics that is involved in the programming of antifuse bitcells. The integration of advanced programming and detection schemes is also tackled in this thesis. The breakdown mechanisms in the dielectric material SiO2 and high-K under a high electric field were studied. Dedicated experimental setups were needed in order to perform the characterization of antifuse bitcells under the conditions define in memory product. Typical time-to-breakdown values shorter than a micro second were identified. The latter measurements allowed the statistical study of dielectric breakdown and the modeling in a high voltage range, i.e. beyond the conventional range studied in reliability. The model presented in this PhD thesis enables the optimization of the antifuse bitcell sizes according to a targeted mean time-to- breakdown value. A particular mechanism leading to a high bulk current overshoot occuring during the programming operation was highlighted. The study of this phenomenon was achieved using electrical characterizations and simulations. The triggering of a parasitic P-N-P bipolar transistor localized in the antifuse bitcell appeared as a relevant hypothesis. The analysis of the impact of the programming conditions on the resulting read current measured under a low voltage was performed using analog test structures. The amplitude of the programming current was controlled in an augmented antifuse bitcell. The programming time is controlled by a programming detection system and a delay. Finally, these solutions are to be validated using a 1-kb demonstrator yet designed and fabricated in a logic 32-nm CMOS process.
|
42 |
Conception, réalisation de capteurs non-invasifs ambulatoires et d'exocapteurs embarqués pour l'étude et le suivi de la réactivité émotionnelle / Design and development of non-invasive, ambulatory or embedded sensors for the monitoring and the study of emotional reactivityMassot, Bertrand 12 December 2011 (has links)
Le suivi de l'état de santé et de la réactivité émotionnelle chez l'individu est au cœur de la médecine de demain ; il participe notamment au développement de nouveaux services de soins en santé tels que la médecine à domicile, la médecine mobile ou encore la médecine personnalisée. Cependant il nécessite d'une part la définition d'indicateurs adaptés à la mesure en environnement complexe, et d'autre part la conception d'exocapteurs et d'instrumentations intégrés dans l'environnement de l'individu. Les travaux de cette thèse présentent la démarche nécessaire au passage de mesures physiologiques en laboratoire à celles des conditions de la vie de tous les jours, en s'articulant autour de deux axes d'étude : Le premier axe concerne la conception et le développement d'une instrumentation ambulatoire pour la mesure de paramètres physiologiques en conditions écologiques. Le système portable EmoSense conçu pour la mesure de la fréquence cardiaque, de la résistance cutanée et de la température cutanée permet l'identification de nouveaux indicateurs de la réactivité émotionnelle à partir de mesures réalisées en situations réelles. L'expérimentation présentée sur l'objectivation du stress chez les personnes aveugles pendant leur déplacement en milieu urbain a permis la construction d'un nouvel indicateur pour l'analyse de l'activité électrodermale. Par ailleurs, cette démarche met en avant l'importance de la mise en place de plateformes ayant pour objectif de fournir un support pour l'expérimentation en conditions écologiques, telles que les Living Lab. La seconde partie des travaux est consacrée à la mesure de l'activité électrodermale (résistance électrique cutanée) pendant la conduite de véhicule. Cette mesure est basée sur la conception et le développement d'un volant instrumenté. Ce travail illustre les difficultés technologiques liées à la mesure de signaux bioélectriques par exocapteurs pour leur intégration dans l'environnement de l'individu. Nous proposons ainsi une topologie innovante de placement des électrodes dans le but d'optimiser les facteurs de disponibilité et de robustesse du signal liés à la mesure de signaux bioélectriques par exocapteurs. / Improvement in quality and efficiency of health and medicine, at home and in hospital, has become of paramount importance. The solution to this problem would require the continuous monitoring of several key patient parameters, including emotional reactivity analysis, in order to assist the development of mobile Health or personalized Health. But it often requires a new definition of commonly used indicators to adapt them for an in situ monitoring, and also the design of exo-sensors and instrumentations integrated in the environment. This PhD work contributes to the definition of the steps leading experiments from laboratory to real-life conditions: First a new ambulatory device was developed to enable the measurement of heart rate, electrodermal activity and skin temperature during in situ experiments, for the definition of new indicators of emotional reactivity. Experimenting in real-life settings has led to the definition of a novel, more pertinent parameter for the evaluation of stress in the blind when walking in urban space.These results were very encouraging for the use of such ambulatory devices for experiments under real-life conditions, such as Living Labs. The second part deals with the assessment of electrodermal activity while driving. This work is based on the design and the development of a steering wheel enabling the measurement of galvanic skin resistance. This has shown the challenges and issues of the assessment of bioelectric signals with exo-sensors for their integration in the human environment. Therefore we propose a new and innovative topology of electrodes on the steering wheel, for the optimization of the amount of available data and the quality of biolectric signals.
|
43 |
Modélisation en vue de l'intégration d'un système audio de micro puissance comprenant un haut-parleur MEMS et son amplificateur / Micro power audio system modeling in order to integrate a MEMS loudspeaker and its amplification architectureSturtzer, Eric 25 April 2013 (has links)
Ce manuscrit de thèse propose l'optimisation de l'ensemble de la chaîne de reproduction sonore dans un système embarqué. Le premier axe de recherche introduit les notions générales concernant les systèmes audio embarqués nécessaires à la bonne compréhension du contexte de la recherche. Le principe de conversion de l'ensemble de la chaine est présenté afin de comprendre les différentes étapes qui composent un système audio. Un état de l'art présente les différents types de haut-parleurs ainsi que l'électronique associé les plus couramment utilisées dans les systèmes embarqués. Le second axe de recherche propose une approche globale : une modélisation électrique du haut-parleur (tenant compte d'un nombre optimal de paramètres) permet à un électronicien de mieux appréhender les phénomènes non-linéaires du haut-parleur qui dégradent majoritairement la qualité audio. Il en résulte un modèle viable qui permet d'évaluer la non-linéarité intrinsèque du haut-parleur et d'en connaitre sa cause. Les résultats des simulations montrent que le taux de distorsion harmonique intrinsèque au haut-parleur est supérieur à celui généré par un amplificateur. Le troisième axe de recherche met en avant l'impact du contrôle du transducteur. L'objectif étant de savoir s'il existe une différence, du point de vue de la qualité audio, entre la commande asservie par une tension ou par un courant, d'un micro-haut-parleur électrodynamique. Pour ce type de transducteur et à ce niveau de la modélisation, le contrôle en tension est équivalent à contrôler directement le haut-parleur en courant. Néanmoins, une solution alternative (ne dégradant pas davantage la qualité audio du signal) pourrait être de contrôler le micro-haut-parleur en courant. Le quatrième axe de recherche propose d'adapter les spécifications des amplificateurs audio aux performances des micro-haut-parleurs. Une étude globale (énergétique) démontre qu'un des facteurs clés pour améliorer l'efficacité énergétique du côté de l'amplificateur audio est la minimalisation de la consommation statique en courant, en maximalisant le rendement à puissance nominale. Pour les autres spécifications, l'approche globale se base sur l'étude de l'impact de la spécification d'un amplificateur sur la partie acoustique. Cela nous a par exemple permis de réduire la contrainte en bruit de 300%. Le dernier axe de recherche s'articule autour d'un nouveau type de transducteur : un micro-haut-parleur en technologie MEMS. La caractérisation électroacoustique présente l'amélioration en terme de qualité audio (moins de 0,016% de taux de distorsion harmonique) et de plage de fréquence utile allant de 200 Hz à 20 kHz le tout pour un niveau sonore moyen de 80dB (10cm). La combinaison de tous les efforts présente un réel saut technologique. Enfin, la démarche globale d'optimisation de la partie électrique a été appliquée aux performances du MEMS dans la dernière section, ce qui a notamment permis de réduire la contrainte en bruit de 500%. / This thesis proposes the optimization of the whole sound reproduction chain in an embedded system. The first research axis is introduces the general concepts concerning audio systems necessary for the good understanding of the context of research. The principle of conversion of the entire chain is presented to understand the stages that make up a sound system. A state of the art presents various loudspeakers and the associated electronics most commonly used in embedded systems. The second research axis proposes a global approach: electric modeling of loudspeaker (taking into account an optimum number of parameters) that allows electronics engineer a better understanding of the nonlinear phenomena that degrade mostly audio quality in loudspeakers. It results in a sustainable model which evaluates the intrinsic non-linearity in loudspeakers and to know its cause. The simulation results show that the total harmonic distortion intrinsic to the loudspeaker is higher than that the distortion generated by an amplifier. The third research axis highlights the impact of the control of the transducer. The aim is to find out if there is a difference, in terms of audio quality, between the feedback control by voltage or current, for an electrodynamic micro-speaker. For this type of transducer and at this level of modeling, voltage control is equivalent to directly control the current of the micro-speaker. However, an alternative solution (not further degrading the signal audio quality) could be to control directly the micro-speaker by a current. The fourth research axis proposes to adapt the audio amplifiers specification to the performance of the micro-speakers. A comprehensive study of an energy point of view shows that a key factor for improving the energy efficiency of the audio amplifier is the minimization of the static power consumption and the maximization of the performance at nominal power. For other specifications, the global approach is based on the study of the impact of the specification of an amplifier on the sound pressure level. This has allowed, for example to reduce the stress in output noise voltage by a ratio of 300 %. The last research axis focuses on a new type of transducer: a micro-speaker in MEMS technology. Electroacoustic characterization shows the improvement: in terms of audio quality (less than 0.016 % total harmonic distortion) and the useful frequency range from 200 Hz to 20 kHz, the whole for an average sound level of 80 dB (10 cm). The combination of all the efforts presents a real technological leap. Finally, the overall process of optimization of the electrical part has been applied to the performance of MEMS in this last section, which has resulted, for example, in a reduction in the noise constraint of 500 %.
|
44 |
Restauration d'images par temps de brouillard et de pluie : applications aux aides à la conduiteHalmaoui, Houssam 30 November 2012 (has links) (PDF)
Les systèmes d'aide à la conduite (ADAS) ont pour objectif d'assister le conducteur et en particulier d'améliorer la sécurité routière. Pour cela, différents capteurs sont généralement embarqués dans les véhicules afin, par exemple, d'avertir le conducteur en cas de danger présent sur la route. L'utilisation de capteurs de type caméra est une solution économiquement avantageuse et de nombreux ADAS à base de caméra voient le jour. Malheureusement, les performances de tels systèmes se dégradent en présence de conditions météorologiques défavorables, notamment en présence de brouillard ou de pluie, ce qui obligerait à les désactiver temporairement par crainte de résultats erronés. Hors, c'est précisément dans ces conditions difficiles que le conducteur aurait potentiellement le plus besoin d'être assisté. Une fois les conditions météorologiques détectées et caractérisées par vision embarquée, nous proposons dans cette thèse de restaurer l'image dégradée à la sortie du capteur afin de fournir aux ADAS un signal de meilleure qualité et donc d'étendre la gamme de fonctionnement de ces systèmes. Dans l'état de l'art, il existe plusieurs approches traitant la restauration d'images, parmi lesquelles certaines sont dédiées à nos problématiques de brouillard ou de pluie, et d'autres sont plus générales : débruitage, rehaussement du contraste ou de la couleur, "inpainting"... Nous proposons dans cette thèse de combiner les deux familles d'approches. Dans le cas du brouillard notre contribution est de tirer profit de deux types d'approches (physique et signal) afin de proposer une nouvelle méthode automatique et adaptée au cas d'images routières. Nous avons évalué notre méthode à l'aide de critères ad hoc (courbes ROC, contraste visibles à 5 %, évaluation sur ADAS) appliqués sur des bases de données d'images de synthèse et réelles. Dans le cas de la pluie, une fois les gouttes présentes sur le pare-brise détectées, nous reconstituons les parties masquées de l'image à l'aide d'une méthode d'"inpainting" fondée sur les équations aux dérivées partielles. Les paramètres de la méthode ont été optimisés sur des images routières. Enfin, nous montrons qu'il est possible grâce à cette approche de construire trois types d'applications : prétraitement, traitement et assistance. Dans chaque famille, nous avons proposé et évalué une application spécifique : détection des panneaux dans le brouillard ; détection de l'espace navigable dans le brouillard ; affichage de l'image restaurée au conducteur.
|
45 |
Résonateur à ondes élastiques de volume à harmoniques élevés (HBARs) pour mesures gravimétriques : application à la détection de gazRabus, David 18 December 2013 (has links) (PDF)
Le besoin d'appareils compacts et autonomes dédiés à la détection d'espèces chimiques pour des analyses de terrain est d'actualité dans un contexte international en rapide mutation (agroalimentaire, développement durable, sécurité, etc.). La thèse présentée au sein de ce manuscrit, financée par la Délégation Générale de l'Armement, développe de nouvelles solutions de capteurs résonants à ondes élastiques de volume à modes harmoniques élevés (HBARs) pour la détection de gaz et plus particulièrement de composés explosifs. Ces résonateurs de très haute compacité se composent d'un transducteur reporté ou déposé sur une cavité résonante multimode, produisant un spectre de raies modulant sa propre réponse fréquentielle. De nature dipolaire, ces résonateurs permettent toutefois la mise au point de quadripôles par couplage latéral de modes mis à profit dans nos travaux. L'étude théorique du comportement de résonateurs à base de niobate de lithium aminci et reporté sur quartz ou fondés sur un empilement de nitrure d'aluminium et de silicium a permis de déterminer les propriétés gravimétriques spécifiques de chaque combinaison de matériaux et des modes associés. Des méthodes de calibrage en phase liquide et gazeuse sont proposées pour valider l'analyse théorique et permettre le choix de la structure la mieux adaptée à une configuration expérimentale donnée. Les résultats obtenus, comparés à ceux d'une microbalance à ondes guidées sur quartz, mettent en évidence les forces (compacité, cinétique chimique réduite, nature multi-physique des mesures) et faiblesses (sensibilité gravimétrique imposant des structures d'épaisseur inférieure à 100 μm) de notre solution face à cette référence. Nous avons également développé une électronique de traitement en boucle ouverte des informations issues de nos dispositifs, permettant des modes de détection rapide ou de haute précision (quelques milli-degrés de variation de phase). L'électronique dédiée a pour vocation de fournir la flexibilité nécessire au suivi de nombreux modes à diverses fréquences fixes et de s'affranchir des temps longs de balayage en fréquence des analyseurs de réseaux généralistes. Une version à 8 voies permet enfin la manipulation de plusieurs capteurs ou l'étude en parallèle des modes de 2 HBARs, donnant ainsi lieu à un système multi-physique efficace associé à des capteurs capables de sonder plusieurs grandeurs dans un volume de très petite dimension (quelques mm3 ).La limite de détection est déterminée par le bruit de phase de l'oscillateur local. Le système ainsi réalisé est exploité pour la détection de gaz mais aussi pour le pilotage de grandeurs physiques telles que la température ou la viscosité (milieux aqueux) dans différents contextes expérimentaux.
|
46 |
Localisation et transmissions sécurisées pour la communication Véhicule à Infrastructure (V2I) : Application au service de télépéage ITS-G5 / Localization and secure transmissions for Vehicle to Infrastructure communication (V2I) : Application to the electronic toll service using the ITS-G5 technologyRandriamasy, Malalatiana 24 May 2019 (has links)
La localisation précise des véhicules et la sécurité des échanges sont deux grands axes qui font la fiabilité des services fournis dans les systèmes de transport intelligent. Ces dernières années, elles font l’objet de nombreux projets de recherche pour des champs d’application divers. Dans cette thèse, le contexte d’application est la réalisation d’un service de télépéage utilisant la technologie ITS-G5. Cette technologie de communication sans-fil permet dans un premier temps le partage des informations de sécurité routière entre les véhicules (V2V), le véhicule et l’infrastructure (V2I). Dans cette thèse, on propose une architecture permettant d’échanger des transactions de télépéage utilisant les équipements communicants en ITS-G5 embarqués dans les véhicules connectés et les unités bord de route (UBR) de l’infrastructure. Les problématiques de nos travaux de recherche se concentrent sur la méthode de localisation des véhicules ayant effectué la transaction afin de pouvoir la valider et sur la sécurité de l’architecture proposée pour assurer l’échange de cette transaction. Afin de bien localiser les véhicules lors du passage au péage, notre approche propose la compréhension de la cinématique du véhicule par une modélisation adéquate à partir des données recueillies dans les messages coopératifs (CAM : Cooperative Awareness Message) en approche du péage. Cela améliorera les informations de géolocalisation déjà présentes. Notre objectif est d’arriver à une précision de moins d’un mètre pour distinguer 2 véhicules adjacents. D’autre part, le protocole de sécurité proposé permet d’assurer l’authentification des équipements participant à l’échange et à la validation de la transaction, l’intégrité des données échangées ainsi que la confidentialité des échanges compte tenu du contexte de communication sans-fil et de la sensibilité des données échangées. Une preuve de concept de la solution de télépéage utilisant la technologie ITS-G5 est développée et intègre nos deux contributions. / The precise localization of vehicles and the security of communication are requirements that make almost of the services provided in intelligent transport systems (ITS) more reliable. In recent years, they have been the subject of numerous research projects for various fields of application. In this thesis, the context is the development of an electronic toll service using the ITS-G5 technology. This wireless communication technology initially allows the sharing of traffic safety information between vehicles (V2V), vehicle and infrastructure (V2I). In our work, we propose a tolling application using equipment operating in ITS-G5 embedded in the connected vehicles and roadside units. For this, ensuring both precise geolocation of the vehicles and security of communication are required to validate the transaction.In order to properly locate the vehicles during the toll crossing, our approach is based on the understanding of the kinematics of the vehicle through a suitable modeling from the data collected in the cooperative messages (called CAM: Cooperative Awareness Message). This approach aims to improve the geolocation information already present in the message. Our goal is to achieve vehicle localization with an accuracy lower than one meter to distinguish two adjacent vehicles. On the other hand, the proposed tolling protocol ensures the authentication of the equipment or entities involved in the exchange and the validation of the transaction, the integrity of the transmitted data as well as the confidentiality of the communication. In this way, we take into account the context of the wireless communication and the sensitivity of the exchanged data. Our two contributions are integrated in the implemented Proof of Concept of the tolling application using the ITS-G5 technology.
|
47 |
Using Event-Based and Rule-Based Paradigms to Develop Context-Aware Reactive Applications / Programmation événementielle et programmation à base de règles pour le développement d'applications réactives sensibles au contexteLe, Truong Giang 30 September 2013 (has links)
Les applications réactives et sensibles au contexte sont des applications intelligentes qui observent l’environnement (ou contexte) dans lequel elles s’exécutent et qui adaptent, si nécessaire, leur comportement en cas de changements dans ce contexte, ou afin de satisfaire les besoins ou d'anticiper les intentions des utilisateurs. La recherche dans ce domaine suscite un intérêt considérable tant de la part des académiques que des industriels. Les domaines d'applications sont nombreux: robots industriels qui peuvent détecter les changements dans l'environnement de travail de l'usine pour adapter leurs opérations; systèmes de contrôle automobiles pour observer d'autres véhicules, détecter les obstacles, ou surveiller le niveau d'essence ou de la qualité de l'air afin d'avertir les conducteurs en cas d'urgence; systèmes embarqués monitorant la puissance énergétique disponible et modifiant la consommation en conséquence. Dans la pratique, le succès de la mise en œuvre et du déploiement de systèmes sensibles au contexte dépend principalement du mécanisme de reconnaissance et de réaction aux variations de l'environnement. En d'autres termes, il est nécessaire d'avoir une approche adaptative bien définie et efficace de sorte que le comportement des systèmes peut être modifié dynamiquement à l'exécution. En outre, la concurrence devrait être exploitée pour améliorer les performances et la réactivité des systèmes. Tous ces exigences, ainsi que les besoins en sécurité et fiabilité constituent un grand défi pour les développeurs.C’est pour permettre une écriture plus intuitive et directe d'applications réactives et sensibles au contexte que nous avons développé dans cette thèse un nouveau langage appelé INI. Pour observer les changements dans le contexte et y réagir, INI s’appuie sur deux paradigmes : la programmation événementielle et la programmation à base de règles. Événements et règles peuvent être définis en INI de manière indépendante ou en combinaison. En outre, les événements peuvent être reconfigurésdynamiquement au cours de l’exécution. Un autre avantage d’INI est qu’il supporte laconcurrence afin de gérer plusieurs tâches en parallèle et ainsi améliorer les performances et la réactivité des programmes. Nous avons utilisé INI dans deux études de cas : une passerelle M2M multimédia et un programme de suivi d’objet pour le robot humanoïde Nao. Enfin, afin d’augmenter la fiabilité des programmes écrits en INI, un système de typage fort a été développé, et la sémantique opérationnelle d’INI a été entièrement définie. Nous avons en outre développé un outil appelé INICheck qui permet de convertir automatiquement un sous-ensemble d’INI vers Promela pour permettre un analyse par model checking à l’aide de l’interpréteur SPIN. / Context-aware pervasive computing has attracted a significant research interest from both academy and industry worldwide. It covers a broad range of applications that support many manufacturing and daily life activities. For instance, industrial robots detect the changes of the working environment in the factory to adapt their operations to the requirements. Automotive control systems may observe other vehicles, detect obstacles, and monitor the essence level or the air quality in order to warn the drivers in case of emergency. Another example is power-aware embedded systems that need to work based on current power/energy availability since power consumption is an important issue. Those kinds of systems can also be considered as smart applications. In practice, successful implementation and deployment of context-aware systems depend on the mechanism to recognize and react to variabilities happening in the environment. In other words, we need a well-defined and efficient adaptation approach so that the systems' behavior can be dynamically customized at runtime. Moreover, concurrency should be exploited to improve the performance and responsiveness of the systems. All those requirements, along with the need for safety, dependability, and reliability pose a big challenge for developers.In this thesis, we propose a novel programming language called INI, which supports both event-based and rule-based programming paradigms and is suitable for building concurrent and context-aware reactive applications. In our language, both events and rules can be defined explicitly, in a stand-alone way or in combination. Events in INI run in parallel (synchronously or asynchronously) in order to handle multiple tasks concurrently and may trigger the actions defined in rules. Besides, events can interact with the execution environment to adjust their behavior if necessary and respond to unpredictable changes. We apply INI in both academic and industrial case studies, namely an object tracking program running on the humanoid robot Nao and a M2M gateway. This demonstrates the soundness of our approach as well as INI's capabilities for constructing context-aware systems. Additionally, since context-aware programs are wide applicable and more complex than regular ones, this poses a higher demand for quality assurance with those kinds of applications. Therefore, we formalize several aspects of INI, including its type system and operational semantics. Furthermore, we develop a tool called INICheck, which can convert a significant subset of INI to Promela, the input modeling language of the model checker SPIN. Hence, SPIN can be applied to verify properties or constraints that need to be satisfied by INI programs. Our tool allows the programmers to have insurance on their code and its behavior.
|
Page generated in 0.0472 seconds