Context-sensitive multivariant assertion checking in modular programs

We propose a modular, assertion-based system for verification and debugging of large logic programs, together with several interesting models for checking assertions statically in modular programs, each with different characteristics and representing different trade-offs. Our proposal is a modular and multivariant extensión of our previously proposed abstract assertion checking model and we also report on its implementation in the CiaoPP system. In our approach, the specification of the program, given by a set of assertions, may be partial, instead of the complete specification required by raditional verification systems. Also, the system can deal with properties which cannot always be determined at compile-time. As a result, the proposed system needs to work with safe approximations: all assertions proved correct are guaranteed to be valid and all errors actual errors. The use of modular, context-sensitive static analyzers also allows us to introduce a new distinction between assertions checked in a particular context or checked in general.

Experiments in context-sensitive analysis of modular programs

Several models for context-sensitive analysis of modular programs have been proposed, each with different characteristics and representing different trade-offs. The advantage of these context-sensitive analyses is that they provide information which is potentially more accurate than that provided by context-free analyses. Such information can then be applied to validating/debugging the program and/or to specializing the program in order to obtain important performance improvements. Some very preliminary experimental results have also been reported for some of these models which provided initial evidence on their potential. However, further experimentation, which is needed in order to understand the many issues left open and to show that the proposed modes scale and are usable in the context of large, real-life modular programs, was left as future work. The aim of this paper is two-fold. On one hand we provide an empirical comparison of the different models proposed in previous work, as well as experimental data on the different choices left open in those designs. On the other hand we explore the scalability of these models by using larger modular programs as benchmarks. The results have been obtained from a realistic implementation of the models, integrated in a production-quality compiler (CiaoPP/Ciao). Our experimental results shed light on the practical implications of the different design choices and of the models themselves. We also show that contextsensitive analysis of modular programs is indeed feasible in practice, and that in certain critical cases it provides better performance results than those achievable by analyzing the whole program at once, specially in terms of memory consumption and when reanalyzing after making changes to a program, as is often the case during program development.

A generic framework for context-sensitive analysis of modular programs

Context-sensitive analysis provides information which is potentially more accurate than that provided by context-free analysis. Such information can then be applied in order to validate/debug the program and/or to specialize the program obtaining important improvements. Unfortunately, context-sensitive analysis of modular programs poses important theoretical and practical problems. One solution, used in several proposals, is to resort to context-free analysis. Other proposals do address context-sensitive analysis, but are only applicable when the description domain used satisfies rather restrictive properties. In this paper, we argüe that a general framework for context-sensitive analysis of modular programs, Le., one that allows using all the domains which have proved useful in practice in the non-modular setting, is indeed feasible and very useful. Driven by our experience in the design and implementation of analysis and specialization techniques in the context of CiaoPP, the Ciao system preprocessor, in this paper we discuss a number of design goals for context-sensitive analysis of modular programs as well as the problems which arise in trying to meet these goals. We also provide a high-level description of a framework for analysis of modular programs which does substantially meet these objectives. This framework is generic in that it can be instantiated in different ways in order to adapt to different contexts. Finally, the behavior of the different instantiations w.r.t. the design goals that motivate our work is also discussed.

A generic, context sensitive analysis framework for object oriented programs

Abstract interpreters rely on the existence of a nxpoint algorithm that calculates a least upper bound approximation of the semantics of the program. Usually, that algorithm is described in terms of the particular language in study and therefore it is not directly applicable to programs written in a different source language. In this paper we introduce a generic, block-based, and uniform representation of the program control flow graph and a language-independent nxpoint algorithm that can be applied to a variety of languages and, in particular, Java. Two major characteristics of our approach are accuracy (obtained through a topdown, context sensitive approach) and reasonable efficiency (achieved by means of memoization and dependency tracking techniques). We have also implemented the proposed framework and show some initial experimental results for standard benchmarks, which further support the feasibility of the solution adopted.

Modulation instability-induced fading in phase-sensitive optical time-domain reflectometry

Phase-sensitive optical time-domain reflectometry (?OTDR) is a simple and effective tool allowing the distributed monitoring of vibrations along single-mode fibers. We show in this Letter that modulation instability (MI) can induce a position-dependent signal fading in long-range ?OTDR over conventional optical fibers. This fading leads to a complete masking of the interference signal recorded at certain positions and therefore to a sensitivity loss at these positions. We illustrate this effect both theoretically and experimentally. While this effect is detrimental in the context of distributed vibration analysis using ?OTDR, we also believe that the technique provides a clear and insightful way to evidence the Fermi?Pasta?Ulam recurrence associated with the MI process.

I feel you: Towards affect-sensitive domotic Spoken Conversational Agents

We describe the work on infusion of emotion into limitedtask autonomous spoken conversational agents (SCAs) situated in the domestic environment, using a Need-inspired task-independentEmotion model (NEMO). In order to demonstrate the generation of a?ect through the use of the model, we describe the work of integrating it with a naturallanguage mixed-initiative HiFi-control SCA. NEMO and the host system communicates externally, removing the need for the Dialog Manager to be modi?ed as done in most existing dialog systems, in order to be adaptive. We also summarize the work on automatic a?ect prediction, namely frustration and contentment from dialog features, a non-conventional source, in the attempt of moving towards a more user-centric approach.

Ion-temperature-sensitive effect in transient langmuir probe response

A theory is presented for a method, recently proposed by Hester and Sonin, of determining the ion temperature in a plasma by measuring the transient current to a cylindrical Langmuir probe after applying a potential Vp{ — eVpy>KTe) under conditions where collection is collision free and the ratio of probe radius to Debye length is small. The ion component of the current does not approach its final steady-state value monotonicalfy, but exhibits a strong, ion-temperature-dependent overshoot in the first few ion-plasma periods following the biasing of the probe. Analytical formulas are derived for the case of a Maxwellian plasma, and convenient graphical results are presented. The possible masking of the overshoot by a transient displacement current is discussed; it is shown how to avoid such displacement effects. For the overshoot to be sensitive to the ion temperature T the probe must be near plasma (zero) potential before applying V1,(eVp~<0.lKTe, VP~ being that initial potential); this is not a drawback of the method, but, on the contrary, it can be used to accurately determine plasma potential along with T.

I feel you: the design and evaluation of a domotic affect-sensitive spoken conversational agent

We describe the work on infusion of emotion into a limited-task autonomous spoken conversational agent situated in the domestic environment, using a need-inspired task-independent emotion model (NEMO). In order to demonstrate the generation of affect through the use of the model, we describe the work of integrating it with a natural-language mixed-initiative HiFi-control spoken conversational agent (SCA). NEMO and the host system communicate externally, removing the need for the Dialog Manager to be modified, as is done in most existing dialog systems, in order to be adaptive. The first part of the paper concerns the integration between NEMO and the host agent. The second part summarizes the work on automatic affect prediction, namely, frustration and contentment, from dialog features, a non-conventional source, in the attempt of moving towards a more user-centric approach. The final part reports the evaluation results obtained from a user study, in which both versions of the agent (non-adaptive and emotionally-adaptive) were compared. The results provide substantial evidences with respect to the benefits of adding emotion in a spoken conversational agent, especially in mitigating users' frustrations and, ultimately, improving their satisfaction.

Accessible interaction solution based on confidence for the deployment of pervasive sensitive services in intelligent environments

Los servicios basados en las Tecnologías de la Información y las Comunicaciones (TIC) están cada vez más presentes en la vida de las personas. El avance de las TIC en términos técnicos y de aceptación social ha dado lugar la creación de nuevos modelos de provisión de servicios. Estos modelos de servicio implican una mayor integración con las actividades de las personas de forma que ya no solo están presentes en su ámbito profesional o de espacio ciudadano sino también en un ámbito más íntimo relacionado con su propia identidad. Así en la actualidad es común encontrar servicios conocedores del estado de salud de las personas, sus hábitos domésticos, su ideología, etc. Por tanto el análisis de los servicios actuales no puede limitarse a una componente técnica sino que es más necesario que nunca la inclusión de aspectos más relacionados con la forma de ser y sentir de sus usuarios. De esta forma no solo se garantizará la corrección técnica de sus funcionalidades sino que también se fomentará la generación de soluciones cívicamente seguras y respetuosas tanto con los derechos como con la forma de ser y sentir de sus usuarios. Desde el punto de vista de ingeniería, la perspectiva del usuario se ha englobado históricamente bajo el concepto de aceptación tecnológica. Dentro de este ámbito se puede interpretar que soluciones respetuosas y adaptadas a los usuarios fomentarán la aceptación por parte de éstos. La aceptación de una solución es algo deseable si bien es difícil de asegurar. Esta dificultad es debida al desconocimiento del número de variables que afectan a la aceptación de soluciones tecnológicas y a la dificultad de optimización de las variables conocidas. En esta tesis doctoral se estudia y caracteriza una de las variables que afecta a la aceptación de los servicios actuales: la confianza. Se define la confianza en términos psicológicos caracterizándola para permitir su uso en los métodos propios de la ingeniería. Además se proponen distintas herramientas que facilitan la optimización de la confianza en servicios cuya complejidad convierte a esta variable en una cuestión básica para mejorar la aceptación. Como contexto de trabajo para la tesis se ha escogido un servicio de salud desplegado en un hogar. Este escenario presenta una serie de restricciones de aceptación relativas a la tecnología utilizada para la creación de los servicios y la forma en que éstos gestionan la información adquirida del usuario. Se trata de servicios altamente sensibles y deslocalizados que pueden afectar a la percepción del usuario sobre el entorno, el hogar, y generar temores o rechazos que impidan su adopción final como solución válida. Una vez definido el marco genérico de trabajo, el objetivo principal de esta tesis doctoral se concreta en contribuir al fomento de la aceptación de nuevos servicios de salud pervasivos y personalizados y su despliegue en entornos inteligentes domésticos mediante un marco de diseño que promueva un estado psicológico de confianza en los usuarios. Para lograr abordar correctamente este objetivo se han proporcionado una serie de resultados tanto a nivel conceptual como tecnológico y experimental. En concreto se ha ofrecido una caracterización completa del sentimiento de confianza desde un punto de vista de ingeniería y una definición del concepto de servicio sensible deslocalizado o pervasivo. Además se ofrece un método para la inclusión del Diseño de Interacción, herramienta muy relacionada con la mejora de las variables de aceptación de tecnología, en los procesos de ingeniería de este tipo de servicios mediante un conjunto de patrones de interacción Persona – Entorno Inteligente. Finalmente se ha proporcionado el desarrollo de una arquitectura software para garantizar el correcto despliegue de estos servicios sensibles pervasivos en espacios inteligentes de una forma confiable. La discusión de los resultados obtenidos sugiere la extensión del modelo a diferentes servicios de la Sociedad de la Información que manejen datos sensibles tanto en el contexto del Hogar Digital como otros contextos donde el usuario realice actividades cotidianas, como los espacios de trabajo o los centros educativos. Las líneas de trabajo futuras contemplan la necesidad inminente de aplicar los resultados a desarrollos en curso, dentro de proyectos de investigación en los que participa el autor así como el desarrollo de nuevas líneas de investigación orientadas a la generación de nuevos espacios y tecnologías de interacción como el Colegio Digital, juguetes del futuro, sistemas de visualización confiables o sistemas de seguridad basados en el estado de las personas.

Sensitive detection of major food allergens in breast milk: first gateway for allergenic contact during breastfeeding

Food allergy is recognized as a major public health issue, especially in early childhood. It has been hypothesized that early sensitization to food allergens maybe due to their ingestion as components dissolved in the milk during the breastfeeding, explaining reaction to a food, which has never been taken before. Thus, the aim of this work has been to detect the presence of the food allergens in breast milk by microarray technology. We produced a homemade microarray with antibodies produced against major food allergens. The antibody microarray was incubated with breast milk from 14 women collected from Fundación Jiménez Díaz Hospital. In this way, we demonstrated the presence of major foods allergens in breast milk. The analysis of allergens presented in breast milk could be a useful tool in allergy prevention and could provide us a key data on the role of this feeding in tolerance induction or sensitization in children.