Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)

The technique of Abstract Interpretation has allowed the development of very sophisticated global program analyses which are at the same time provably correct and practical. We present in a tutorial fashion a novel program development framework which uses abstract interpretation as a fundamental tool. The framework uses modular, incremental abstract interpretation to obtain information about the program. This information is used to validate programs, to detect bugs with respect to partial specifications written using assertions (in the program itself and/or in system libraries), to generate and simplify run-time tests, and to perform high-level program transformations such as multiple abstract specialization, parallelization, and resource usage control, all in a provably correct way. In the case of validation and debugging, the assertions can refer to a variety of program points such as procedure entry, procedure exit, points within procedures, or global computations. The system can reason with much richer information than, for example, traditional types. This includes data structure shape (including pointer sharing), bounds on data structure sizes, and other operational variable instantiation properties, as well as procedure-level properties such as determinacy, termination, nonfailure, and bounds on resource consumption (time or space cost). CiaoPP, the preprocessor of the Ciao multi-paradigm programming system, which implements the described functionality, will be used to illustrate the fundamental ideas.

A Mobile Feedback System for Integrated E-health Platforms to improve Self-Care and Compliance of Diabetes Mellitus Patients

Exploiting the full potential of telemedical systems means using platform based solutions: data are recovered from biomedical sensors, hospital information systems, care-givers, as well as patients themselves, and are processed and redistributed in an either centralized or, more probably, decentralized way. The integration of all these different devices, and interfaces, as well as the automated analysis and representation of all the pieces of information are current key challenges in telemedicine. Mobile phone technology has just begun to offer great opportunities of using this diverse information for guiding, warning, and educating patients, thus increasing their autonomy and adherence to their prescriptions. However, most of these existing mobile solutions are not based on platform systems and therefore represent limited, isolated applications. This article depicts how telemedical systems, based on integrated health data platforms, can maximize prescription adherence in chronic patients through mobile feedback. The application described here has been developed in an EU-funded R&D project called METABO, dedicated to patients with type 1 or type 2 Diabetes Mellitus

Integrated electronic system for ultrasonic structural health monitoring

A fully integrated on-board electronic system that can perform in-situ structural health monitoring (SHM) of aircraft?s structures using specifically designed equipment for SHM based on guided wave ultrasonic method or Lamb waves? method is introduced. This equipment is called Phased Array Monitoring for Enhanced Life Assessment (PAMELA III) and is an essential part of overall PAMELA SHM? system. PAMELA III can generate any kind of excitation signals, acquire the response signals that propagate throughout the structure being tested, and perform the signal processing for damage detection directly on the structure without need to send the huge amount of raw signals but only the final SHM maps. It monitors the structure by means of an array of integrated Phased Array (PhA) transducers preferably bonded onto the host structure. The PAMELA III hardware for SHM mapping has been designed, built and subjected to laboratory tests, using aluminum and CFRP structures. The 12 channel system has been designed to be low weight (265 grams only), to have a small form factor, to be directly mounted above the integrated PhA transducers without need for cables and to be EMI protected so that the equipment can be taken on board an aircraft to perform required SHM analyses by use of embedded SHM algorithms. Moreover, the autonomous, automatic and on real-time working procedure makes it suitable for the avionic field, sending the corresponding alerts, maps and reports to external equipment.

Steady state analysis of a storage integrated solar thermophotovoltaic (SISTPV) system

This paper presents the theoretical analysis of a storage integrated solar thermophotovoltaic (SISTPV) system operating in steady state. These systems combine thermophotovoltaic (TPV) technology and high temperature thermal storage phase-change materials (PCM) in the same unit, providing a great potential in terms of efficiency, cost reduction and storage energy density. The main attraction in the proposed system is its simplicity and modularity compared to conventional Concentrated Solar Power (CSP) technologies. This is mainly due to the absence of moving parts. In this paper we analyze the use of Silicon as the phase change material (PCM). Silicon is an excellent candidate because of its high melting point (1680 K) and its very high latent heat of fusion of 1800 kJ/kg, which is about ten times greater than the conventional PCMs like molten salts. For a simple system configuration, we have demonstrated that overall conversion efficiencies up to ?35% are approachable. Although higher efficiencies are expected by incorporating more advanced devices like multijunction TPV cells, narrow band selective emitters or adopting near-field TPV configurations as well as by enhancing the convective/conductive heat transfer within the PCM. In this paper, we also discuss about the optimum system configurations and provide the general guidelines for designing these systems. Preliminary estimates of night time operations indicate it is possible to achieve over 10 h of operation with a relatively small quantity of Silicon.

A user-focused integrated system for sustainable refurbishment.

Nowadays, it is urgent to renovate a great number of residential buildings. The necessity of improving energy efficiency must also be considered as an opportunity to improve indoor comfort. To achieve this goal, it is essential to develop tools to be used in the decision-making process, aiming to refurbish buildings in an integrated, efficient and sustainable way. The integrated system developed is based on a set of indicators. Sustainability indicators are useful to synthesize and organize complex information. They can provide data to evaluate a process in different stages: evaluation, diagnosis, comparison and tracing. The set of proposed indicators aims to accomplish the holistic approach pursued by sustainable development. So, these indicators are divided into three groups: environmental, social and economic. However, the main innovation of the system of indicators is the social ones. The sustainable refurbishment system aims to be a user-focused one. Therefore, the starting point is the needs of the user and social indicators are developed around this. The system tackles the sustainable refurbishment of buildings beyond energy problems. It proposes incorporating users in the decision-making process involving them in the refurbishment and so, contributing to the success of the renovation. In order to achieve this target, three social indicators are used, divided into 10 sub-indicators, and a ?Questionnaire about Sustainable Refurbishment? is drawn up. This research has been carried out in the framework of ?Sustainable Refurbishment? Research and Development Project, an integrated project under the supervision of the Centro para el Desarrollo Tecnológico e Industrial (CDTI) from the Spanish Government, in which University and the Construction Industry collaborate. This research project aims to develop an integrated system for the retrofitting of existing buildings to improve their energy efficiency. Accordingly, an additional objective of the project is to improve quality of life of residents.

Preliminary results of ON/OFF detection using an integrated system for Parkinson's disease monitoring

This paper describes the experimental set up of a system composed by a set of wearable sensors devices for the recording of the motion signals and software algorithms for the signal analysis. This system is able to automatically detect and assess the severity of bradykinesia, tremor, dyskinesia and akinesia motor symptoms. Based on the assessment of the akinesia, the ON-OFF status of the patient is determined for each moment. The assessment performed through the automatic evaluation of the akinesia is compared with the status reported by the patients in their diaries. Preliminary results with a total recording period of 32 hours with two PD patients are presented, where a good correspondence (88.2 +/- 3.7 %) was observed. Best (93.7 por ciento) and worst (87 por ciento) correlation results are illustrated, together with the analysis of the automatic assessment of the akinesia symptom leading to the status determination. The results obtained are promising, and if confirmed with further data, this automatic assessment of PD motor symptoms will lead to a better adjustment of medication dosages and timing, cost savings and an improved quality of life of the patients.

Night time performance of a storage integrated solar thermophotovoltaic (SISTPV) system

Energy storage at low maintenance cost is one of the key challenges for generating electricity from the solar energy. This paper presents the theoretical analysis (verified by CFD) of the night time performance of a recently proposed conceptual system that integrates thermal storage (via phase change materials) and thermophotovoltaics for power generation. These storage integrated solar thermophotovoltaic (SISTPV) systems are attractive owing to their simple design (no moving parts) and modularity compared to conventional Concentrated Solar Power (CSP) technologies. Importantly, the ability of high temperature operation of these systems allows the use of silicon (melting point of 1680 K) as the phase change material (PCM). Silicon's very high latent heat of fusion of 1800 kJ/kg and low cost ($1.70/kg), makes it an ideal heat storage medium enabling for an extremely high storage energy density and low weight modular systems. In this paper, the night time operation of the SISTPV system optimised for steady state is analysed. The results indicate that for any given PCM length, a combination of small taper ratio and large inlet hole-to-absorber area ratio are essential to increase the operation time and the average power produced during the night time. Additionally, the overall results show that there is a trade-off between running time and the average power produced during the night time. Average night time power densities as high as 30 W/cm(2) are possible if the system is designed with a small PCM length (10 cm) to operate just a few hours after sun-set, but running times longer than 72 h (3 days) are possible for larger lengths (50 cm) at the expense of a lower average power density of about 14 W/cm(2). In both cases the steady state system efficiency has been predicted to be about 30%. This makes SISTPV systems to be a versatile solution that can be adapted for operation in a broad range of locations with different climate conditions, even being used off-grid and in space applications.

A system for functional analysis of Ebola virus glycoprotein

Ebola virus causes hemorrhagic fever in humans and nonhuman primates, resulting in mortality rates of up to 90%. Studies of this virus have been hampered by its extraordinary pathogenicity, which requires biosafety level 4 containment. To circumvent this problem, we developed a novel complementation system for functional analysis of Ebola virus glycoproteins. It relies on a recombinant vesicular stomatitis virus (VSV) that contains the green fluorescent protein gene instead of the receptor-binding G protein gene (VSVΔG*). Herein we show that Ebola Reston virus glycoprotein (ResGP) is efficiently incorporated into VSV particles. This recombinant VSV with integrated ResGP (VSVΔG*-ResGP) infected primate cells more efficiently than any of the other mammalian or avian cells examined, in a manner consistent with the host range tropism of Ebola virus, whereas VSVΔG* complemented with VSV G protein (VSVΔG*-G) efficiently infected the majority of the cells tested. We also tested the utility of this system for investigating the cellular receptors for Ebola virus. Chemical modification of cells to alter their surface proteins markedly reduced their susceptibility to VSVΔG*-ResGP but not to VSVΔG*-G. These findings suggest that cell surface glycoproteins with N-linked oligosaccharide chains contribute to the entry of Ebola viruses, presumably acting as a specific receptor and/or cofactor for virus entry. Thus, our VSV system should be useful for investigating the functions of glycoproteins from highly pathogenic viruses or those incapable of being cultured in vitro.

The insect endosymbiont Sodalis glossinidius utilizes a type III secretion system for cell invasion

Sodalis glossinidius is a maternally transmitted secondary endosymbiont residing intracellularly in tissues of the tsetse flies, Glossina spp. In this study, we have used Tn5 mutagenesis and a negative selection procedure to derive a S. glossinidius mutant that is incapable of invading insect cells in vitro and is aposymbiotic when microinjected into tsetse. This mutant strain harbors Tn5 integrated into a chromosomal gene sharing high sequence identity with a type III secretion system invasion gene (invC) previously identified in Salmonella enterica. With the use of degenerate PCR, we have amplified a further six Sodalis inv/spa genes sharing high sequence identity with type III secretion system genes encoded by Salmonella pathogenicity island 1. Phylogenetic reconstructions based on the inv/spa genes of Sodalis and other members of the family Enterobacteriaceae have consistently identified a well-supported clade containing Sodalis and the enteric pathogens Shigella and Salmonella. These results suggest that Sodalis may have evolved from an ancestor with a parasitic intracellular lifestyle, possibly a latter-day entomopathogen. These observations lend credence to a hypothesis suggesting that vertically transmitted mutualistic endosymbionts evolve from horizontally transmitted parasites through a parasitism–mutualism continuum.

Magnetic resonance microscopy and spectroscopy reveal kinetics of cryoprotectant permeation in a multicompartmental biological system.

Successful cryopreservation of most multicompartmental biological systems has not been achieved. One prerequisite for success is quantitative information on cryoprotectant permeation into and amongst the compartments. This report describes direct measurements of cryoprotectant permeation into a multicompartmental system using chemical shift selective magnetic resonance (MR) microscopy and MR spectroscopy. We used the developing zebrafish embryo as a model for studying these complex systems because these embryos are composed of two membrane-limited compartments: (i) a large yolk (surrounded by the yolk syncytial layer) and (ii) differentiating blastoderm cells (each surrounded by a plasma membrane). MR images of the spatial distribution of three cryoprotectants (dimethyl sulfoxide, propylene glycol, and methanol) demonstrated that methanol permeated the entire embryo within 15 min. In contrast, the other cryoprotectants exhibited little or no permeation over 2.5 h. MR spectroscopy and microinjections of cryoprotectants into the yolk inferred that the yolk syncytial layer plays a critical role in limiting the permeation of some cryoprotectants throughout the embryo. This study demonstrates the power of MR technology combined with micromanipulation for elucidating key physiological factors in cryobiology.

Study of interaction between Si(O,C) nanowires and the biological system

Nanomedicine is a new branch of medicine, based on the potentiality and intrinsic properties of nanomaterials. Indeed, the nanomaterials ( i.e. the materials with nano and under micron size) can be suitable to different applications in biomedicine. The nanostructures can be used by taking advantage of their properties (for example superparamagnetic nanoparticles) or functionalized to deliver the drug in a specific target, thanks the ability to cross biological barriers. The size and the shape of 1D-nanostructures (nanotubes and nanowires) have an important role on the cell fate: their morphology plays a key role on the interaction between nanostructure and the biological system. For this reason the 1D nanostructure are interesting for their ability to mime the biological system. An implantable material or device must therefore integrate with the surrounding extracellular matrix (ECM), a complex network of proteins with structural and signaling properties. Innovative techniques allow the generation of complex surface patterns that can resemble the structure of the ECM, such as 1D nanostructures. NWs based on cubic silicon carbide (3C-SiC), either bare (3C-SiC NWs) or surrounded by an amorphous shell (3C-SiC/SiO2 core/shell NWs), and silicon oxycarbide nanowires (SiOxCy NWs) can meet the chemical, mechanical and electrical requirements for tissue engineering and have a strong potential to pave the way for the development of a novel generation of implantable nano-devices. Silicon oxycarbide shows promising physical and chemical properties as elastic modulus, bending strength and hardness, chemical durability superior to conventional silicate glasses in aggressive environments and high temperature stability up to 1300 °C. Moreover, it can easily be engineered through functionalization and decoration with macro-molecules and nanoparticles. Silicon carbide has been extensively studied for applications in harsh conditions, as chemical environment, high electric field and high and low temperature, owing to its high hardness, high thermal conductivity, chemical inertness and high electron mobility. Also, its cubic polytype (3C) is highly biocompatible and hemocompatible, and some prototypes of biomedical applications and biomedical devices have been already realized starting from 3C-SiC thin films. Cubic SiC-based NWs can be used as a biomimetic biomaterial, providing a robust and novel biocompatible biological interface . We cultured in vitro A549 human lung adenocarcinoma epithelial cells and L929 murine fibroblast cells over core/shell SiC/SiO2, SiOxCy and bare 3C-SiC nanowire platforms, and analysed the cytotoxicity, by indirect and direct contact tests, the cell adhesion, and the cell proliferation. These studies showed that all the nanowires are biocompatible according to ISO 10993 standards. We evaluated the blood compatibility through the interaction of the nanowires with platelet rich plasma. The adhesion and activation of platelets on the nanowire bundles, assessed via SEM imaging and soluble P-selectin quantification, indicated that a higher platelet activation is induced by the core/shell structures compared to the bare ones. Further, platelet activation is higher with 3C-SiC/SiO2 NWs and SiOxCyNWs, which therefore appear suitable in view of possible tissue regeneration. On the contrary, bare 3C-SiC NWs show a lower platelet activation and are therefore promising in view of implantable bioelectronics devices, as cardiovascular implantable devices. The NWs properties are suitable to allow the design of a novel subretinal Micro Device (MD). This devices is based on Si NWs and PEDOT:PSS, though the well know principle of the hybrid ordered bulk heterojunction (OBHJ). The aim is to develop a device based on a well-established photovoltaic technology and to adapt this know-how to the prosthetic field. The hybrid OBHJ allows to form a radial p–n junction on a nanowire/organic structure. In addition, the nanowires increase the light absorption by means of light scattering effects: a nanowires based p-n junction increases the light absorption up to the 80%, as previously demonstrated, overcoming the Shockley-Queisser limit of 30 % of a bulk p-n junction. Another interesting employment of these NWs is to design of a SiC based epicardial-interacting patch based on teflon that include SiC nanowires. . Such contact patch can bridge the electric conduction across the cardiac infarct as nanowires can ‘sense’ the direction of the wavefront propagation on the survival cardiac tissue and transmit it to the downstream surivived regions without discontinuity. The SiC NWs are tested in terms of toxicology, biocompatibility and conductance among cardiomyocytes and myofibroblasts.

Implementing an Integrated Management System (IMS) at an Aerospace Manufacturing Facility

This project analyzes the challenges, issues, benefits, and lessons learned that several companies experienced while implementing integrated management systems. Based on previous experiences, this paper defines several strategies that an organization should use to increase the probability of implementing an integrated management system (IMS) successfully. Strategies include completing a feasibility analysis, creating a policy, allocating resources, developing objectives, modifying documentation, and creating a continuous monitoring process. Moreover, an organization can reduce potential obstacles by promoting a culture that encourages management commitment and employee participation. Results indicate the implementation of an IMS provides the framework to manage environmental, health, and safety programs effectively. By implementing an IMS, an organization can save time and money, as well as proactively control risk.

Evaluation of an integrated system for classification, assessment and comparison of services for long-term care in Europe: the eDESDE-LTC study

Background: The harmonization of European health systems brings with it a need for tools to allow the standardized collection of information about medical care. A common coding system and standards for the description of services are needed to allow local data to be incorporated into evidence-informed policy, and to permit equity and mobility to be assessed. The aim of this project has been to design such a classification and a related tool for the coding of services for Long Term Care (DESDE-LTC), based on the European Service Mapping Schedule (ESMS). Methods: The development of DESDE-LTC followed an iterative process using nominal groups in 6 European countries. 54 researchers and stakeholders in health and social services contributed to this process. In order to classify services, we use the minimal organization unit or “Basic Stable Input of Care” (BSIC), coded by its principal function or “Main Type of Care” (MTC). The evaluation of the tool included an analysis of feasibility, consistency, ontology, inter-rater reliability, Boolean Factor Analysis, and a preliminary impact analysis (screening, scoping and appraisal). Results: DESDE-LTC includes an alpha-numerical coding system, a glossary and an assessment instrument for mapping and counting LTC. It shows high feasibility, consistency, inter-rater reliability and face, content and construct validity. DESDE-LTC is ontologically consistent. It is regarded by experts as useful and relevant for evidence-informed decision making. Conclusion: DESDE-LTC contributes to establishing a common terminology, taxonomy and coding of LTC services in a European context, and a standard procedure for data collection and international comparison.