Tunnig optical A-Sic/A-Si active filters by UV bias light in the visible and infrared spectral ranges

Visible range to telecom band spectral translation is accomplished using an amorphous SiC pi'n/pin wavelength selector under appropriate front and back optical light bias. Results show that background intensity works as selectors in the infrared region, shifting the sensor sensitivity. Low intensities select the near-infrared range while high intensities select the visible part according to its wavelength. Here, the optical gain is very high in the infrared/red range, decreases in the green range, stays close to one in the blue region and strongly decreases in the near-UV range. The transfer characteristics effects due to changes in steady state light intensity and wavelength backgrounds are presented. The relationship between the optical inputs and the output signal is established. A capacitive optoelectronic model is presented and tested using the experimental results. © 2014 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

A system verification strategy based on the BST infrastructure

A good verification strategy should bring near the simulation and real functioning environments. In this paper we describe a system-level co-verification strategy that uses a common flow for functional simulation, timing simulation and functional debug. This last step requires using a BST infrastructure, now widely available on commercial devices, specially on FPGAs with medium/large pin-counts.

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.

Toward a Run-Time Verification Framework for Real-Time Safety-Critical Systems

Presented at SEMINAR "ACTION TEMPS RÉEL:INFRASTRUCTURES ET SERVICES SYSTÉMES". 10, Apr, 2015. Brussels, Belgium.

Monte Carlo simulations for dosimetric verification in photon and electron beam radiotherapy

Dissertação para obtenção do Grau de Doutor em Engenharia Biomédica

Constraint-based verification of imperative programs

work presented in the context of the European Master’s program in Computational Logic, as the partial requirement for obtaining Master of Science degree in Computational Logic

Verification of analog circuits in power-down mode

Dissertação para obtenção do Grau de Mestre em Engenharia Eletrotécnica e Computadores

Planning and verification of multipath routing protocols

Conventionally the problem of the best path in a network refers to the shortest path problem. However, for the vast majority of networks present nowadays this solution has some limitations which directly affect their proper functioning, as well as an inefficient use of their potentialities. Problems at the level of large networks where graphs of high complexity are commonly present as well as the appearing of new services and their respective requirements, are intrinsically related to the inability of this solution. In order to overcome the needs present in these networks, a new approach to the problem of the best path must be explored. One solution that has aroused more interest in the scientific community considers the use of multiple paths between two network nodes, where they can all now be considered as the best path between those nodes. Therefore, the routing will be discontinued only by minimizing one metric, where only one path between nodes is chosen, and shall be made by the selection of one of many paths, thereby allowing the use of a greater diversity of the present paths (obviously, if the network consents). The establishment of multi-path routing in a given network has several advantages for its operation. Its use may well improve the distribution of network traffic, improve recovery time to failure, or it can still offer a greater control of the network by its administrator. These factors still have greater relevance when networks have large dimensions, as well as when their constitution is of high complexity, such as the Internet, where multiple networks managed by different entities are interconnected. A large part of the growing need to use multipath protocols is associated to the routing made based on policies. Therefore, paths with different characteristics can be considered with equal level of preference, and thus be part of the solution for the best way problem. To perform multi-path routing using protocols based only on the destination address has some limitations but it is possible. Concepts of graph theory of algebraic structures can be used to describe how the routes are calculated and classified, enabling to model the routing problem. This thesis studies and analyzes multi-path routing protocols from the known literature and derives a new algebraic condition which allows the correct operation of these protocols without any network restriction. It also develops a range of software tools that allows the planning and the respective verification/validation of new protocols models according to the study made.

Semantics bias in cross-national comparative analyses : Is it good or bad to have "fair" health?

The Health Behavior in School-aged Children is a cross-national study collecting data on social and health indicators on adolescents in 43 countries. The study provides comparable data on health behaviors and health outcomes through the use of a common protocol, which have been a back bone of the study sine its initiation in 1983. Recent years, researchers within the study have noticed a questionable comparability on the widely used item on self-rated health. One of the four response categories to the item "Would you say your health is….?" showed particular variation, as the response category "Fair" varied from 20 % in Latvia and Moldova to 3-4 % in Bulgaria and Macedonia. A qualitative mini-survey of the back-translations showed that the response category "Fair" had a negative slant in 25 countries, a positive slant in 10 countries and was considered neutral in 9 countries. This finding indicates that there are what may be called semantic issues affecting comparability in international studies, since the same original word (in an English original) is interpreted differently across countries and cultures. The paper test and discuss a few possible explanations to this, however, only leaving to future studies to hold a cautious approach to international comparisons if working with the self-rated health item with four response categories.

Local Rainfall Variability - A Potential Bias for Bioecological Studies in the Central Amazon

Rainfall data registered betwe en 1910 and 1979 at Manaus confirm the existence of a dry season between June and November (monthly rainfall: 42-162mm) and a rainy season from December until May (monthly rainfall: 211-300mm). Annual precipitation amounted to 2105mm with about 75% of the rainfall recorded during the rainy season. Rainfall data collected over 12 months at eigth stations in the vicinity of and at Manaus are compared. Annual precipitation was lower in Inundation Regions (1150-2150mm) compared with Dryland Regions (2400-2550mm). Considerable differences are found in rainfall patterns (intensity, frequency and time of rainfall). This is also truefor neighbouring stations, even if data of a 11-year record period are compared. Thus, it is highly recommended that preciptation data for bioecological studies be collected at the study site.

Bias in returns to tenure when firm wages and employment comove: A quantitative assessment and solution

It is well known that, unless worker-firm match quality is controlled for, returns to firm tenure (RTT) estimated directly via reduced form wage (Mincer) equations will be biased. In this paper we show that even if match quality is properly controlled for there is a further pervasive source of bias, namely the co-movement of firm employment and firm wages. In a simple mechanical model where human capital is absent and separation is exogenous we show that positively covarying shocks (either aggregate or firm level) to firms employment and wages cause downward bias in OLS regression estimates of RTT. We show that the long established procedures for dealing with "traditional" RTT bias do not circumvent the additional problem we have identified. We argue that if a reduced form estimation of RTT is undertaken, firm-year fixed effects must be added in order to eliminate this bias. Estimates from two large panel datasets from Portugal and Germany show that the bias is empirically important. Adding firm-year fixed effects to the regression increases estimates of RTT in the two respective countries by between 3.5% and 4.5% of wages at 20 years of tenure over 80% (50%) of the estimated RTT level itself. The results extend to tenure correlates used in macroeconomics such as the minimum unemployment rate since joining the firm. Adding firm-year fixed effects changes estimates of these effects also.

On the verification of architectural reconfigurations

In a reconfigurable system, the response to contextual or internal change may trigger reconfiguration events which, on their turn, activate scripts that change the system׳s architecture at runtime. To be safe, however, such reconfigurations are expected to obey the fundamental principles originally specified by its architect. This paper introduces an approach to ensure that such principles are observed along reconfigurations by verifying them against concrete specifications in a suitable logic. Architectures, reconfiguration scripts, and principles are specified in Archery, an architectural description language with formal semantics. Principles are encoded as constraints, which become formulas of a two-layer graded hybrid logic, where the upper layer restricts reconfigurations, and the lower layer constrains the resulting configurations. Constraints are verified by translating them into logic formulas, which are interpreted over models derived from Archery specifications of architectures and reconfigurations. Suitable notions of bisimulation and refinement, to which the architect may resort to compare configurations, are given, and their relationship with modal validity is discussed.

Perfil neuropsicológico y sesgos cognitivos de adolescentes con diferentes patrones de consumo de alcohol. Neuropsychological profile and cognitive bias in adolescents with different alcohol consumption patterns.

Identificación y caracterización del problema objeto de estudio: Diversas investigaciones señalan que el uso o consumo de alcohol comienza durante la adolescencia. En este periodo del desarrollo típicamente se han reportado deterioros asociados con el consumo de alcohol sobre diversas funciones cognitivas. Sin embargo, los hallazgos no siempre han sido concluyentes. Hipótesis: a) Existe una mayor cantidad de déficits neuropsicológicos (especialmente en los dominios asociados con la toma de decisiones) en los grupos de adolescentes que presentan patrones de consumo elevados o tipo binge y en los adolescentes bajo tratamiento; b) Existen sesgos cognitivos de tipo implícito en los adolescentes expuestos a publicidades referidas a bebidas alcohólicas; y c) Existe mayor presencia de expectativas negativas en el grupo conformado por niños, así como una mayor presencia de expectativas positivas en el grupo conformado por adolescentes. Planteo de Objetivos: se pretende lograr un perfil neuropsicológico de adolescentes de ambos sexos en función de patrones de consumo de alcohol bien diferenciados. Asimismo, se intentará determinar la presencia de sesgos cognitivos hacia estímulos asociados con el alcohol en función de las expectativas hacia el psicotrópico y el tipo de consumo del mismo que presenta la población bajo estudio. Finalmente, se buscará determinar si existen cambios evolutivos en las expectativas hacia el alcohol que pudieran indicar la presencia de mayor vulnerabilidad al consumo de alcohol. Materiales y métodos a utilizar: Se utilizarán pruebas neuropsicológicas (IGT, WCST, otras) y cognitivas (AEQ o similares). Se apelará al uso de diseños ex post facto prospectivos de tipo simple o factoriales, diseños factoriales, estudios instrumentales y estudios descriptivos de poblaciones mediante encuestas. Resultados esperados: 1) Se espera encontrar una mayor cantidad de déficits neuropsicológicos (especialmente en los dominios asociados con la toma de decisiones) en los grupos de adolescentes con patrones de consumo de alcohol elevados y binge, así como en el grupo de adolescentes bajo tratamiento. 2) Se espera encontrar la presencia de sesgos cognitivos implícitos en aquellos adolescentes expuestos a publicidades referidas a bebidas alcohólicas en contraposición a los adolescentes expuestos a publicidades de bebidas no-alcohólicas. 3) Se espera encontrar una mayor presencia de expectativas negativas en el grupo conformado por niños, y una mayor presencia de expectativas positivas en el grupo conformado por adolescentes, con lo que se verificaría el supuesto que señala que las EA se modifican a lo largo del desarrollo. Asimismo, se espera confirmar que las EA cambian en función de la experiencia de consumo de alcohol. Importancia del proyecto: En el ámbito local no se han realizado estudios sistemáticos de esta naturaleza, la información que se obtenga permitirá evaluar el impacto del uso y abuso de alcohol durante la adolescencia así como diseñar y ejecutar mejores estrategias de prevención y de rehabilitación y, al mismo tiempo, facilitará la toma de decisiones en el campo de la planificación de políticas sanitarias dirigidas a los adolescentes.

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.

Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.