Die effiziente Präsentation von Tumorepitopen stellt einen kritischen Faktor zur Eliminierung von Tumorzellen durch die CD8+ cytotoxische T-Lymphozyten (CTL) vermittelte Immunantwort dar. Eine wichtige Rolle spielt in diesem Zusammenhang die effiziente Generierung von Tumorepitopen durch das Ubiquitin-Proteasom-System (UPS). Veränderungen von Komponenten des UPS, die an der Degradation und Prozessierung von Antigenen beteiligt sind, können daher zur Immunevasion von Tumorzellen gegenüber CTL führen. In der vorliegenden Arbeit wurden zwei unterschiedliche UPS-assoziierte Immunevasionsmechanismen des malignen Melanoms identifiziert, die auf einer ineffizienten Präsentation des immundominanten Tumorepitops Melan-A26-35 basieren. Ein Mechanismus beruht auf den unterschiedlichen katalytischen Eigenschaften von Proteasomsubtypen, deren Expression durch INFgamma induziert wird. Proteasomen, die einerseits die Immunountereinheiten beta1i und/oder beta2i beinhalten, oder anderseits mit dem Proteasomaktivator 28 (PA28) assoziiert sind, führen zu einer drastisch reduzierten Generierung des Tumorepitops Melan-A26-35. In beiden Fällen ist dies auf eine ineffiziente Prozessierung des N-Terminus des Epitops zurückzuführen. Der andere Immunevasionsmechanismus steht im Zusammenhang mit der ER-assoziierten Degradation (ERAD), die den retrograden Transport von Proteinen aus dem Endoplasmatischen Retikulum (ER) ins Cytosol zur proteasomalen Degradation beinhaltet. Durch Immunselektion mittels Melan-A26-35-spezifischen CTL wurden cytolyseresistente Melanomzellen identifiziert, deren Resistenz auf eine defiziente ER-assoziierte Degradation zurückzuführen ist. Dieser Defekt beruht auf einer verminderten Expression von ERAD-Komponenten, deren Reduktion die Verfügbarkeit des Antigens Melan-A zur proteasomalen Degradation und Generierung des immundominanten Epitops Melan-A26-35 wesentlich limitiert. / Efficient presentation of tumor epitopes by MHC class I molecules on the cell surface is a prerequisite for the elimination of tumor cells by cytotoxic CD8+ T lymphocytes. The generation of these epitopes requires the degradation and processing of proteins by the ubiquitin proteasome system (UPS). Therefore alterations of UPS components can lead to tumor escape from immune recognition as a result of decreased epitope generation. In the present thesis two different UPS connected immune escape mechanisms of melanoma cells were identified. Both are based on an impaired generation of the immunodominant epitope Melan-A26-35 derived from Melan-A/MART-1 tumor antigen. One mechanism is mediated by the expression of different INFgamma-inducible proteasome immunosubunits leading to the formation of intermediate proteasome subtypes, which differ in their cleavage site preferences. Purified proteasomes harboring the immunosubunits beta1i and/or beta2i show a dramatic decrease in the generation of the Melan-A26-35 epitope. In addition, the INFgamma induced association of proteasomes with the proteaosome activator 28 (PA28) results in a reduced epitope generation. Both mechanisms are induced by an inefficient processing of the epitope’s N-terminus. The second immune escape mechanism is caused by defects of the ER-associated degradation pathway (ERAD). ERAD mediates the transport of ER-proteins back to the cytosolic compartment for proteasomal degradation. Via immunselection of tumor cells with Melan-A26-35 specific CTL, cytolysis resistant cells were identified. Resistance to CTL mediated lysis was shown to be connected to a decreased expression of ERAD components. This defect of the ERAD pathway limits the availability of the Melan-A protein and as consequence the generation of the immunodominant Melan-A26-35 epitope by proteasomes.

La conception des systèmes de contrôle-commande souffre souvent des problèmes de communication et d’interprétation des spécifications entre les différents intervenants provenant souvent de domaines techniques très variés. Afin de cadrer la conception de ces systèmes, plusieurs démarches ont été proposées dans la littérature. Parmi elles, la démarche dite mixte (ascendante/descendante), qui voit la conception réalisée en deux phases. Dans la première phase (ascendante), un modèle du système est défini à partir d’un ensemble de composants standardisés. Ce modèle subit, dans la deuxième phase (descendante), plusieurs raffinages et transformations pour obtenir des modèles plus concrets (codes,applicatifs, etc.). Afin de garantir la qualité des systèmes conçus par cette démarche, nous proposons dans cette thèse, deux approches de vérification formelle basées sur le Model-Checking. La première approche porte sur la vérification des composants standardisés et permet la vérification d’une chaîne de contrôle-commande élémentaire complète. La deuxième approche consiste en la vérification des modèles d’architecture (P&ID) utilisés pour la génération des programmes de contrôle-commande. Cette dernière est basée sur la définition d’un style architectural en Alloy pour la norme ANSI/ISA-5.1. Pour supporter les deux approches, deux flots de vérification formelle semi-automatisés basés sur les concepts de l’IDM ont été proposés. L’intégration des méthodes formelles dans un contexte industriel est facilitée, ainsi, par la génération automatique des modèles formels à partir des modèles de conception maîtrisés par les concepteurs métiers. Nos deux approches ont été validées sur un cas industriel concret concernant un système de gestion de fluide embarqué dans un navire. / The design of control-command systems often suffers from problems of communication and interpretation of specifications between the various designers, frequently coming from a wide range of technical fields. In order to address the design of these systems, several methods have been proposed in the literature. Among them, the so-called mixed method (bottom-up/top-down), which sees the design realized in two steps. In the first step (bottom-up), a model of the system is defined from a set of standardized components. This model undergoes, in the second (top-down) step, several refinements and transformations to obtain more concrete models (codes, applications, etc.). To guarantee the quality of the systems designed according to this method, we propose two formal verification approaches,based on Model-Checking, in this thesis. The first approach concerns the verification of standardized components and allows the verification of a complete elementary control-command chain. The second one consists in verifying the model of architecture (P&ID) used for the generation of control programs.The latter is based on the definition of an architectural style in Alloy for the ANSI/ISA-5.1 standard. To support both approaches, two formal semi-automated verification flows based on Model-Driven Engineering have been proposed. This integration of formal methods in an industrial context is facilitated by the automatic generation of formal models from design models carried out by business designers. Our two approaches have been validated on a concrete industrial case of a fluid management system embedded in a ship.

O desenvolvimento de sistemas críticos é atualmente um dos problemas mais desafiadores enfrentados pela Engenharia. Há frequentemente uma pressão para se reduzir o tempo total de desenvolvimento, o que dificulta a entrega de sistemas com um mínimo aceitável de defeitos. Nos últimos anos, houve um aumento no tráfego aéreo, o que demanda uma modernização dos sistemas de tráfego aéreo atuais, muito dependentes na figura do controlador. Sistemas de tráfego aéreo são sistemas considerados críticos em segurança e de tempo real. O objetivo do presente trabalho é estabelecer um método de modelagem e verificação formal para sistemas críticos, com aplicação no domínio de tráfego aéreo. Com a adoção de técnicas de modelagem e verificação formal, pretende-se garantir a corretude dos sistemas frente aos requisitos inicialmente especificados e a detecção de erros em fases mais iniciais do projeto, o que resultaria em menores custos envolvidos na sua correção. São fornecidas diretivas para a aplicação do método através de um estudo de caso, baseado em três módulos de um sistema ATC em baixo nível de abstração, para a validação do funcionamento de módulos de software. Para verificação formal, é utilizada a ferramenta NuSMV e as propriedades a serem verificadas são descritas na lógica computacional de árvore (CTL) para garantir que o sistema satisfaça requisitos dos tipos vivacidade e segurança. / Developing safety critical systems is one of the most challenging problems in Engineering nowadays. There is usually a pressure to reduce the total time of the development, what makes it difficult to deliver systems with an acceptable low level of defects. In the recent years, there has been an increase in air trffic, what demands a modernization in the current air traffic systems, which are very dependent on the human controller. Air traffic systems are considered safety critical and real time systems. The objective of the present work is to establish a modeling and formal verification method for critical systems, applicable to the air traffic domain. By adopting modeling and formal verification techniques, it is expected to ensure the systems\' correctness compared with the initially specified requirements and the error detection in the initial phases of the project. Guidelines are provided for applying the method by means of a case study, based in three modules of and ATC system in a low abstraction level, for the validation of the operation of software modules. For the formal verification, it is used the NuSMV tool and the properties to be checked are described in the computational tree logic (CTL) to ensure that the system satisfies requirements of liveness and safety types.

Il y a un besoin grandissant pour d'autonomie dans des systèmes temps réel complexes tels que les robots ou les satellites. Ceci met en avant un problème non trivial : d'un côté il y a des systèmes complexes - donc difficiles à valider - avec une intervention de l'humain dans la boucle qui se veut minimale, de l'autre nous avons des domaines où il faut que le système ait un comportement sûr fonctionnellement afin d'éviter les coûts financiers et/ou humains d'une perte ou d'une détérioration du système. Ces deux notions mises en vis-à-vis semblent contradictoires. En effet comment être sûr qu'un système autonome avec un pouvoir décisionnel fort, n'aura pas un comportement non nominal qui pourra menacer le bon déroulement de la mission ? Comment être sûr qu'un satellite n'allumera pas ses réacteurs sans avoir protégé ses capteurs fragiles (objectif de la caméra, ...) ? Une réponse partielle à ce type de problèmes pourrait être d'utiliser un planificateur de haut niveau qui ne donnerait que des plans garantis comme sûrs et valides. Toutefois ces planificateurs n'ont pas un modèle complet des actions qu'ils effectuent et de leurs conséquences. En effet, les directives données par ce planificateur sont généralement affinées en sous tâches par un superviseur. Le planificateur n'a donc pas un contrôle complet sur le moyen d'effectuer cette action. Nous présentons ici les travaux effectués afin d'intégrer un système de contrôle d'exécution en ligne dans une architecture hiérarchisée. Nous décrivons ici la nécessité et le rôle d'un tel composant dans ce type d'architecture. Nous introduisons le R2C, notre contrôleur basé sur les hypothèses synchrones, ainsi que l'outil permettant sa génération en exploitant des techniques issues du model-checking symbolique. Enfin nous discutons de la nécessité de prendre en compte les com-posants décisionnels dans le contrôle afin d'interférer le moins possible avec les décisions prises par ceux-ci. Les résultats obtenus durant des expérimentations sur une plate-forme robotique confirment les idées développées au cours de ce travail et permettent d'en tirer les conclusions et perspectives sur la mise en place d'un contrôle pour l'amélioration de la fiabilité globale de tels systèmes.

Cytotoxic T Lymphocytes (CTL) are known to play an important role in clearing infectious virus from infected hosts in a variety of viral infections. Depending on the type of virus and mode of virus entry both class I and class II restricted CTL can contribute to protection from virus-induced disease. Although CD8 positive CTL are associated with virus elimination and control in many viral infections, elimination of neurotropic viruses from the Central Nervous system (CNS) is more complex due to the lowered expression of MHC antigens on neuronal cells. This failure to constitutively express high levels of MHC antigens by neurons could serve as an advantage to avoid damage to this differentiated and non-renewable tissue. However, abnormal induction of MHC antigens in the CNS mediated by CD4 positive lymphocytes or by astrocytes have also been shown to cause destructive inflammation in the CNS. The present study deals with CTL responses against one such neurotropic virus called Japanese Encephalitis Virus (JEV). JEV is a positive-stranded RNA virus that belongs to the flavivirus group, a group that is among the most important agents causing human encephalitis worldwide. Although passive transfer of monoclonal antibodies against this virus has been shown to confer protection of mice from lethal challenge with virus, neither the presence of CTL against this virus nor its role in conferring protection has been reported so far. Understanding the CTL responses against these viruses acquired importance in light of recent reports that neurovirulence of JEV and yellow fever viruses can be enhanced by the administration of virus specific antibodies. Hence this study was undertaken to examine the possibility of raising CTL specific to JEV. The specificity of the CTL raised, their therapeutic value and the ability of different lymphocyte subsets to mediate protection in vivo are dealt with in this study. Generation of CTL against JEV The generation of CTL against JEV in BALB/c mice, requires MHC defined cell lines that not only support virus infection but are also histocompatible. Several cell lines were initially examined for their ability to support JEV infection as a prc-rcquisitc before their utilization in in vivo and in vitro stimulation protocols aimed at generating JEV-specific CTL. Virus infection was monitored by immunofluorescence using JEV envelope-specific monoclonal antibodies as well as by titration of virus produced from infected cells by plaque assays. These different cell lines that were characterised for their ability to support JEV infection were then utilised to generate and monitor antiviral CTL. Several in vivo immunisation protocols were examined initially find out which of these infected cells prime BALB/c mice efficiently for generation of virus-specific CTL upon secondary stimulation in vitro with infected syngeneic cells. Immunisation of mice with infected cells per se was preferred over free virus since this was thought to facilitate priming against some viral non-structural proteins preferentially found on infected cells in addition to other viral structural proteins. It was observed that not only infected syngeneic and allogeneic cells but also infected xenogeneic cells prime BALB/c mice for the generation of JEV- specific CTL upon secondary restimulation in vitro. An optimal protocol was standardised for the generation of CTL against JEV. This included primary in vivo immunisation of mice followed by secondary in vitro restimulation of splenocytes with infected syngeneic cells. Either immunisation alone or in vitro stimulation of naive splenocytes alone was unsuccessful. The effector cells generated specifically lysed JEV-infccted P388D1 targets but not uninfected P388D1 or YAC-1 targets suggesting that the lysis on infected targets is not mediated by Natural Killer activity. Specificity and MHC restriction of anti JEV Effectors Cell depletion studies using complement mediated lysis were performed to examine the phenotype of the cells mediating virus specific lysis of infected targets. Depletion of Lyt 2.2+ or Thy 1+ but not L3T4+ sub-populations of effector cells inhibited lysis of infected targets showing that the effectors mediating virus-specific lysis were Lyt-2+ T cells. Examination of target specificities and MHC restriction of the antiviral CTL generated showed that although infected xenogeneic cells were used for immunisation, the effector cells recognised only infected syngeneic (P388D1, Sp2/0) and semisyngeneic (Neuro 2a, YAC-1) cells. Virus-specific recognition was found to be class I Kd and class I Dd restricted. These effector cells were also found to recognise cells infected with a closely related flavivirus, West Nile Virus (WNV) suggesting that they were crossreactive to some degree. Based on the consensus motif that has been established for H-2Kd associated peptides, several nonamers were predicted as possible CTL epitopes by scanning the deduced amino acid sequences of three strains of JEV and WNV. Among several predicted nonamers, three peptides were examined for their ability to reconstitute lysis of uninfected targets by polyclonal anti JEV CTL populations. Results demonstrate that peptides derived from NS1 and NS3 but not NS5 protein of JEV were able to partially reconstitute lysis of uninfected targets by effectors when pulsed with the appropriate peptide. Protective ability of the CTL raised against JEV To examine whether anti-JEV effectors raised in vitro could confer protection from intracerebral challenge with JEV, these effectors were adoptively transferred into adult BALB/c mice intracerebrally along with 10 x LDJ0 dose of JEV. More than 55% of these animals were protected from death and survived beyond 100 days after JEV challenge demonstrating that adoptively transferred anti-JEV effectors could indeed confer protection from lethal challenge with JEV. However, adoptive transfer of effectors by either intravenous or intraperitoneal routes did not protect adult mice from the lethal effects of intracerebral challenge with JEV. In contrast to adult mice, newborn mice were not protected from death by the adoptively transferred effector cells. This was also supported by experiments where a correlation was observed with the increasing age of mice and the success of protection conferred by the adoptively transferred effector cells. To establish the identity of cell subsets responsible for protection, Lyt 2, L3T4 or Thy 1 positive cells were specifically depleted from the polyclonal CTL by multiple cycles of complement mediated lysis and the remaining cells were adoptively transferred intracerebrally along with 10 x LD of JEV. These results demonstrate that both Lyt 2 and L3T4 positive T cells present in the effector population were necessary to confer protection of adult mice. Examination of virus-specific neutralising antibodies in the sera of protected and unprotected mice revealed that presence of L3T4 positive cells in the adoptively transferred population increases virus-specific neutralising antibodies. However presence of neutralising antibodies alone was not sufficient to confer protection. The protection required both Lyt-2 and L3T4 positive cells together. These studies could in the long term throw some light on similar observations about age dependant susceptibility to JEV in humans.

O desenvolvimento de sistemas críticos é atualmente um dos problemas mais desafiadores enfrentados pela Engenharia. Há frequentemente uma pressão para se reduzir o tempo total de desenvolvimento, o que dificulta a entrega de sistemas com um mínimo aceitável de defeitos. Nos últimos anos, houve um aumento no tráfego aéreo, o que demanda uma modernização dos sistemas de tráfego aéreo atuais, muito dependentes na figura do controlador. Sistemas de tráfego aéreo são sistemas considerados críticos em segurança e de tempo real. O objetivo do presente trabalho é estabelecer um método de modelagem e verificação formal para sistemas críticos, com aplicação no domínio de tráfego aéreo. Com a adoção de técnicas de modelagem e verificação formal, pretende-se garantir a corretude dos sistemas frente aos requisitos inicialmente especificados e a detecção de erros em fases mais iniciais do projeto, o que resultaria em menores custos envolvidos na sua correção. São fornecidas diretivas para a aplicação do método através de um estudo de caso, baseado em três módulos de um sistema ATC em baixo nível de abstração, para a validação do funcionamento de módulos de software. Para verificação formal, é utilizada a ferramenta NuSMV e as propriedades a serem verificadas são descritas na lógica computacional de árvore (CTL) para garantir que o sistema satisfaça requisitos dos tipos vivacidade e segurança. / Developing safety critical systems is one of the most challenging problems in Engineering nowadays. There is usually a pressure to reduce the total time of the development, what makes it difficult to deliver systems with an acceptable low level of defects. In the recent years, there has been an increase in air trffic, what demands a modernization in the current air traffic systems, which are very dependent on the human controller. Air traffic systems are considered safety critical and real time systems. The objective of the present work is to establish a modeling and formal verification method for critical systems, applicable to the air traffic domain. By adopting modeling and formal verification techniques, it is expected to ensure the systems\' correctness compared with the initially specified requirements and the error detection in the initial phases of the project. Guidelines are provided for applying the method by means of a case study, based in three modules of and ATC system in a low abstraction level, for the validation of the operation of software modules. For the formal verification, it is used the NuSMV tool and the properties to be checked are described in the computational tree logic (CTL) to ensure that the system satisfies requirements of liveness and safety types.

Made available in DSpace on 2014-06-12T15:07:27Z (GMT). No. of bitstreams: 2 arquivo5620_1.pdf: 8916043 bytes, checksum: 669ed68c15dd8910790b9473691f2d57 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2010 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / Na ausência de um sistema imune adaptativo propriamente dito, os cnidários se valem de uma série de mecanismos bioquímicos e celulares que coletivamente compreendem sistemas da imunidade inata e são utilizados para o reconhecimento de micro-organismos, tanto parasitas quanto simbiontes. O objetivo do presente trabalho foi investigar se precursores gênicos relacionados a três polipeptídios envolvidos na resposta inata (CTL: lectina do tipo C, MBL: lectina ligante de manose e C3: componente 3 do sistema complemento) seriam expressos em Palythoa caribaeorum. Tendo como base dados moleculares descritos na literatura para os cnidários Nematostella vectensis, Pocillopora damicornis, Acropora millepora e Swiftia exserta, foram utilizadas duas estratégias metodológicas distintas para responder tal proposição: (1) síntese direta de cDNA a partir do RNAm e amplificação dos homólogos por RT-PCR e (2) construção de uma biblioteca de cDNA para propagação e resgate dos precursores completos (full length cDNAs). Ao todo, foram obtidos 11 produtos de RT-PCR (cDNAs amplificados), dos quais um se refere a um segmento similar a um domínio do receptor de imunoglobulinas das células NK (KIR), encontrado em gorilas. A presença de um domínio semelhante a KIR em P. caribaeorum sugeriria a existência de formas alternativas de imunidade antecipatória em cnidários. Tão importante quanto esse achado foi a obtenção de amplicons de CTL. Dessa forma, os níveis de expressão de transcritos de CTL foram comparados entre colônias sadias e doentes (em processo de branqueamento) de P. caribaeorum. Os resultados para o ensaio de expressão diferencial mostraram que a CTL teve uma expressão aumentada entre 63,2 e 65,5% nas colônias branqueadas, o que sugere um possível papel na resposta ao branqueamento, uma vez que essas moléculas participam do processo de reconhecimento celular. Esse resultado pode ser interpretado de duas formas: o aumento na transcrição de CTL após o branqueamento seria uma tentativa de proteção imediata contra patógenos ou estaria envolvido no recrutamento de novos simbiontes. Como um todo, o estudo de moléculas polipeptídicas da imunidade de cnidários é de importância considerável. Não somente fornece dados sobre a ancestralidade e evolução das reações imunes, mas também serve de base para uma série de aplicações de caráter científico e biotecnológico, que vão desde o monitoramento e conservação de espécies marinhas até estudos voltados ao tratamento e cura de doenças que acometem vertebrados superiores

Final publication is available at http://www.bloodjournal.org/ / 京都大学 / 0048 / 新制・課程博士 / 博士(医学) / 甲第19614号 / 医博第4121号 / 新制||医||1015(附属図書館) / 32650 / 京都大学大学院医学研究科医学専攻 / (主査)教授 髙折 晃史, 教授 山田 亮, 教授 三森 経世 / 学位規則第4条第1項該当 / Doctor of Medical Science / Kyoto University / DFAM

Ethics and Issues in Media is an interactive case-study software that allows communications students to make ethical decisions based on real-life case studies. The evaluation of Ethics and Issues in Media focused on whether or not Ethics and Issues in Media 1) was easy to use, 2) allowed students to make real-life ethical decisions in realistic contexts, 3) enabled students to think about ethical issues in new ways, 4) enabled students to think through and determine potential courses of action to realistic ethical issues and 5) enabled students to understand the consequences of others' ethical decisions. A focus group discussion was held with the creator of Ethics and Issues in Media and with the students who had used it. Students' comments regarding Ethics and Issues in Media were generally positive. Ethics and Issues in Media proved to be successful in the ways that it enabled students to think through ethical issues for themselves, understand the consequences of others' ethical decisions, and think about ethical issues in new ways. Some students found Ethics and Issues in Media to be difficult to navigate, and many had trouble trusting that their answers were saved or submitted properly. The students recommended that the instructor expand the number and type of case studies included in Ethics and Issues in Media. Additionally, I recommend a more thorough orientation to Ethics and Issues in Media prior to implementation as a final exam.

One problem with computers is that the operating system automatically trusts any externallyconnected peripheral. This can result in abuse when a peripheral technically can violate the security model because the peripheral is trusted. Because of that the security is an important issue to look at.The aim of our project is to see in which cases hardware peripherals can be trusted. We built amodel of the universal asynchronous transmitter/receiver (UART), a model of the main memory(RAM) and a model of a DMA controller. We analysed interaction between hardware peripherals,user processes and the main memory.One of our results is that connections with hardware peripherals are secure if the hardware is properly configured. A threat scenario could be an eavesdropper or man-in-the-middle trying to steal data or change a cryptographic key.We consider the use-cases of DMA and protecting a cryptographic key. We prove the well-behavior of the algorithm. Some error-traces resulted from incorrect modelling that was resolved by adjusting the models. Benchmarks were done for different memory sizes.The result is that a peripheral can be trusted provided a configuration is done. Our models consist of finite state machines and their corresponding SMV modules. The models represent computer hardware with DMA. We verified the SMV models using the model checkers NuSMV and nuXmv. / Målet med vårt projekt är att verifiera olika specifikationer av externa enheter som ansluts till datorn. Vi utför formell verifikation av sådan datorutrustning och virtuellt minne. Verifikation med temporal logik, LTL, utförs. Specifikt verifierar vi 4 olika use-case och 9 formler för seriell datakommunikation, DMA och virtuellt minne. Slutsatsen är att anslutning av extern hårdvara är säker om den är ordentligt konfigurerad.Vi gör jämförelser mellan olika minnesstorlekar och mätte tidsåtgången för att verifiera olika system. Vi ser att tidsåtgången för verifikation är långsammare än linjärt beroende och att relativt små system tar relativt lång tid att verifiera.