Experiments in abstract interpretation-based code certification for pervasive systems

Proof carrying code (PCC) is a general is originally a roof in ñrst-order logic of certain vermethodology for certifying that the execution of an un- ification onditions and the checking process involves trusted mobile code is safe. The baste idea is that the ensuring that the certifícate is indeed a valid ñrst-order code supplier attaches a certifícate to the mobile code proof. which the consumer checks in order to ensure that the The main practical difñculty of PCC techniques is in code is indeed safe. The potential benefit is that the generating safety certiñeates which at the same time: i) consumer's task is reduced from the level of proving to allow expressing interesting safety properties, ii) can be the level of checking. Recently, the abstract interpre- generated automatically and, iii) are easy and efficient tation techniques developed, in logic programming have to check. In [1], the abstract interpretation techniques been proposed as a basis for PCC. This extended ab- [5] developed in logic programming1 are proposed as stract reports on experiments which illustrate several is- a basis for PCC. They offer a number of advantages sues involved in abstract interpretation-based certifica- for dealing with the aforementioned issues. In particution. First, we describe the implementation of our sys- lar, the xpressiveness of existing abstract domains will tem in the context of CiaoPP: the preprocessor of the be implicitly available in abstract interpretation-based Ciao multi-paradigm programming system. Then, by code certification to deñne a wide range of safety propermeans of some experiments, we show how code certifi- ties. Furthermore, the approach inherits the automation catión is aided in the implementation of the framework. and inference power of the abstract interpretation en- Finally, we discuss the application of our method within gines used in (Constraint) Logic Programming, (C)LP. the área, of pervasive systems

Abstract interpretation-based code certification for pervasive systems: Preliminary experiments

Proof carrying code is a general methodology for certifying that the execution of an untrusted mobile code is safe, according to a predefined safety policy. The basic idea is that the code supplier attaches a certifícate (or proof) to the mobile code which, then, the consumer checks in order to ensure that the code is indeed safe. The potential benefit is that the consumer's task is reduced from the level of proving to the level of checking, a much simpler task. Recently, the abstract interpretation techniques developed in logic programming have been proposed as a basis for proof carrying code [1]. To this end, the certifícate is generated from an abstract interpretation-based proof of safety. Intuitively, the verification condition is extracted from a set of assertions guaranteeing safety and the answer table generated during the analysis. Given this information, it is relatively simple and fast to verify that the code does meet this proof and so its execution is safe. This extended abstract reports on experiments which illustrate several issues involved in abstract interpretation-based code certification. First, we describe the implementation of our system in the context of CiaoPP: the preprocessor of the Ciao multi-paradigm (constraint) logic programming system. Then, by means of some experiments, we show how code certification is aided in the implementation of the framework. Finally, we discuss the application of our method within the área of pervasive systems which may lack the necessary computing resources to verify safety on their own. We herein illustrate the relevance of the information inferred by existing cost analysis to control resource usage in this context. Moreover, since the (rather complex) analysis phase is replaced by a simpler, efficient checking process at the code consumer side, we believe that our abstract interpretation-based approach to proof-carrying code becomes practically applicable to this kind of systems.

Efficient spatio-temporal hole filling strategy for Kinect depth maps

In this paper we present an efficient hole filling strategy that improves the quality of the depth maps obtained with the Microsoft Kinect device. The proposed approach is based on a joint-bilateral filtering framework that includes spatial and temporal information. The missing depth values are obtained applying iteratively a joint-bilateral filter to their neighbor pixels. The filter weights are selected considering three different factors: visual data, depth information and a temporal-consistency map. Video and depth data are combined to improve depth map quality in presence of edges and homogeneous regions. Finally, the temporal-consistency map is generated in order to track the reliability of the depth measurements near the hole regions. The obtained depth values are included iteratively in the filtering process of the successive frames and the accuracy of the hole regions depth values increases while new samples are acquired and filtered

Plataforma terapeútica basada en Kinect para niños con parálisis cerebral infantil

El sistema SONRIE (Sistema de terapia, basadO en KiNect, paRa nIños con parálisis cErebral), realizado como Proyecto Fin de Grado por Dña. Estefanía Sampedro Sánchez, se desarrolló con el fin de permitir el proceso de rehabilitación de los músculos faciales en niños con Parálisis Cerebral Infantil (PCI). SONRIE se compone de una plataforma de juegos cuyo objetivo es lograr una mejora terapéutica en la musculatura orofacial de niños diagnosticados de PCI con edades comprendidas entre los 4 y los 12 años. El escenario de aplicación del sistema SONRIE son las escuelas de integración que tienen escolarizados alumnos diagnosticados con este trastorno. La posibilidad de rehabilitación de los músculos faciales mediante tratamientos que se apoyan en el uso de sistemas telemáticos, junto con el empleo de tecnologías actuales (Realidad Virtual, Realidad Aumentada y Serious Games) supone una gran innovación en el entorno de la neuro-rehabilitación, entendida como el proceso de terapia que permite optimizar la participación de una persona en la sociedad, alcanzando un grado de bienestar óptimo. El trabajo realizado en este Proyecto Fin de Grado pretende escalar el sistema SONRIE, mediante el análisis, diseño y desarrollo de un Framework encargado de facilitar, ampliar y validar el uso adecuado del sistema SONRIE en entornos escolares a través de la integración de nuevas tecnologías. La plataforma desarrollada en este proyecto, permite dotar de dinamismo y persistencia a la plataforma de juegos, ofreciendo a los usuarios de SONRIE (principalmente fisioterapeutas y rehabilitadores que trabajan en entornos escolares) un sistema de terapia para niños con PCI accesible vía web. En este Proyecto Fin de Grado se describe el conjunto de componentes software desarrollados con el fin de proporcionar un entorno web que escale el sistema SONRIE, convirtiéndolo en un sistema de terapia efectivo, completo y usable. ABSTRACT. The SONRIE system (Sistema de terapia, basadO en KiNect, paRa nIños con parálisis cErebral), performed as a final project by Miss Estefanía Sampedro, was developed in order to allow the rehabilitation process of the facial muscles of children with Cerebral Palsy (CP). SONRIE consists of a gaming platform which aims to achieve a therapeutic improvement in the orofacial musculature on children diagnosed with CP aged between 4 and 12 years. The application scenario of the SONRIE system are the integration schools that have students diagnosed with this disorder. The possibility of rehabilitation of facial muscles through treatments based on the use of telematics systems, together with the use of new technologies (Virtual Reality, Augmented Reality and Serious Games) is a great innovation in the neuro-rehabilitation environment, understood as the therapy process that optimizes the participation of a person in the society, reaching an optimum level of welfare. The work done in this final project aims to scale the SONRIE system, through the analysis, design and development of a framework in charge of facilitating, extending and validating the proper use of the SONRIE system in school environments, through the integration of new technologies. The platform developed in this project, can provide dynamism and persistence to the gaming platform, offering to the SONRIE users (mainly physiotherapists and rehabilitators who work in school settings) a therapy system for children with CP accessible via web. In this final project are described the software components developed in order to provide a web environment that scales the SONRIE system, making it an effective, complete and usable therapy system.