Timing verification in transaction modeling

Les systèmes Matériels/Logiciels deviennent indispensables dans tous les aspects de la vie quotidienne. La présence croissante de ces systèmes dans les différents produits et services incite à trouver des méthodes pour les développer efficacement. Mais une conception efficace de ces systèmes est limitée par plusieurs facteurs, certains d'entre eux sont: la complexité croissante des applications, une augmentation de la densité d'intégration, la nature hétérogène des produits et services, la diminution de temps d’accès au marché. Une modélisation transactionnelle (TLM) est considérée comme un paradigme prometteur permettant de gérer la complexité de conception et fournissant des moyens d’exploration et de validation d'alternatives de conception à des niveaux d’abstraction élevés. Cette recherche propose une méthodologie d’expression de temps dans TLM basée sur une analyse de contraintes temporelles. Nous proposons d'utiliser une combinaison de deux paradigmes de développement pour accélérer la conception: le TLM d'une part et une méthodologie d’expression de temps entre différentes transactions d’autre part. Cette synergie nous permet de combiner dans un seul environnement des méthodes de simulation performantes et des méthodes analytiques formelles. Nous avons proposé un nouvel algorithme de vérification temporelle basé sur la procédure de linéarisation des contraintes de type min/max et une technique d'optimisation afin d'améliorer l'efficacité de l'algorithme. Nous avons complété la description mathématique de tous les types de contraintes présentées dans la littérature. Nous avons développé des méthodes d'exploration et raffinement de système de communication qui nous a permis d'utiliser les algorithmes de vérification temporelle à différents niveaux TLM. Comme il existe plusieurs définitions du TLM, dans le cadre de notre recherche, nous avons défini une méthodologie de spécification et simulation pour des systèmes Matériel/Logiciel basée sur le paradigme de TLM. Dans cette méthodologie plusieurs concepts de modélisation peuvent être considérés séparément. Basée sur l'utilisation des technologies modernes de génie logiciel telles que XML, XSLT, XSD, la programmation orientée objet et plusieurs autres fournies par l’environnement .Net, la méthodologie proposée présente une approche qui rend possible une réutilisation des modèles intermédiaires afin de faire face à la contrainte de temps d’accès au marché. Elle fournit une approche générale dans la modélisation du système qui sépare les différents aspects de conception tels que des modèles de calculs utilisés pour décrire le système à des niveaux d’abstraction multiples. En conséquence, dans le modèle du système nous pouvons clairement identifier la fonctionnalité du système sans les détails reliés aux plateformes de développement et ceci mènera à améliorer la "portabilité" du modèle d'application.

Studies on the exaggerated inflammatory response caused by streptococcus suis at systemic and central nervous system levels

Streptococcus suis de type 2 est un microorganisme pathogène d’importance chez le porc. Il est la cause de différentes pathologies ayant comme caractéristique commune la méningite. C’est également un agent émergeant de zoonose : des cas cliniques humains ont récemment été rapportés en Asie. Cependant, la pathogénèse de S. suis n’est pas encore complètement élucidée. Jusqu’à présent, la réponse pro-inflammatoire initiée par S. suis n’a été étudiée qu’in vitro. L’étude du choc septique et de la méningite requiert toujours des modèles expérimentaux appropriés. Au cours de cette étude, nous avons développé un modèle in vivo d’infection chez la souris qui utilise la voie d’inoculation intra-péritonéale. Ce modèle a servi à l’étude de la réponse pro-inflammatoire associée à ce pathogène, tant au niveau systémique qu’au niveau du système nerveux central (SNC). Il nous a également permis de déterminer si la sensibilité aux infections à S. suis pouvait être influencée par des prédispositions génétiques de l’hôte. Le modèle d’infection par S. suis a été mis au point sur des souris de lignée CD1. Les résultats ont démontré une bactériémie élevée pendant les trois jours suivant l’infection. Celle-ci était accompagnée d’une libération rapide et importante de différentes cytokines pro-inflammatoires (TNF-α, IL-6, IL-12p40/p70, IFN-ɣ) et de chémokines (KC, MCP-1 and RANTES), qui ont entraîné un choc septique et la mort de 20 % des animaux. Ensuite, pour confirmer le rôle de l’inflammation sur la mortalité et pour déterminer si les caractéristiques génétiques de l’hôte pouvaient influencer la réponse inflammatoire et l’issue de la maladie, le modèle d’infection a été étendu à deux lignées murines consanguines différentes considérées comme résistante : la lignée C57BL/6 (B6), et sensible : la lignée A/J. Les résultats ont démontré une importante différence de sensibilité entre les souris A/J et les souris B6, avec un taux de mortalité atteignant 100 % à 20 h post-infection (p.i.) pour la première lignée et de seulement 16 % à 36 h p.i. pour la seconde. La quantité de bactéries dans le sang et dans les organes internes était similaire pour les deux lignées. Donc, tout comme dans la lignée CD1, la bactériémie ne semblait pas être liée à la mort des souris. La différence entre les taux de mortalité a été attribuée à un choc septique non contrôlé chez les souris A/J infectées par S. suis. Les souris A/J présentaient des taux exceptionnellement élevés de TNF-α, IL-12p40/p70, IL-1β and IFN- γ, significativement supérieurs à ceux retrouvés dans la lignée B6. Par contre, les niveaux de chémokines étaient similaires entre les lignées, ce qui suggère que leur influence est limitée dans le développement du choc septique dû à S. suis. Les souris B6 avaient une production plus élevée d’IL-10, une cytokine anti-inflammatoire, ce qui suppose que la cascade cytokinaire pro-inflammatoire était mieux contrôlée, entraînant un meilleur taux de survie. Le rôle bénéfique potentiel de l’IL-10 chez les souris infectées par S. suis a été confirmé par deux approches : d’une part en bloquant chez les souris B6 le récepteur cellulaire à l’IL-10 (IL-10R) par un anticorps monoclonal anti-IL-10R de souris et d’autre part en complémentant les souris A/J avec de l’IL-10 de souris recombinante. Les souris B6 ayant reçu le anticorps monoclonal anti-IL-10R avant d’être infectées par S. suis ont développé des signes cliniques aigus similaires à ceux observés chez les souris A/J, avec une mortalité rapide et élevée et des taux de TNF-α plus élevés que les souris infectées non traitées. Chez les souris A/J infectées par S. suis, le traitement avec l’IL-10 de souris recombinante a significativement retardé l’apparition du choc septique. Ces résultats montrent que la survie au choc septique dû à S. suis implique un contrôle très précis des mécanismes pro- et anti-inflammatoires et que la réponse anti-inflammatoire doit être activée simultanément ou très rapidement après le début de la réponse pro-inflammatoire. Grâce à ces expériences, nous avons donc fait un premier pas dans l’identification de gènes associés à la résistance envers S. suis chez l’hôte. Une des réussites les plus importantes du modèle d’infection de la souris décrit dans ce projet est le fait que les souris CD1 ayant survécu à la septicémie présentaient dès 4 jours p.i. des signes cliniques neurologiques clairs et un syndrome vestibulaire relativement similaires à ceux observés lors de méningite à S. suis chez le porc et chez l’homme. L’analyse par hybridation in situ combinée à de l’immunohistochimie des cerveaux des souris CD1 infectées a montré que la réponse inflammatoire du SNC débutait avec une augmentation significative de la transcription du Toll-like receptor (TLR)2 et du CD14 dans les microvaisseaux cérébraux et dans les plexus choroïdes, ce qui suggère que S. suis pourrait se servir de ces structures comme portes d’entrée vers le cerveau. Aussi, le NF-κB (suivi par le système rapporteur de l’activation transcriptionnelle de IκBα), le TNF-α, l’IL-1β et le MCP-1 ont été activés, principalement dans des cellules identifiées comme de la microglie et dans une moindre mesure comme des astrocytes. Cette activation a également été observée dans différentes structures du cerveau, principalement le cortex cérébral, le corps calleux, l’hippocampe, les plexus choroïdes, le thalamus, l’hypothalamus et les méninges. Partout, cette réaction pro-inflammatoire était accompagnée de zones extensives d’inflammation et de nécrose, de démyélinisation sévère et de la présence d’antigènes de S. suis dans la microglie. Nous avons mené ensuite des études in vitro pour mieux comprendre l’interaction entre S. suis et la microglie. Pour cela, nous avons infecté des cellules microgliales de souris avec la souche sauvage virulente (WT) de S. suis, ainsi qu’avec deux mutants isogéniques, un pour la capsule (CPS) et un autre pour la production d’hémolysine (suilysine). Nos résultats ont montré que la capsule était un important mécanisme de résistance à la phagocytose pour S. suis et qu’elle modulait la réponse inflammatoire, en dissimulant les composants pro-inflammatoires de la paroi bactérienne. Par contre, l’absence d’hémolysine, qui est un facteur cytotoxique potentiel, n’a pas eu d’impact majeur sur l’interaction de S. suis avec la microglie. Ces études sur les cellules microgliales ont permis de confirmer les résultats obtenus précédemment in vivo. La souche WT a induit une régulation à la hausse du TLR2 ainsi que la production de plusieurs médiateurs pro-inflammatoires, dont le TNF-α et le MCP-1. S. suis a induit la translocation du NF-kB. Cet effet était plus rapide dans les cellules stimulées par le mutant déficient en CPS, ce qui suggère que les composants de la paroi cellulaire représentent de puissants inducteurs du NF-kB. De plus, la souche S. suis WT a stimulé l’expression de la phosphotyrosine, de la PKC et de différentes cascades liées à l’enzyme mitogen-activated protein kinase (MAPK). Cependant, les cellules microgliales infectées par le mutant déficient en CPS ont montré des profils de phosphorylation plus forts et plus soutenus que celles infectées par le WT. Finalement, la capsule a aussi modulé l’expression de l’oxyde nitrique synthétase inductible (iNOS) induite par S. suis et par la production subséquente d’oxyde nitrique par la microglie. Ceci pourrait être lié in vivo à la neurotoxicité et à la vasodilatation. Nous pensons que ces résultats contribueront à une meilleure compréhension des mécanismes sous-tendant l’induction de l’inflammation par S. suis, ce qui devrait permettre, d’établir éventuellement des stratégies plus efficaces de lutte contre la septicémie et la méningite. Enfin, nous pensons que ce modèle expérimental d’infection chez la souris pourra être utilisé dans l’étude de la pathogénèse d’autres bactéries ayant le SNC pour cible.

A Categorical Framework for the Specification and the Verification of Aspect Oriented Systems

Un objectif principal du génie logiciel est de pouvoir produire des logiciels complexes, de grande taille et fiables en un temps raisonnable. La technologie orientée objet (OO) a fourni de bons concepts et des techniques de modélisation et de programmation qui ont permis de développer des applications complexes tant dans le monde académique que dans le monde industriel. Cette expérience a cependant permis de découvrir les faiblesses du paradigme objet (par exemples, la dispersion de code et le problème de traçabilité). La programmation orientée aspect (OA) apporte une solution simple aux limitations de la programmation OO, telle que le problème des préoccupations transversales. Ces préoccupations transversales se traduisent par la dispersion du même code dans plusieurs modules du système ou l’emmêlement de plusieurs morceaux de code dans un même module. Cette nouvelle méthode de programmer permet d’implémenter chaque problématique indépendamment des autres, puis de les assembler selon des règles bien définies. La programmation OA promet donc une meilleure productivité, une meilleure réutilisation du code et une meilleure adaptation du code aux changements. Très vite, cette nouvelle façon de faire s’est vue s’étendre sur tout le processus de développement de logiciel en ayant pour but de préserver la modularité et la traçabilité, qui sont deux propriétés importantes des logiciels de bonne qualité. Cependant, la technologie OA présente de nombreux défis. Le raisonnement, la spécification, et la vérification des programmes OA présentent des difficultés d’autant plus que ces programmes évoluent dans le temps. Par conséquent, le raisonnement modulaire de ces programmes est requis sinon ils nécessiteraient d’être réexaminés au complet chaque fois qu’un composant est changé ou ajouté. Il est cependant bien connu dans la littérature que le raisonnement modulaire sur les programmes OA est difficile vu que les aspects appliqués changent souvent le comportement de leurs composantes de base [47]. Ces mêmes difficultés sont présentes au niveau des phases de spécification et de vérification du processus de développement des logiciels. Au meilleur de nos connaissances, la spécification modulaire et la vérification modulaire sont faiblement couvertes et constituent un champ de recherche très intéressant. De même, les interactions entre aspects est un sérieux problème dans la communauté des aspects. Pour faire face à ces problèmes, nous avons choisi d’utiliser la théorie des catégories et les techniques des spécifications algébriques. Pour apporter une solution aux problèmes ci-dessus cités, nous avons utilisé les travaux de Wiels [110] et d’autres contributions telles que celles décrites dans le livre [25]. Nous supposons que le système en développement est déjà décomposé en aspects et classes. La première contribution de notre thèse est l’extension des techniques des spécifications algébriques à la notion d’aspect. Deuxièmement, nous avons défini une logique, LA , qui est utilisée dans le corps des spécifications pour décrire le comportement de ces composantes. La troisième contribution consiste en la définition de l’opérateur de tissage qui correspond à la relation d’interconnexion entre les modules d’aspect et les modules de classe. La quatrième contribution concerne le développement d’un mécanisme de prévention qui permet de prévenir les interactions indésirables dans les systèmes orientés aspect.

In vivo phosphorus spectroscopy in human subjects on a clinical 3T MRI system

Alors que l’Imagerie par résonance magnétique (IRM) permet d’obtenir un large éventail de données anatomiques et fonctionnelles, les scanneurs cliniques sont généralement restreints à l’utilisation du proton pour leurs images et leurs applications spectroscopiques. Le phosphore jouant un rôle prépondérant dans le métabolisme énergétique, l’utilisation de cet atome en spectroscopie RM présente un énorme avantage dans l’observation du corps humain. Cela représente un certain nombre de déEis techniques à relever dus à la faible concentration de phosphore et sa fréquence de résonance différente. L’objectif de ce projet a été de développer la capacité à réaliser des expériences de spectroscopie phosphore sur un scanneur IRM clinique de 3 Tesla. Nous présentons ici les différentes étapes nécessaires à la conception et la validation d’une antenne IRM syntonisée à la fréquence du phosphore. Nous présentons aussi l’information relative à réalisation de fantômes utilisés dans les tests de validation et la calibration. Finalement, nous présentons les résultats préliminaires d’acquisitions spectroscopiques sur un muscle humain permettant d’identiEier les différents métabolites phosphorylés à haute énergie. Ces résultats s’inscrivent dans un projet de plus grande envergure où les impacts des changements du métabolisme énergétique sont étudiés en relation avec l’âge et les pathologies.

Studies on a syntax based approach for translation between structurally different languages and the development of a prototype for Malayalam to English translation

This thesis summarizes the results on the studies on a syntax based approach for translation between Malayalam, one of Dravidian languages and English and also on the development of the major modules in building a prototype machine translation system from Malayalam to English. The development of the system is a pioneering effort in Malayalam language unattempted by previous researchers. The computational models chosen for the system is first of its kind for Malayalam language. An in depth study has been carried out in the design of the computational models and data structures needed for different modules: morphological analyzer , a parser, a syntactic structure transfer module and target language sentence generator required for the prototype system. The generation of list of part of speech tags, chunk tags and the hierarchical dependencies among the chunks required for the translation process also has been done. In the development process, the major goals are: (a) accuracy of translation (b) speed and (c) space. Accuracy-wise, smart tools for handling transfer grammar and translation standards including equivalent words, expressions, phrases and styles in the target language are to be developed. The grammar should be optimized with a view to obtaining a single correct parse and hence a single translated output. Speed-wise, innovative use of corpus analysis, efficient parsing algorithm, design of efficient Data Structure and run-time frequency-based rearrangement of the grammar which substantially reduces the parsing and generation time are required. The space requirement also has to be minimised

Efficient Watermarking Schemes for Speaker Verification Guaranteeing Non-repudiation

Presently different audio watermarking methods are available; most of them inclined towards copyright protection and copy protection. This is the key motive for the notion to develop a speaker verification scheme that guar- antees non-repudiation services and the thesis is its outcome. The research presented in this thesis scrutinizes the field of audio water- marking and the outcome is a speaker verification scheme that is proficient in addressing issues allied to non-repudiation to a great extent. This work aimed in developing novel audio watermarking schemes utilizing the fun- damental ideas of Fast-Fourier Transform (FFT) or Fast Walsh-Hadamard Transform (FWHT). The Mel-Frequency Cepstral Coefficients (MFCC) the best parametric representation of the acoustic signals along with few other key acoustic characteristics is employed in crafting of new schemes. The au- dio watermark created is entirely dependent to the acoustic features, hence named as FeatureMark and is crucial in this work. In any watermarking scheme, the quality of the extracted watermark de- pends exclusively on the pre-processing action and in this work framing and windowing techniques are involved. The theme non-repudiation provides immense significance in the audio watermarking schemes proposed in this work. Modification of the signal spectrum is achieved in a variety of ways by selecting appropriate FFT/FWHT coefficients and the watermarking schemes were evaluated for imperceptibility, robustness and capacity char- acteristics. The proposed schemes are unequivocally effective in terms of maintaining the sound quality, retrieving the embedded FeatureMark and in terms of the capacity to hold the mark bits. Robust nature of these marking schemes is achieved with the help of syn- chronization codes such as Barker Code with FFT based FeatureMarking scheme and Walsh Code with FWHT based FeatureMarking scheme. An- other important feature associated with this scheme is the employment of an encryption scheme towards the preparation of its FeatureMark that scrambles the signal features that helps to keep the signal features unreve- laed. A comparative study with the existing watermarking schemes and the ex- periments to evaluate imperceptibility, robustness and capacity tests guar- antee that the proposed schemes can be baselined as efficient audio water- marking schemes. The four new digital audio watermarking algorithms in terms of their performance are remarkable thereby opening more opportu- nities for further research.

FEM based Virtual Prototyping and Design of Third Harmonic Excitation System for Low Voltage Brushless Alternators

Salient pole brushless alternators coupled to IC engines are extensively used as stand-by power supply units for meeting in- dustrial power demands. Design of such generators demands high power to weight ratio, high e ciency and low cost per KVA out- put. Moreover, the performance characteristics of such machines like voltage regulation and short circuit ratio (SCR) are critical when these machines are put into parallel operation and alterna- tors for critical applications like defence and aerospace demand very low harmonic content in the output voltage. While designing such alternators, accurate prediction of machine characteristics, including total harmonic distortion (THD) is essential to mini- mize development cost and time. Total harmonic distortion in the output voltage of alternators should be as low as possible especially when powering very sophis- ticated and critical applications. The output voltage waveform of a practical AC generator is replica of the space distribution of the ux density in the air gap and several factors such as shape of the rotor pole face, core saturation, slotting and style of coil disposition make the realization of a sinusoidal air gap ux wave impossible. These ux harmonics introduce undesirable e ects on the alternator performance like high neutral current due to triplen harmonics, voltage distortion, noise, vibration, excessive heating and also extra losses resulting in poor e ciency, which in turn necessitate de-rating of the machine especially when connected to non-linear loads. As an important control unit of brushless alternator, the excitation system and its dynamic performance has a direct impact on alternator's stability and reliability. The thesis explores design and implementation of an excitation i system utilizing third harmonic ux in the air gap of brushless al- ternators, using an additional auxiliary winding, wound for 1=3rd pole pitch, embedded into the stator slots and electrically iso- lated from the main winding. In the third harmonic excitation system, the combined e ect of two auxiliary windings, one with 2=3rd pitch and another third harmonic winding with 1=3rd pitch, are used to ensure good voltage regulation without an electronic automatic voltage regulator (AVR) and also reduces the total harmonic content in the output voltage, cost e ectively. The design of the third harmonic winding by analytic methods demands accurate calculation of third harmonic ux density in the air gap of the machine. However, precise estimation of the amplitude of third harmonic ux in the air gap of a machine by conventional design procedures is di cult due to complex geome- try of the machine and non-linear characteristics of the magnetic materials. As such, prediction of the eld parameters by conven- tional design methods is unreliable and hence virtual prototyping of the machine is done to enable accurate design of the third har- monic excitation system. In the design and development cycle of electrical machines, it is recognized that the use of analytical and experimental methods followed by expensive and in exible prototyping is time consum- ing and no longer cost e ective. Due to advancements in com- putational capabilities over recent years, nite element method (FEM) based virtual prototyping has become an attractive al- ternative to well established semi-analytical and empirical design methods as well as to the still popular trial and error approach followed by the costly and time consuming prototyping. Hence, by virtually prototyping the alternator using FEM, the important performance characteristics of the machine are predicted. Design of third harmonic excitation system is done with the help of results obtained from virtual prototype of the machine. Third harmonic excitation (THE) system is implemented in a 45 KVA ii experimental machine and experiments are conducted to validate the simulation results. Simulation and experimental results show that by utilizing third harmonic ux in the air gap of the ma- chine for excitation purposes during loaded conditions, triplen harmonic content in the output phase voltage is signi cantly re- duced. The prototype machine with third harmonic excitation system designed and developed based on FEM analysis proved to be economical due to its simplicity and has the added advan- tage of reduced harmonics in the output phase voltage.

Molekularbiologische Funktionsanalysen von Thioredoxinen aus Dictyostelium discoideum und Identifizierung neuer Interaktionspartner durch das Two-Hybrid-System

Thioredoxins are small, regulatory proteins with a mass of approximately 12 kDa and a characteristic conserved active center, which is represented in the pentapeptide trp-cys-gly-pro-cys. Up to now it is not possible to present a complete list of thioredoxin interaction partners because there is no predictable sequence in the target enzymes where thioredoxins can interact with. To get closer information about the functions and possible interaction partners of the three thioredoxins from the social soil amoeba Dictyostelium discoideum (DdTrx1 - 3) we have chosen two different strategies. In the first one the thioredoxin levels in the cell should changed by different mutants. But both the antisense technique as well as the creation of knock out mutants were not appropiate strategies in this case. Just an thioredoxin overexpressing mutant results in a developmental phenotype which allows some conclusions for possible functions of the thioredoxin in Dictyostelium discoideum. The second strategie was the two hybrid system where thioredoxin interactions partners can identified systematically. After a screening with a cDNA library from Dictyostelium 13 potential interaction partners could be detected, among them a ribonucleotid reductase, TRFA, two different cytochrome c oxidase subunits, filopodin, three ribosomal proteins, the elongationfactor 1a and the alcohol dehydrogenase from yeast. The verification of the interaction between thioredoxin and these two hybrid clones happened indirectly by a dobble mutant of thioredoxin 1, where the cysteines in the active center were replaced by redox-inactive serins. Further examinations of two choosen candidates resulted that the alcohol dehydrogenase from yeast is a thioredoxin-modululated enzym and that there is an interaction between the elongationfactor 1a and the thioredoxin 1 from Dictyostelium discoideum.

Formal Multilevel Hierarchical Verification of Synchronous MOS Circuits

I have designed and implemented a system for the multilevel verification of synchronous MOS VLSI circuits. The system, called Silica Pithecus, accepts the schematic of an MOS circuit and a specification of the circuit's intended digital behavior. Silica Pithecus determines if the circuit meets its specification. If the circuit fails to meet its specification Silica Pithecus returns to the designer the reason for the failure. Unlike earlier verifiers which modelled primitives (e.g., transistors) as unidirectional digital devices, Silica Pithecus models primitives more realistically. Transistors are modelled as bidirectional devices of varying resistances, and nodes are modelled as capacitors. Silica Pithecus operates hierarchically, interactively, and incrementally. Major contributions of this research include a formal understanding of the relationship between different behavioral descriptions (e.g., signal, boolean, and arithmetic descriptions) of the same device, and a formalization of the relationship between the structure, behavior, and context of device. Given these formal structures my methods find sufficient conditions on the inputs of circuits which guarantee the correct operation of the circuit in the desired descriptive domain. These methods are algorithmic and complete. They also handle complex phenomena such as races and charge sharing. Informal notions such as races and hazards are shown to be derivable from the correctness conditions used by my methods.

ONTIC: A Knowledge Representation System for Mathematics

Ontic is an interactive system for developing and verifying mathematics. Ontic's verification mechanism is capable of automatically finding and applying information from a library containing hundreds of mathematical facts. Starting with only the axioms of Zermelo-Fraenkel set theory, the Ontic system has been used to build a data base of definitions and lemmas leading to a proof of the Stone representation theorem for Boolean lattices. The Ontic system has been used to explore issues in knowledge representation, automated deduction, and the automatic use of large data bases.

Maygen: A Symbolic Debugger Generation System

With the development of high-level languages for new computer architectures comes the need for appropriate debugging tools as well. One method for meeting this need would be to develop, from scratch, a symbolic debugger with the introduction of each new language implementation for any given architecture. This, however, seems to require unnecessary duplication of effort among developers. This paper describes Maygen, a "debugger generation system," designed to efficiently provide the desired language-dependent and architecture-dependent debuggers. A prototype of the Maygen system has been implemented and is able to handle the semantically different languages of C and OPAL.

Development, implementation and evaluation of an activated sludge supervisory system for the Granollers WWTP

La present tesi pretén recollir l'experiència viscuda en desenvolupar un sistema supervisor intel·ligent per a la millora de la gestió de plantes depuradores d'aigües residuals., implementar-lo en planta real (EDAR Granollers) i avaluar-ne el funcionament dia a dia amb situacions típiques de la planta. Aquest sistema supervisor combina i integra eines de control clàssic de les plantes depuradores (controlador automàtic del nivell d'oxigen dissolt al reactor biològic, ús de models descriptius del procés...) amb l'aplicació d'eines del camp de la intel·ligència artificial (sistemes basats en el coneixement, concretament sistemes experts i sistemes basats en casos, i xarxes neuronals). Aquest document s'estructura en 9 capítols diferents. Hi ha una primera part introductòria on es fa una revisió de l'estat actual del control de les EDARs i s'explica el perquè de la complexitat de la gestió d'aquests processos (capítol 1). Aquest capítol introductori juntament amb el capítol 2, on es pretén explicar els antecedents d'aquesta tesi, serveixen per establir els objectius d'aquest treball (capítol 3). A continuació, el capítol 4 descriu les peculiaritats i especificitats de la planta que s'ha escollit per implementar el sistema supervisor. Els capítols 5 i 6 del present document exposen el treball fet per a desenvolupar el sistema basat en regles o sistema expert (capítol 6) i el sistema basat en casos (capítol 7). El capítol 8 descriu la integració d'aquestes dues eines de raonament en una arquitectura multi nivell distribuïda. Finalment, hi ha una darrer capítol que correspon a la avaluació (verificació i validació), en primer lloc, de cadascuna de les eines per separat i, posteriorment, del sistema global en front de situacions reals que es donin a la depuradora

Dental training system using haptic technology

In the U.K., dental students require to perform training and practice on real human tissues at the very early stage of their courses. Currently, the human tissues, such as decayed teeth, are mounted in a human head like physical model. The problems with these models in teaching are; (1) every student operates on tooth, which are always unique; (2) the process cannot be recorded for examination purposes and (3) same training are not repeatable. The aim of the PHATOM Project is to develop a dental training system using Haptic technology. This paper documents the project background, specification, research and development of the first prototype system. It also discusses the research in the visual display, haptic devices and haptic rendering. This includes stereo vision, motion parallax, volumetric modelling, surface remapping algorithms as well as analysis design of the system. A new volumetric to surface model transformation algorithm is also introduced. This paper includes the future work on the system development and research.

How well does the ECMWF Ensemble Prediction System predict blocking?

Forecasting atmospheric blocking is one of the main problems facing medium-range weather forecasters in the extratropics. The European Centre for Medium-Range Weather Forecasts (ECMWF) Ensemble Prediction System (EPS) provides an excellent basis for medium-range forecasting as it provides a number of different possible realizations of the meteorological future. This ensemble of forecasts attempts to account for uncertainties in both the initial conditions and the model formulation. Since 18 July 2000, routine output from the EPS has included the field of potential temperature on the potential vorticity (PV) D 2 PV units (PVU) surface, the dynamical tropopause. This has enabled the objective identification of blocking using an index based on the reversal of the meridional potential-temperature gradient. A year of EPS probability forecasts of Euro-Atlantic and Pacific blocking have been produced and are assessed in this paper, concentrating on the Euro-Atlantic sector. Standard verification techniques such as Brier scores, Relative Operating Characteristic (ROC) curves and reliability diagrams are used. It is shown that Euro-Atlantic sector-blocking forecasts are skilful relative to climatology out to 10 days, and are more skilful than the deterministic control forecast at all lead times. The EPS is also more skilful than a probabilistic version of this deterministic forecast, though the difference is smaller. In addition, it is shown that the onset of a sector-blocking episode is less well predicted than its decay. As the lead time increases, the probability forecasts tend towards a model climatology with slightly less blocking than is seen in the real atmosphere. This small under-forecasting bias in the blocking forecasts is possibly related to a westerly bias in the ECMWF model. Copyright © 2003 Royal Meteorological Society

Design, implementation and characterisation of a contactless power transfer system for rotating applications

This paper describes the design, implementation and characterisation of a contactless power transfer system for rotating applications. The power transfer system is based upon a zero-voltage-switched, full-bridge, DC-DC converter, but utilises a non-standard transformer. This transformer allows power transfer between its primary and secondary windings while also allowing free rotation between these windings. The aim of this research is to develop a solution that could replace mechanical slip-rings in certain applications where a non-contacting system would be advantageous. Based upon the design method presented in this paper, a 2 kW prototype system is constructed. Results obtained from testing the 2 kW prototype are presented and discussed. This discussion considers how the performance of the transformer varies with rotation and also the overall efficiency of the system