Contribution to Theme A of the Benchmark Workshop: Effect of Concrete Swelling on the Equilibrium and Displacements of an Arch Dam

The Kariba dam is undergoing concrete expansion as a result of an alkali-aggregate reaction. The model adopted to simulate the process is explained in the paper; it is based on the model first proposed by Ulm et al, as later modified by Saouma and Perotti. It has been implemented in the commercial finite element code Abaqus and applied to solve the benchmark problem. The parameters of the model were calibrated using the data recorded up to 1995. The calibrated model was then used for predicting the evolution of the dam up to the present date. Apart from this prediction the paper offers a number of conclusions, such as the fact that the stress level appears to have a major influence on the expansion process; and it presents some suggestions to improve the formulation of the benchmark, such as providing temperature data and widening the locations and conditions of the data employed in the calibration

Experimentel ADS-B based surveillance

This paper describes an ADS-B implementation in air-to-air and ground based experimental surveillance within a prototype ATM system. The relations between airborne and ground systems related to surveillance are detailed, and the prototype surveillance systems and their algorithms described. Their performance is analysed, based both on simulated and real data.

Implementation of safety based incentives in Public Private Partnerships (PPPs): an empirical analysis for the case of Spain

Public Private Partnerships (PPPs) are mostly implemented to circumvent budgetary constraints, and to encourage efficiency and quality in the provision of public infrastructure in order to reach social welfare. One of the ways of reaching the latter objective is by the introduction of performance based standards tied to bonuses and penalties to reward or punish the performance of the contractor. This paper focuses on the implementation of safety based incentives in PPPs in such a way that the better the safety outcome the greater larger will be the economic reward to the contractor. The main aim of this paper is to identify whether the incentives to improve road safety in PPPs are ultimately effective in improving safety ratios in Spain. To that end, Poisson and negative binomial regression models have been applied using information of motorways of the Spanish network of 2006. The findings indicate that even though road safety is highly influenced by variables that are not much controllable by the contractor such as the Average Annual Daily Traffic and the percentage of heavy vehicles, the implementation of safety incentives in PPPs has a positive influence in the reduction of fatalities, injuries and accidents.

Gas sensor based on room temperature optical properties of Surface QDs

Self-organized InGaAs QDs are intensively studied for optoelectronic applications. Several approaches are in study to reach the emission wavelengths needed for these applications. The use of antimony (Sb) in either the capping layer or into the dots is one example. However, these studies are normally focused on buried QD (BQD) where there are still different controversial theories concerning the role of Sb. Ones suggest that Sb incorporates into the dot [1], while others support the hypothesis that the Sb occupies positions surrounding the dot [2] thus helping to keep their shape during the capping growth.

Mid-infrared photodetectors based on GaAsSb-capped InAs quantum dots

Quantum dot infrared photodetectors (QDIPs) are very attractive for many applications such as infrared imaging, remote sensing and gas sensing, thanks to its promising features such as high temperature operation, normal incidence response and low dark current [1]. However, the key issue is to obtain a high-quality active region which requires an optimization of the nanostructure. By using GaAsSb capping layer, InAs QDs have improved their optical emission in the range between 1.15 and 1.3 m (at Sb composition of 14 %), due to a reduction of a compressive strain in QD and an increment of a QD height [2]. In this work, we have demonstrated strong and narrow intraband photoresponses at ~ 5 m from GaAsSb-capped InAs/GaAs QDIPs under normal light-incidence.

An iPhone-based application for promoting type 2 diabetic patients self- management towards healthy lifestyle habits

— In 2000, according to the World Health Organization, at least 171 million people, 2.8% of the population worldwide, suffered from diabetes. The Centres for Disease Control has defined it as an epidemic disease. Its incidence is increasing rapidly, and it is estimated that by 2030 this number will almost double. Diabetes mellitus occurs throughout the world, but is more common (especially type 2) in the more developed countries. Diabetes is a chronic condition that occurs when pancreas does not assure enough insulin secretion or when the body does not consume the insulin produced. Insulin is a hormone that regulates blood sugar. The effect of uncontrolled diabetes is the hyperglycaemia (blood sugar), which eventually seriously damage many organs and systems, especially the nerves and blood vessels. Diabetes type 2 (most common type of diabetes) is highly correlated with elderly people, obesity or overweight. Promoting a healthy lifestyle helps patients to improve their quality of life and in many cases to avoid complications related to the disease. This paper is intended to describe an iPhone-based application for self-management of type 2 diabetic patients, which allow them improving their lifestyle through healthy diet, physical activity and education

FPGA Acceleration of Monte Carlo-based Financial Simulation: Design Challenges and Lessons Learnt

The simulation of interest rate derivatives is a powerful tool to face the current market fluctuations. However, the complexity of the financial models and the way they are processed require exorbitant computation times, what is in clear conflict with the need of a processing time as short as possible to operate in the financial market. To shorten the computation time of financial derivatives the use of hardware accelerators becomes a must.

Self-reference Scrubber for TMR Systems Based on Xilinx Virtex FPGAs

SRAM-based FPGAs are sensitive to radiation effects. Soft errors can appear and accumulate, potentially defeating mitigation strategies deployed at the Application Layer. Therefore, Configuration Memory scrubbing is required to improve radiation tolerance of such FPGAs in space applications. Virtex FPGAs allow runtime scrubbing by means of dynamic partial reconfiguration. Even with scrubbing, intra-FPGA TMR systems are subjected to common-mode errors affecting more than one design domain. This is solved in inter-FPGA TMR systems at the expense of a higher cost, power and mass. In this context, a self-reference scrubber for device-level TMR system based on Xilinx Virtex FPGAs is presented. This scrubber allows for a fast SEU/MBU detection and correction by peer frame comparison without needing to access a golden configuration memory

MBE growth and characterization of InGaN-based films and nanocolumns on Silicon substrates and GaN templates

InN layers: MBE growth issues Growth of InN-based thin films: InN/InGaN QWS on GaN Growth of InN-based nanorods ● Self Self-assembled assembled InN InN nanorods nanorods onon different different substrates substrates ● Self-assembled InGaN nanorods ● Broad- Broad-emission emission nanostructures ● Self Self--assembled assembled InGaN InGaN--based based Qdisks Qdisks ● Selective area growth (SAG) of InGaN Qdisks

Aeronautical Metadata Profile based on Geographic International Standards

The aeronautical information plays an essential rolein air safety, chief objective of the aeronautical industry. Community policies and projects are being currently developed for the adequate management of a single European air space. To make this possible, an appropriate information management and a set of tools that allow sharing and exchanging this information, ensuring its interoperability and integrity, are necessary. This paper presents the development and implementation of a metadata profile for description of the aeronautical information based on international regulations and recommendations applied within the geographic scope. The elements taken into account for its development are described, as well as the implementation process and the results obtained.

Combined static and dynamic assertion-based debugging of constraint logic programs

We propose a general framework for assertion-based debugging of constraint logic programs. Assertions are linguistic constructions for expressing properties of programs. We define several assertion schemas for writing (partial) specifications for constraint logic programs using quite general properties, including user-defined programs. The framework is aimed at detecting deviations of the program behavior (symptoms) with respect to the given assertions, either at compile-time (i.e., statically) or run-time (i.e., dynamically). We provide techniques for using information from global analysis both to detect at compile-time assertions which do not hold in at least one of the possible executions (i.e., static symptoms) and assertions which hold for all possible executions (i.e., statically proved assertions). We also provide program transformations which introduce tests in the program for checking at run-time those assertions whose status cannot be determined at compile-time. Both the static and the dynamic checking are provably safe in the sense that all errors flagged are definite violations of the pecifications. Finally, we report briefly on the currently implemented instances of the generic framework.

Towards a concurrent semantics-based analysis of CC and CLP. principles and practice of constraint programming

Abstract is not available.

Interval-based resource usage verification: Formalization and prototype

In an increasing number of applications (e.g., in embedded, real-time, or mobile systems) it is important or even essential to ensure conformance with respect to a specification expressing resource usages, such as execution time, memory, energy, or user-defined resources. In previous work we have presented a novel framework for data size-aware, static resource usage verification. Specifications can include both lower and upper bound resource usage functions. In order to statically check such specifications, both upper- and lower-bound resource usage functions (on input data sizes) approximating the actual resource usage of the program which are automatically inferred and compared against the specification. The outcome of the static checking of assertions can express intervals for the input data sizes such that a given specification can be proved for some intervals but disproved for others. After an overview of the approach in this paper we provide a number of novel contributions: we present a full formalization, and we report on and provide results from an implementation within the Ciao/CiaoPP framework (which provides a general, unified platform for static and run-time verification, as well as unit testing). We also generalize the checking of assertions to allow preconditions expressing intervals within which the input data size of a program is supposed to lie (i.e., intervals for which each assertion is applicable), and we extend the class of resource usage functions that can be checked.

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.

An abstract interpretation-based approach to mobile code safety

Recent approaches to mobile code safety, like proof- arrying code, involve associating safety information to programs. The code supplier provides a program and also includes with it a certifícate (or proof) whose validity entails compliance with a predefined safety policy. The intended benefit is that the program consumer can locally validate the certifícate w.r.t. the "untrusted" program by means of a certifícate checker—a process which should be much simpler, eflicient, and automatic than generating the original proof. We herein introduce a novel approach to mobile code safety which follows a similar scheme, but which is based throughout on the use of abstract interpretation techniques. In our framework the safety policy is specified by using an expressive assertion language defined over abstract domains. We identify a particular slice of the abstract interpretation-based static analysis results which is especially useful as a certifícate. We propose an algorithm for checking the validity of the certifícate on the consumer side which is itself in fact a very simplified and eflicient specialized abstract-interpreter. Our ideas are illustrated through an example implemented in the CiaoPP system. Though further experimentation is still required, we believe the proposed approach is of interest for bringing the automation and expressiveness which is inherent in the abstract interpretation techniques to the área of mobile code safety.