Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

Plataforma de resolució de problemes RCPSP utilitzant SMT

El problema d'operacions (scheduling) és un procés de presa de decisions quejuga un paper molt important en organitzacions de manufactura i serveis, jaque té una aplicació a la producció, transport i distribució, i a la comunicaciói processament d'informació, entre d'altres. Consisteix en assignar d'unamanera apropiada els recursos disponibles per al processament de tasquesde manera que es puguin optimitzar els objectius de l’organització.Com cas particular de la programació d'operacions, hi ha la programacióde projectes (Project Scheduling), que és el procés de planificar, organitzari controlar activitats i recursos per aconseguir un objectiu concret, generalmentamb limitacions de temps, recursos o costos. Dins aquest grup essituen els problemes de programació de projectes (PSP), que és un nomgenèric que es dóna a tota una classe de problemes en els quals és necessàriala programació de manera òptima el temps, el cost i els recursos dels projectes.La finalitat d'aquest projecte és crear una plataforma RCPSP que puguillegir diferents formats d'entrada (fitxers del tipus :.rcp,.sch,.sm,.data,.pat),pre-processar-los, codificar-los a través de diferents modelitzacions (TaskRD,TimeRD...) per tal de poder-los passar a instàncies SMT i poder executar-losa través de la API de Yices. L'objectiu és trobar el temps d'inici percada activitat de manera que es minimitzi la longitud del makespan senseque es violin les restriccions.Cal dissenyar una aplicació en C++, que sigui escalable i que puguiaconseguir el resultat del problema en el temps més òptim possible

Alignment Model and Training Technique in SMT from English to Malayalam

This paper investigates certain methods of training adopted in the Statistical Machine Translator (SMT) from English to Malayalam. In English Malayalam SMT, the word to word translation is determined by training the parallel corpus. Our primary goal is to improve the alignment model by reducing the number of possible alignments of all sentence pairs present in the bilingual corpus. Incorporating morphological information into the parallel corpus with the help of the parts of speech tagger has brought around better training results with improved accuracy

Arquiteturas multi-tarefas simultâneas : SEMPRE : arquitetura SMT com capacidade de execução e escalonamento de processos

O avanço tecnológico no projeto de microprocessadores, nos recentes anos, tem seguido duas tendências principais. A primeira tenta aumentar a freqüência do relógio dos mesmos usando componentes digitais e técnicas VLSI mais eficientes. A segunda tenta explorar paralelismo no nível de instrução através da reorganização dos seus componentes internos. Dentro desta segunda abordagem estão as arquiteturas multi-tarefas simultâneas, que são capazes de extrair o paralelismo existente entre e dentro de diferentes tarefas das aplicações, executando instruções de vários fluxos simultaneamente e maximizando assim a utilização do hardware. Apesar do alto custo da implementação em hardware, acredita-se no potencial destas arquiteturas para o futuro próximo, pois é previsto que em breve haverá a disponibilidade de bilhões de transistores para o desenvolvimento de circuitos integrados. Assim, a questão principal a ser encarada talvez seja: como prover instruções paralelas para uma arquitetura deste tipo? Sabe-se que a maioria das aplicações é seqüencial pois os problemas nem sempre possuem uma solução paralela e quando a solução existe os programadores nem sempre têm habilidade para ver a solução paralela. Pensando nestas questões a arquitetura SEMPRE foi projetada. Esta arquitetura executa múltiplos processos, ao invés de múltiplas tarefas, aproveitando assim o paralelismo existente entre diferentes aplicações. Este paralelismo é mais expressivo do que aquele que existe entre tarefas dentro de uma mesma aplicação devido a não existência de sincronismo ou comunicação entre elas. Portanto, a arquitetura SEMPRE aproveita a grande quantidade de processos existentes nas estações de trabalho compartilhadas e servidores de rede. Além disso, esta arquitetura provê suporte de hardware para o escalonamento de processos e instruções especiais para o sistema operacional gerenciar processos com mínimo esforço. Assim, os tempos perdidos com o escalonamento de processos e as trocas de contextos são insignificantes nesta arquitetura, provendo ainda maior desempenho durante a execução das aplicações. Outra característica inovadora desta arquitetura é a existência de um mecanismo de prébusca de processos que, trabalhando em cooperação com o escalonamento de processos, permite reduzir faltas na cache de instruções. Também, devido a essa rápida troca de contexto, a arquitetura permite a definição de uma fatia de tempo (fatia de tempo) menor do que aquela praticada pelo sistema operacional, provendo maior dinâmica na execução das aplicações. A arquitetura SEMPRE foi analisada e avaliada usando modelagem analítica e simulação dirigida por execução de programas do SPEC95. A modelagem mostrou que o escalonamento por hardware reduz os efeitos colaterais causados pela presença de processos na cache de instruções e a simulação comprovou que as diferentes características desta arquitetura podem, juntas, prover ganho de desempenho razoável sobre outras arquiteturas multi-tarefas simultâneas equivalentes, com um pequeno acréscimo de hardware, melhor aproveitando as fatias de tempo atribuídas aos processos.

La escuela rural debe formar “solucionadores de problemas”

Introducción Hasta el presidente del Banco Mundial, institución cuya principal función es exactamente otorgar créditos para el desarrollo, reconoce que el conocimiento es más importante que el capital…

Cervical mobilisation: concurrent effects on pain, sympathetic nervous system activity and motor activity

Recent findings that spinal manual therapy (SMT) produces concurrent hypoalgesic and sympathoexcitatory effects have led to the proposal that SMT may exert its initial effects by activating descending inhibitory pathways from the dorsal periaqueductal gray area of the midbrain (dPAG). In addition to hypoalgesic and sympathoexcitatory effects, stimulation of the dPAG in animals has been shown to hal e a facilitatory effect on motor activity. This study sought to further investigate the proposal regarding SMT and the FAG by including a test of motor function in addition to the variables previously investigated, Using a condition randomised, placebo-controlled, double blind, repeated measures design, 30 subjects with mid to lon er cervical spine pain of insidious onset participated in the study. The results indicated that the cervical mobilisation technique produced a hypoalgesic effect as revealed by increased pressure pain thresholds on the side of treatment (P = 0.0001) and decreased resting visual analogue scale scores (P = 0.049). The treatment technique also produced a sympathoexcitatory effect with an increase in skin conductance (P < 0.002) and a decrease in skin temperature (P = < 0.02). There was a decrease in superficial neck flexor muscle activity (P < 0.0002) at the lower levels of a staged cranio-cervical flexion test. This could imply facilitation of the deep neck flexor muscles with a decreased need for co-activation of the superficial neck flexors, The combination of all findings,would support the proposal that SMT may, at least initially, exert part of its influence via activation of the PAG, (C) 2000 Harcourt Publishers Ltd.

Formal Contracts for Runtime Verification Support in the Ada Programming Language

Poster presented in The 28th GI/ITG International Conference on Architecture of Computing Systems (ARCS 2015). 24 to 26, Mar, 2015. Porto, Portugal.

Caracterização química e física de conformal coatings envolvidos na produção de PCBA's

Dissertação de mestrado integrado em Engenharia de Materiais

Controlo de qualidade e inspeção visual por imagem: definição de uma aplicação para registo de alterações e avaliação de desempenho

Dissertação de mestrado em Engenharia e Gestão da Qualidade

Métodos para el análisis de programas probabilistas y no-deterministas utilizando probadores de teoremas. Methods for the analysis of probabilistic and nondeterministic programs using theorem provers.

La verificación y el análisis de programas con características probabilistas es una tarea necesaria del quehacer científico y tecnológico actual. El éxito y su posterior masificación de las implementaciones de protocolos de comunicación a nivel hardware y soluciones probabilistas a problemas distribuidos hacen más que interesante el uso de agentes estocásticos como elementos de programación. En muchos de estos casos el uso de agentes aleatorios produce soluciones mejores y más eficientes; en otros proveen soluciones donde es imposible encontrarlas por métodos tradicionales. Estos algoritmos se encuentran generalmente embebidos en múltiples mecanismos de hardware, por lo que un error en los mismos puede llegar a producir una multiplicación no deseada de sus efectos nocivos.Actualmente el mayor esfuerzo en el análisis de programas probabilísticos se lleva a cabo en el estudio y desarrollo de herramientas denominadas chequeadores de modelos probabilísticos. Las mismas, dado un modelo finito del sistema estocástico, obtienen de forma automática varias medidas de performance del mismo. Aunque esto puede ser bastante útil a la hora de verificar programas, para sistemas de uso general se hace necesario poder chequear especificaciones más completas que hacen a la corrección del algoritmo. Incluso sería interesante poder obtener automáticamente las propiedades del sistema, en forma de invariantes y contraejemplos.En este proyecto se pretende abordar el problema de análisis estático de programas probabilísticos mediante el uso de herramientas deductivas como probadores de teoremas y SMT solvers. Las mismas han mostrado su madurez y eficacia en atacar problemas de la programación tradicional. Con el fin de no perder automaticidad en los métodos, trabajaremos dentro del marco de "Interpretación Abstracta" el cual nos brinda un delineamiento para nuestro desarrollo teórico. Al mismo tiempo pondremos en práctica estos fundamentos mediante implementaciones concretas que utilicen aquellas herramientas.

Verificación Formal de Sistemas basada Formal Software Verification based on Automated Analysisen Análisis Automático.

Identificación y caracterización del problema. Uno de los problemas más importantes asociados con la construcción de software es la corrección del mismo. En busca de proveer garantías del correcto funcionamiento del software, han surgido una variedad de técnicas de desarrollo con sólidas bases matemáticas y lógicas conocidas como métodos formales. Debido a su naturaleza, la aplicación de métodos formales requiere gran experiencia y conocimientos, sobre todo en lo concerniente a matemáticas y lógica, por lo cual su aplicación resulta costosa en la práctica. Esto ha provocado que su principal aplicación se limite a sistemas críticos, es decir, sistemas cuyo mal funcionamiento puede causar daños de magnitud, aunque los beneficios que sus técnicas proveen son relevantes a todo tipo de software. Poder trasladar los beneficios de los métodos formales a contextos de desarrollo de software más amplios que los sistemas críticos tendría un alto impacto en la productividad en tales contextos. Hipótesis. Contar con herramientas de análisis automático es un elemento de gran importancia. Ejemplos de esto son varias herramientas potentes de análisis basadas en métodos formales, cuya aplicación apunta directamente a código fuente. En la amplia mayoría de estas herramientas, la brecha entre las nociones a las cuales están acostumbrados los desarrolladores y aquellas necesarias para la aplicación de estas herramientas de análisis formal sigue siendo demasiado amplia. Muchas herramientas utilizan lenguajes de aserciones que escapan a los conocimientos y las costumbres usuales de los desarrolladores. Además, en muchos casos la salida brindada por la herramienta de análisis requiere cierto manejo del método formal subyacente. Este problema puede aliviarse mediante la producción de herramientas adecuadas. Otro problema intrínseco a las técnicas automáticas de análisis es cómo se comportan las mismas a medida que el tamaño y complejidad de los elementos a analizar crece (escalabilidad). Esta limitación es ampliamente conocida y es considerada crítica en la aplicabilidad de métodos formales de análisis en la práctica. Una forma de atacar este problema es el aprovechamiento de información y características de dominios específicos de aplicación. Planteo de objetivos. Este proyecto apunta a la construcción de herramientas de análisis formal para contribuir a la calidad, en cuanto a su corrección funcional, de especificaciones, modelos o código, en el contexto del desarrollo de software. Más precisamente, se busca, por un lado, identificar ambientes específicos en los cuales ciertas técnicas de análisis automático, como el análisis basado en SMT o SAT solving, o el model checking, puedan llevarse a niveles de escalabilidad superiores a los conocidos para estas técnicas en ámbitos generales. Se intentará implementar las adaptaciones a las técnicas elegidas en herramientas que permitan su uso a desarrolladores familiarizados con el contexto de aplicación, pero no necesariamente conocedores de los métodos o técnicas subyacentes. Materiales y métodos a utilizar. Los materiales a emplear serán bibliografía relevante al área y equipamiento informático. Métodos. Se emplearán los métodos propios de la matemática discreta, la lógica y la ingeniería de software. Resultados esperados. Uno de los resultados esperados del proyecto es la individualización de ámbitos específicos de aplicación de métodos formales de análisis. Se espera que como resultado del desarrollo del proyecto surjan herramientas de análisis cuyo nivel de usabilidad sea adecuado para su aplicación por parte de desarrolladores sin formación específica en los métodos formales utilizados. Importancia del proyecto. El principal impacto de este proyecto será la contribución a la aplicación práctica de técnicas formales de análisis en diferentes etapas del desarrollo de software, con la finalidad de incrementar su calidad y confiabilidad. A crucial factor for software quality is correcteness. Traditionally, formal approaches to software development concentrate on functional correctness, and tackle this problem basically by being based on well defined notations founded on solid mathematical grounds. This makes formal methods better suited for analysis, due to their precise semantics, but they are usually more complex, and require familiarity and experience with the manipulation of mathematical definitions. So, their acceptance by software engineers is rather restricted, and formal methods applications have been confined to critical systems. Nevertheless, it is obvious that the advantages that formal methods provide apply to any kind of software system. It is accepted that appropriate software tool support for formal analysis is essential, if one seeks providing support for software development based on formal methods. Indeed, some of the relatively recent sucesses of formal methods are accompanied by good quality tools that automate powerful analysis mechanisms, and are even integrated in widely used development environments. Still, most of these tools either concentrate on code analysis, and in many cases are still far from being simple enough to be employed by software engineers without experience in formal methods. Another important problem for the adoption of tool support for formal methods is scalability. Automated software analysis is intrinsically complex, and thus techniques do not scale well in the general case. In this project, we will attempt to identify particular modelling, design, specification or coding activities in software development processes where to apply automated formal analysis techniques. By focusing in very specific application domains, we expect to find characteristics that might be exploited to increase the scalability of the corresponding analyses, compared to the general case.

Optimisation of a surface mount technology process using a SnAgCu lead-free alloy

The impending introduction of lead-free solder in the manufacture of electrical and electronic products has presented the electronics industry with many challenges. European manufacturers must transfer from a tin-lead process to a lead-free process by July 2006 as a result of the publication of two directives from the European Parliament. Tin-lead solders have been used for mechanical and electrical connections on printed circuit boards for over fifty years and considerable process knowledge has been accumulated. Extensive literature reviews were conducted on the topic and as a result it was found there are many implications to be considered with the introduction of lead-free solder. One particular question that requires answering is; can lead-free solder be used in existing manufacturing processes? The purpose of this research is to conduct a comparative study of a tin-lead solder and a lead-free solder in two key surface mount technology (SMT) processes. The two SMT processes in question were the stencil printing process and the reflow soldering process. Unreplicated fractional factorial experimental designs were used to carry out the studies. The quality of paste deposition in terms of height and volume were the characteristics of interest in the stencil printing process. The quality of solder joints produced in the reflow soldering experiment was assessed using x-ray and cross sectional analysis. This provided qualitative data that was then uniquely scored and weighted using a method developed during the research. Nested experimental design techniques were then used to analyse the resulting quantitative data. Predictive models were developed that allowed for the optimisation of both processes. Results from both experiments show that solder joints of comparable quality to those produced using tin-lead solder can be produced using lead-free solder in current SMT processes.

Sound objects in time, space and action

SOUND OBJECTS IN TIME, SPACE AND ACTIONThe term "sound object" describes an auditory experience that is associated with an acoustic event produced by a sound source. At cortical level, sound objects are represented by temporo-spatial activity patterns within distributed neural networks. This investigation concerns temporal, spatial and action aspects as assessed in normal subjects using electrical imaging or measurement of motor activity induced by transcranial magnetic stimulation (TMS).Hearing the same sound again has been shown to facilitate behavioral responses (repetition priming) and to modulate neural activity (repetition suppression). In natural settings the same source is often heard again and again, with variations in spectro-temporal and spatial characteristics. I have investigated how such repeats influence response times in a living vs. non-living categorization task and the associated spatio-temporal patterns of brain activity in humans. Dynamic analysis of distributed source estimations revealed differential sound object representations within the auditory cortex as a function of the temporal history of exposure to these objects. Often heard sounds are coded by a modulation in a bilateral network. Recently heard sounds, independently of the number of previous exposures, are coded by a modulation of a left-sided network.With sound objects which carry spatial information, I have investigated how spatial aspects of the repeats influence neural representations. Dynamics analyses of distributed source estimations revealed an ultra rapid discrimination of sound objects which are characterized by spatial cues. This discrimination involved two temporo-spatially distinct cortical representations, one associated with position-independent and the other with position-linked representations within the auditory ventral/what stream.Action-related sounds were shown to increase the excitability of motoneurons within the primary motor cortex, possibly via an input from the mirror neuron system. The role of motor representations remains unclear. I have investigated repetition priming-induced plasticity of the motor representations of action sounds with the measurement of motor activity induced by TMS pulses applied on the hand motor cortex. TMS delivered to the hand area within the primary motor cortex yielded larger magnetic evoked potentials (MEPs) while the subject was listening to sounds associated with manual than non- manual actions. Repetition suppression was observed at motoneuron level, since during a repeated exposure to the same manual action sound the MEPs were smaller. I discuss these results in terms of specialized neural network involved in sound processing, which is characterized by repetition-induced plasticity.Thus, neural networks which underlie sound object representations are characterized by modulations which keep track of the temporal and spatial history of the sound and, in case of action related sounds, also of the way in which the sound is produced.LES OBJETS SONORES AU TRAVERS DU TEMPS, DE L'ESPACE ET DES ACTIONSLe terme "objet sonore" décrit une expérience auditive associée avec un événement acoustique produit par une source sonore. Au niveau cortical, les objets sonores sont représentés par des patterns d'activités dans des réseaux neuronaux distribués. Ce travail traite les aspects temporels, spatiaux et liés aux actions, évalués à l'aide de l'imagerie électrique ou par des mesures de l'activité motrice induite par stimulation magnétique trans-crânienne (SMT) chez des sujets sains. Entendre le même son de façon répétitive facilite la réponse comportementale (amorçage de répétition) et module l'activité neuronale (suppression liée à la répétition). Dans un cadre naturel, la même source est souvent entendue plusieurs fois, avec des variations spectro-temporelles et de ses caractéristiques spatiales. J'ai étudié la façon dont ces répétitions influencent le temps de réponse lors d'une tâche de catégorisation vivant vs. non-vivant, et les patterns d'activité cérébrale qui lui sont associés. Des analyses dynamiques d'estimations de sources ont révélé des représentations différenciées des objets sonores au niveau du cortex auditif en fonction de l'historique d'exposition à ces objets. Les sons souvent entendus sont codés par des modulations d'un réseau bilatéral. Les sons récemment entendus sont codé par des modulations d'un réseau du côté gauche, indépendamment du nombre d'expositions. Avec des objets sonores véhiculant de l'information spatiale, j'ai étudié la façon dont les aspects spatiaux des sons répétés influencent les représentations neuronales. Des analyses dynamiques d'estimations de sources ont révélé une discrimination ultra rapide des objets sonores caractérisés par des indices spatiaux. Cette discrimination implique deux représentations corticales temporellement et spatialement distinctes, l'une associée à des représentations indépendantes de la position et l'autre à des représentations liées à la position. Ces représentations sont localisées dans la voie auditive ventrale du "quoi".Des sons d'actions augmentent l'excitabilité des motoneurones dans le cortex moteur primaire, possiblement par une afférence du system des neurones miroir. Le rôle des représentations motrices des sons d'actions reste peu clair. J'ai étudié la plasticité des représentations motrices induites par l'amorçage de répétition à l'aide de mesures de potentiels moteurs évoqués (PMEs) induits par des pulsations de SMT sur le cortex moteur de la main. La SMT appliquée sur le cortex moteur primaire de la main produit de plus grands PMEs alors que les sujets écoutent des sons associée à des actions manuelles en comparaison avec des sons d'actions non manuelles. Une suppression liée à la répétition a été observée au niveau des motoneurones, étant donné que lors de l'exposition répétée au son de la même action manuelle les PMEs étaient plus petits. Ces résultats sont discuté en termes de réseaux neuronaux spécialisés impliqués dans le traitement des sons et caractérisés par de la plasticité induite par la répétition. Ainsi, les réseaux neuronaux qui sous-tendent les représentations des objets sonores sont caractérisés par des modulations qui gardent une trace de l'histoire temporelle et spatiale du son ainsi que de la manière dont le son a été produit, en cas de sons d'actions.

Análisis de rendimiento de aplicaciones en sistemas multicore

El rápido crecimiento del los sistemas multicore y los diversos enfoques que estos han tomado, permiten que procesos complejos que antes solo eran posibles de ejecutar en supercomputadores, hoy puedan ser ejecutados en soluciones de bajo coste también denominadas "hardware de comodidad". Dichas soluciones pueden ser implementadas usando los procesadores de mayor demanda en el mercado de consumo masivo (Intel y AMD). Al escalar dichas soluciones a requerimientos de cálculo científico se hace indispensable contar con métodos para medir el rendimiento que los mismos ofrecen y la manera como los mismos se comportan ante diferentes cargas de trabajo. Debido a la gran cantidad de tipos de cargas existentes en el mercado, e incluso dentro de la computación científica, se hace necesario establecer medidas "típicas" que puedan servir como soporte en los procesos de evaluación y adquisición de soluciones, teniendo un alto grado de certeza de funcionamiento. En la presente investigación se propone un enfoque práctico para dicha evaluación y se presentan los resultados de las pruebas ejecutadas sobre equipos de arquitecturas multicore AMD e Intel.