Cette thèse a pour cadre scientifique la décomposition formelle des spécifications centrali- sées Event-B appliquée aux systèmes distribués BIP. Elle propose une démarche descendante de développement des systèmes distribués corrects par construction en combinant judicieu- sement Event-B et BIP. La démarche proposée comporte trois étapes : Fragmentation, Dis- tribution et Génération de code BIP. Les deux concepts clefs Fragmentation et Distribution, considérés comme deux sortes de raffinement automatique Event-B paramétrées à l'aide de deux DSL appropriés, sont introduits par cette thèse. Cette thèse apporte également une contribution au problème de la génération de code à partir d'un modèle Event-B issu de l'étape de distribution. Nous traitons aussi bien les aspects architecturaux que comportemen- taux. Un soin particulier a été accordé à l'outillage et l'expérimentation de cette démarche. Pour y parvenir, nous avons utilisé l'approche IDM pour l'outillage et l'application Hôtel à clés électroniques pour l'expérimentation. / The scientific framework of this thesis is the formal decomposition of the centralized specifications Event-B applied to distributed systems based on the BIP (Behavior, Interaction, Priority) component framework. It suggets a top-down approach to the development of correct by construction distributed systems by judiciously combining Event-B and BIP. The proposed approach consists in three steps : Fragmentation, Distribution and Generation of BIP code. We introduce two key concepts, Fragmentation and Distribution, which are considered as two kinds of automatic refinement of Event-B models. They are parameterized using two appropriate DSL. This thesis also contributes to the problem of code generation from Event- B models resulting from the Distribution step. Accordingly, we deal with both architectural and behavioral aspects. A special care has been devoted to the implementation and the experimentation of this approach. To achieve this, we have used the IDM approach for tooling and the Electronic Hotel Key System for experimentation.

O cDNA da glicoproteína do vírus da raiva (GPV) foi clonado em vetores plasmidiais (indutíveis) contendo ou não o cDNA do sinal de secreção BiP e da resistência ao antibiótico higromicina B. Esses vetores foram transfectados em células S2 e foram obtidas populações e subpopulações. A população S2MTGPV-H apresentou níveis 5x maiores na expressão da GPV em análise por FACS (~ 50% das células) e por ELISA (~ 0,65 µg/107 células). A seleção de subpopulações permitiu um aumento de aproximadamente 10x na expressão da GPV, especialmente na população S2MTGPV*-H. O tratamento com NaBu resultou em uma redução de aproximadamente 20% no crescimento celular e um aumento de 50% na GPV expressa pela população S2MTGPV*-H (~ 8,3 µg/107 células). O meio de cultura SF900 II permitiu um maior crescimento das células S2MTGPV*-H e uma maior síntese de GPV comparado com outros meios de cultura. Nossos dados mostram que a expressão da GPV pôde ser otimizada através da construção de vetores de expressão/seleção, subpopulações, da exposição da cromatina e do meio de cultura utilizado. / The cDNA encoding the entire rabies virus glycoprotein (RVGP) gene was cloned in plasmids (inductive) with or without a cDNA coding for the secretion signal and coding for the selection hygromicin antibiotic. These vectors were transfected into S2 cells and we had obtain cells populations and subpopulations S2MTRVGP-H cell population were shown to express 5 times higher of RVGP as evaluated by FACS (~ 50 %) and ELISA (~ 0.65 mg/107 cells at day 7). Sub-population selection allowed a higher RVGP expression, especially for the S2MTRVGP*-H. NaBu treatment leading to lower cell growth and higher RVGP expression allowed an even higher RVGP synthesis by S2MTRVGP*-H (~ 8.3 mg/107 cells at day 7 after induction). SF900II medium leading to a higher S2MTRVGP*-H cell growth allowed a higher final RVGP synthesis in this cell culture. The data show that RVGP synthesis may be optimized by the expression/selection vectors design, cell sub-populations selection, chromatine exposure and culture medium employed.

This dissertation describes a study utilizing bioinformatics to analyze homologues of a molecular chaperone, glucose-regulated protein 78 (grp 78), also known as BiP. The selected homologous proteins originate from organisms of infinitely diverse genera. Comparisons of protein sequence yielded the first clues of a common ancestry among these proteins. Furthermore, protein molecular weights, isoelectric points, N-terminal amino acids and half-lives of a known homolog and a non-homologous protein were examined. Additionally, electroporation, a state-of-the-art plasmid insertion technique, was explored using Chlamydomonas reinhardtii, a green alga, as the recipient of a parent plasmid, pSP124S. Distinctive hypertonic solutions and three separate field strengths were used in the plasmolysis of the cell wall of C. reinhardtii and subsequent electroporation, respectively. The number of transformants was tallied to evaluate which electroporation condition would yield the most transformed colonies. We had two discrete hypotheses: 1) that a structurally and functionally similar protein to glucose-regulated protein 78 exists across a wide spectrum of organisms and 2) that Chlamydomonas reinhardtii could be successfully transformed with pSP124S under certain electroporation conditions. The bioinformatics investigation revealed that analogous proteins to Human GRP 78 existed in Mus musculus (mouse), Rattus norvegicus (rat), Gallus domesticus (chicken), Gallus domesticus (chicken), Mesocricetus auratus (golden hamster), Bos taurus (cow), Xenopus laevis (frog), and Spinacia oleracea (spinach). Moreover, these homologous proteins more likely have a common evolutionary origin.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Magíster en Ciencias, Mención Computación / Ingeniero Civil en Computación / A fines del año 2007 se descubrieron vulnerabilidades en el cifrado de las tarjetas modelo MIFARE Classic, populares en el mundo por su masivo uso en sistemas de transporte público. En Chile son usadas como medio de pago en el Transantiago, sistema de transporte público iniciado el 2007, bajo el nombre de tarjetas bip!. A raíz de estas vulnerabilidades, las tarjetas bip! fueron blanco de masivos ataques el año 2014. El objetivo de este trabajo es analizar la seguridad de la utilización de la tarjeta bip! como sistema de pago, y las consecuencias que las vulnerabilidades de la tarjeta pueden llegar a tener sobre la población chilena. Para esto, este trabajo mide no sólo la factibilidad técnica de varios ataques (tanto conocidos como nuevos) sino también el eventual impacto de los mismos. Partiendo de una revisión cuidadosa de los estándares, especificaciones y diversos ataques de sistemas similares, el análisis utiliza diversas técnicas, destacando entre ellas la ingeniería reversa efectuada sobre el sistema y las distintas tarjetas bip! utilizadas, la ingeniería reversa de aplicaciones móviles asociadas al sistema, y la experimentación directa sobre el sistema distribuido real y en funcionamiento del Transantiago, utilizando sólo información públicamente disponible (no información privilegiada). Fruto de este trabajo, en esta tesis se presentan y discuten los resultados obtenidos del análisis mencionado anteriormente, incluidos los éxitos y fracasos cosechados tras intentar vulnerar las medidas de seguridad encontradas. También se analizan las posibles mitigaciones para dichos ataques y se presentan propuestas de mejora. Entre sus resultados más relevantes, destacan varios ataques exitosos que permiten, por ejemplo, inhabilitar tarjetas de otros usuarios mediante el contacto, obtener información personal del dueño de una tarjeta, e incluso obtener beneficios económicos directos. Ejemplo de estos últimos están los ataques donde se simula un transbordo en vez de un viaje nuevo, se modifica el saldo almacenado en una tarjeta o se vuelve a estados previos de la misma utilizando información almacenada previamente en la tarjeta. Junto con esto, el trabajo también clarifica la distribución de la información almacenada en cada tarjeta y su función en el contexto del sistema, aprendida gracias a los distintos experimentos realizados. Finalmente, desde una perspectiva más general, este trabajo entrega un estudio comprensivo de los efectos del uso de una tecnología vulnerable en la operación de un sistema de pago asociado a un sistema de transporte masivo como el Transantiago.

Le langage d'analyse et de description d'architectures (AADL) fait l'objet d'un intérêt croissant dans l'industrie des systèmes embarqués tempsréel. Il définit plusieurs catégories de composants, réparties en trois grandes familles (logiciel, matériel, système). Le travail réalisé durant cette thèse exploite les fonctionnalités offertes par AADL pour spécifier les besoins exacts d'une application et exprimer toutes les caractéristiques tant fonctionnelles que non fonctionnelles dimensions temporelle et spatiale), afin de la produire automatiquement. La méthodologie de production que nous proposons génère automatiquement, à partir d'une application décrite en AADL, une application décrite en BIP. BIP permet de mettre en place des systèmes robustes et sûrs en produisant un contrôleur d'exécution correct par construction et en fournissant un modèle formel. Les objectifs de ce processus de production sont : (1) fournir à AADL une sémantique formelle définie en termes de systèmes de transitions étiquetés ; (2) permettre l'analyse et la validation, c'est à dire, l'exploration exhaustive de l'espace des états du système, la détection des blocages potentiels et la vérification de certaines propriétés ; (3) permettre la génération d'une application exécutable pour simuler et déboguer les modèles AADL. Ces trois derniers points jouent en faveur de l'utilisation de méthodes formelles dans le cycle de développement.

Submitted by Reginaldo Soares de Freitas (reginaldo.freitas@ufv.br) on 2016-09-01T12:08:27Z No. of bitstreams: 1 texto completo.pdf: 631605 bytes, checksum: 52432c66349cbd1015ae06e8db596889 (MD5) / Made available in DSpace on 2016-09-01T12:08:27Z (GMT). No. of bitstreams: 1 texto completo.pdf: 631605 bytes, checksum: 52432c66349cbd1015ae06e8db596889 (MD5) Previous issue date: 1998-07-20 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Proteínas solúveis e de membrana da rota secretora são inicialmente endereçadas ao retículo endoplasmático (RE) e translocadas através da membrana deste. Em seguida, elas transitam através do Golgi para alcançar os compartimentos subcelulares e o meio extracelular. O RE mantém uma eficiente maquinaria de translocação, dobramento, associação, montagem de oligômeros e controle de qualidade de proteínas secretórias. A proteína BiP ("Binding Protein"), residente no RE, exibe atividade de chaperone molecular e participa ativamente neste processo por meio de interações proteína:proteína. Com o objetivo de identificar substratos potenciais de BiP, anticorpos contra frações microssomais isoladas da semente de soja foram usados para o escrutínio de uma biblioteca de expressão. Um clone de cDNA, denominado pUFVS64, que codifica uma proteína secretória, foi isolado e caracterizado. A proteína, codificada por pUFVS64 e denominada S-64, é sintetizada na semente de soja, em baixos níveis, e possui uma identidade de seqüência de 85% com uma proteína de membrana que se liga à sacarose, denominada SBP ("Sucrose Binding Protein"). Células intactas foram utilizadas para introdução de genes via eletroporação, ou biobalística, com o objetivo de aumentar a síntese da proteína S-64 em suspensões celulares de soja, de forma a aumentar a sensibilidade dos ensaios para determinação de associações entre as proteínas BiP e S-64.A associação entre BiP e S-64 foi avaliada, levando-se em consideração características bioquímicas diferenciadas, associadas com as referidas proteínas. Ensaios de sedimentação por afinidade, com o uso das resinas de ATP-agarose, GTP-agarose e ConA- sepharose, foram conduzidos, utilizando-se extratos de proteína total, de suspensões celulares de soja. Tanto S-64 quanto BiP são co-precipitadas por GTP-agarose, embora BiP não se associe com este nucleotídeo. A capacidade da resina GTP-agarose em sedimentar BiP reflete associação prévia entre BiP e uma proteína que liga GTP. Similarmente, ATP-agarose foi eficiente em co-sedimentar ambas as proteínas, embora apenas BiP se ligue diretamente à ATP. A sedimentação indireta de S-64 pela resina ATP-agarose demonstrou que S-64 estava a uma proteína que liga a ATP. A proteína S-64 é glicosilada e se liga diretamente a ConA-sepharose, enquanto BiP não se associa diretamente com concanavalina-A. Mesmo assim, BiP foi co-sedimentada indiretamente por ConA- sepharose. Coletivamente, estes resultados sugerem que S-64 interage com BiP, constituindo um substrato em potencial para caracterização de associações mediadas pela proteína BiP de plantas. / Newly synthesized secretory and membrane proteins are synthesized on membrane-bound polysomes and co-translationally sequestered in the lumen of the endoplasmic reticulum (ER). These proteins then move to and through the Golgi complex where they are either secreted or sorted to subcelullar compartments. The ER keeps an efficient machinery for translocation, association, assembly of secretory proteins which functions as a quality control system of protein exit from this organelle. The ER-resident protein BiP (Binding Protein) exhibits a molecular chaperone activity and has been described as an important component of the quality control mechanism in the ER which is mediated by protein:protein interaction. In order to identify potential substrates for BiP, antibodies raised against membrane-enriched protein fractions from soybean seeds where used as a probe to screen a expression library. A cDNA clone, named pUFVS64, that encodes a secretory protein was isolated and characterized. The cDNA-encoded protein, designated S-64, is synthesized at low levels in soybean seeds and shares 85% sequence identity with the sucrose binding protein (SBP) which is a membrane-associated protein. In order to increase the sensitivity in the assays for detection of BiP:S-64 associations, the S- 64 cDNA was introduzed in soybean cultured cells by electroporation or a biolistic particle delivery system. The S-64:BiP association was evaluated taking advantage of the differential biochemical properties associated with the proteins. Affinity-precipitation assays, using ATP-agarose, GTP-agarose and ConA- sepharose resins, were performed with total protein extracts from soybean cultured cells. Both S-64 and BiP are co-precipitated by GTP-agarose, although BiP does not bind to GTP. The capacity of GTP-agarose to precipitate BiP reflects previous association between BiP and a GTP-binding protein. Likewise, the ATP-agarose resin co-precipitates efficiently both proteins, although just BiP binds ATP. The indirect precipitation of S-64 by ATP-agarose demonstrated that S-64 interacts with an ATP-binding protein. The S-64 protein is glycosylated and binds directly to ConA-sepharose, while BiP does not. However, the efficiency of BiP precipitation by ConA-sepharose was as high as of S-64 precipitation. Taken together, these results suggest that S-64 interacts with BiP and may be a potential substrate for the characterization of protein interactions mediated by plant BiP. / Não foi localizado o cpf do autor.

Ingeniero Civil / El presente trabajo de título tiene por objetivo analizar ciertos patrones anómalos en las transacciones realizadas por los usuarios de Transantiago, sistema de transporte público de Santiago, realizado mediante la tarjeta de pago integrado llamada bip!, los cuales impiden obtener la estimación de bajada en paradero de los usuarios mediante la metodología aplicada para aquello, que actualmente logra obtener un 80% de estimaciones de bajada. El objetivo específico de este trabajo es proponer soluciones desde el punto de vista metodológico a aquellas anomalías detectadas y estudiadas que impiden una obtención completa de la estimación de bajada de los usuarios de Transantiago. Estas soluciones deben ser factibles de incorporar en el modelo, tanto del punto de vista metodológico como del punto de vista computacional. Como parte de este trabajo se revisó tanto el modelo de asignación de bajada en paraderos, en el cual se basa este trabajo, como experiencias internacionales en el uso de información extraída a partir de sistemas de pago similares al de Santiago. Ambas revisiones permiten dar a conocer la base en la cual se trabajará en encontrar y analizar aquellas problemáticas que afecten la metodología. Se realiza además un análisis estadístico de los problemas encontrados, con el fin de tener un estudio más acabado de las anomalías, y desprender de ellas las causas que las originan. Esto conlleva hacer un análisis a parte importante del 20% de estimaciones de bajada que no son posibles de obtener. Entre los principales problemas se destacan el multipago, los problemas de datos de los buses y la validación en zonas paga. En estos tres casos se abordan problemas relacionados con estimación de paradero de bajada nula como estimaciones de bajada incorrectas producto de fallas en el modelo. Luego de analizar las principales anomalías y sus causas, se proponen soluciones factibles orientadas a dos ámbitos: una mejora en los datos de ingreso y cambios en las definiciones de patrones asociados a la forma de viajar de los usuarios de transporte público. Esto si bien no permitirá que el 100% de las estimaciones sean obtenidas, si logrará aumentar con respecto al porcentaje actual de estimaciones.

Ingeniero Civil Industrial / El siguiente trabajo pretende encontrar la tarifa óptima de un abono T el precio por viaje P el sistema de transporte público para la ciudad de Santiago de Chile,resolviendo un problema de tarificación óptima con cobertura de costos (second best) en una sociedad estratificada por su ingreso. Este problema está basado en el modelo de Jara-Díaz y Cruz (2013), el cual considera dos principales efectos relacionados con el ingreso de los individuos sobre la demanda de transporte público. El primero, corresponde a un efecto de corto plazo, llamado efecto ingreso disponible , que corresponde a la variación en la demanda individual del usuario cuando éste, adquiere un abono de transporte. Por otro lado, el segundo efecto corresponde al efecto socioeconómico del ingreso, denominado efecto tasa de motorización , pues corresponde a la disminución de la demanda de transporte público a medida que aumenta el ingreso, el cual está correlacionado con la posesión y uso del automóvil. Para encontrar las tarifas óptimas, se avanza en la obtención de los parámetros del modelo desde dos principales fuentes de datos, que son la encuesta origen destino y las declaraciones de costos de los operadores de buses. En este sentido dentro de este trabajo, se desarrolla un procedimiento de obtención de dichos parámetros debido a las particularidades que presentan las fuentes de información antes mencionadas. Si bien se desarrolla para el caso de la ciudad de Santiago de Chile, al ser las fuentes de información genéricas podría ser aplicado en otras ciudades. Una vez estimado los parámetros requeridos, el modelo se resuelve mediante la evaluación de todos los casos posibles de las alternativas de pagos a los que pueden optar los individuos de los estratos, llegando a un valor óptimo de T=22.176 y de P=663 con un alcance superior al 90% que elige la alternativa del abono por sobre el pago por viaje.

Magíster en Ciencias de la Ingeniería, Mención Transporte / Ingeniero Civil Industrial / El objetivo de esta tesis es desarrollar y aplicar una metodología de corrección de la matriz origen-destino de viajes de Santiago, generada con datos pasivos de transacciones y del sistema de posicionamiento global instalado en los buses de transporte público, de forma que incorpore los efectos de la evasión de la tarifa, ya que estos viajes, de haber sido evadidos totalmente no aparecen en la matriz, y en el caso de tratarse de una evasión de parte de las etapas de viajes, distorsionan la estimación de viajes. Esta situación entorpece algunas de las aplicaciones que tiene esta potente herramienta de planificación. Para tal fin, se desarrolla una metodología que consta de dos pasos principales: una primera etapa corrige la evasión parcial de los viajes que utilizan metro. Se usa información proveniente de la encuesta origen-destino realizada por Metro S.A. para generar un factor de expansión que refleje la sobreestimación de los viajes que se inician en una estación de Metro, en desmedro de los que realizan una etapa en bus para llegar, pero sin pagarla. Esta corrección modifica la estructura de la matriz, ya que disminuye el peso de los viajes cuya primera transacción es en metro en desmedro de algunos de los que utilizan bus para acercarse al tren subterráneo. En forma posterior, un segundo módulo calibra un factor de expansión que incorpora la evasión dura, en la cual se evaden todas las etapas. Este se realiza mediante un método iterativo de punto fijo, en el cual la expansión de los viajes cubre un total de etapas evadidas calculadas desde mediciones exógenas de evasión en bus, a las cuales se les resta las que fueron explicadas por la corrección de la etapa anterior. El método se calibró experimentalmente con datos de la ciudad de Santiago, lo que arrojó una serie de recomendaciones para la captura y tratamiento de datos, que facilita la aplicación práctica de este trabajo. El análisis del comportamiento de la evasión en la aplicación experimental, arroja que se produce poca evasión blanda para acceder a metro en una distancia caminable a la estación, indicando que la gente al no tener carga prefiere caminar. Respecto a la evasión dura, se predice mayor tasa de viajes evadidos entre pares de comunas que no tienen opción de realizar un viaje de una sola etapa en Metro, lo que indica que frente a una mejor calidad de servicio, los usuarios prefieren pagar.