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.

The CIAO Multi-Dialect Compiler and System: An Experimentation Workbench for Future (C)LP Systems

CIAO is an advanced programming environment supporting Logic and Constraint programming. It offers a simple concurrent kernel on top of which declarative and non-declarative extensions are added via librarles. Librarles are available for supporting the ISOProlog standard, several constraint domains, functional and higher order programming, concurrent and distributed programming, internet programming, and others. The source language allows declaring properties of predicates via assertions, including types and modes. Such properties are checked at compile-time or at run-time. The compiler and system architecture are designed to natively support modular global analysis, with the two objectives of proving properties in assertions and performing program optimizations, including transparently exploiting parallelism in programs. The purpose of this paper is to report on recent progress made in the context of the CIAO system, with special emphasis on the capabilities of the compiler, the techniques used for supporting such capabilities, and the results in the áreas of program analysis and transformation already obtained with the system.

Towards modular extensions for a modular language

Modularity allows the construction of complex designs from simpler, independent units that most of the time can be developed separately. In this paper we are concerned with developing mechanisms for easily implementing modular extensions to modular (logic) languages. By (language) extensions we refer to different groups of syntactic definitions and translation rules that extend a language. Our application of the concept of modularity in this context is twofold. We would like these extensions to be modular, in the above sense, i.e., we should be able to develop different extensions mostly separately. At the same time, the sources and targets for the extensions are modular languages, i.e., such extensions may take as input separate pieces of code and also produce separate pieces of code. Dealing with this double requirement involves interesting challenges to ensure that modularity is not broken: first, combinations of extensions (as if they were a single extension) must be given a precise meaning. Also, the separate translation of multiple sources (as if they were a single source) must be feasible. We present a detailed description of a code expansion-based framework that proposes novel solutions for these problems. We argue that the approach, while implemented for Ciao, can be adapted for other languages and Prolog-based systems.

E-learning systems support of collaborative agreements: a theoretical model

This paper introduces a theoretical model for developing integrated degree programmes through e-learning systems as stipulated by a collaboration agreement signed by two universities. We have analysed several collaboration agreements between universities at the national, European, and transatlantic level as well as various e-learning frameworks. A conceptual model, a business model, and the architecture design are presented as part of the theoretical model. The paper presents a way of implementing e-learning systems as a tool to support inter-institutional degree collaborations, from the signing of the collaborative agreement to the implementation of the necessary services. In order to show how the theory can be tested one sample scenario is presented.

Detection and Isolation of Simultaneous Additive and Parametric Faults in Nonlinear Stochastic Dynamical Systems

This paper presents a new fault detection and isolation scheme for dealing with simultaneous additive and parametric faults. The new design integrates a system for additive fault detection based on Castillo and Zufiria, 2009 and a new parametric fault detection and isolation scheme inspired in Munz and Zufiria, 2008 . It is shown that the so far existing schemes do not behave correctly when both additive and parametric faults occur simultaneously; to solve the problem a new integrated scheme is proposed. Computer simulation results are presented to confirm the theoretical studies.

The new challenges of end-of-life tyres management systems: a Spanish case study

Directive 2008/98/EC released by the European Union represents a significant step forward in all relevant aspects of waste management. Under the already established, extended produced responsibility (EPR) principle, new policies have been enunciated to continuously achieve better overall environmental performance of key products throughout their life phases. This paper discusses how the directive is being articulated in Spain by the main integrated management system (IMS) for end-of-life (EOL) tyres since its creation in 2006. Focusing on the IMS technological, economic and legal aspects, the study provides a global perspective and evaluation of how the IMS is facing the current issues to resolve, the new challenges that have appeared and the management vision for the coming years.

ARGoS: a modular, multi-engine simulator for heterogeneous swarm robotics

We present ARGoS, a novel open source multi-robot simulator. The main design focus of ARGoS is the real-time simulation of large heterogeneous swarms of robots. Existing robot simulators obtain scalability by imposing limitations on their extensibility and on the accuracy of the robot models. By contrast, in ARGoS we pursue a deeply modular approach that allows the user both to easily add custom features and to allocate computational resources where needed by the experiment. A unique feature of ARGoS is the possibility to use multiple physics engines of different types and to assign them to different parts of the environment. Robots can migrate from one engine to another transparently. This feature enables entirely novel classes of optimizations to improve scalability and paves the way for a new approach to parallelism in robotics simulation. Results show that ARGoS can simulate about 10,000 simple wheeled robots 40% faster than real-time.

Assortative and modular networks are shaped by adaptive synchronization processes

Modular organization and degree-degree correlations are ubiquitous in the connectivity structure of biological, technological, and social interacting systems. So far most studies have concentrated on unveiling both features in real world networks, but a model that succeeds in generating them simultaneously is needed. We consider a network of interacting phase oscillators, and an adaptation mechanism for the coupling that promotes the connection strengths between those elements that are dynamically correlated. We show that, under these circumstances, the dynamical organization of the oscillators shapes the topology of the graph in such a way that modularity and assortativity features emerge spontaneously and simultaneously. In turn, we prove that such an emergent structure is associated with an asymptotic arrangement of the collective dynamical state of the network into cluster synchronization.

Employment rate impacts of charging the Heavy Good Vehicle corridor (Madrid-Sevilla) across Spanish regions: a Random Utility Based Multiregional Input-Output approach

The implementation of a charging policy for heavy goods vehicles in European Union (EU) member countries has been imposed to reflect costs of construction and maintenance of infrastructure as well as externalities such as congestion, accidents and environmental impact. In this context, EU countries approved the Eurovignette directive (1999/62/EC) and its amending directive (2006 /38/EC) which established a legal framework to regulate the system of tolls. Even if that regulation seek s to increase the efficien cy of freight, it will trigger direct and indirect effects on Spain’s regional economies by increasing transport costs. This paper presents the development of a multiregional Input-Output methodology (MRIO) with elastic trade coefficients to predict in terregional trade, using transport attributes integrated in multinomial logit models. This method is highly useful to carry out an ex-ante evaluation of transport policies because it involves road freight transport cost sensitivity, and determine regional distributive and substitution economic effect s of countries like Spain, characterized by socio-demographic and economic attributes, differentiated region by region. It will thus be possible to determine cost-effective strategies, given different policy scenarios. MRIO mode l would then be used to determine the impact on the employment rate of imposing a charge in the Madrid-Sevilla corridor in Spain. This methodology is important for measuring the impact on the employment rate since it is one of the main macroeconomic indicators of Spain’s regional and national economic situation. A previous research developed (DESTINO) using a MRIO method estimated employment impacts of road pricing policy across Spanish regions considering a fuel tax charge (€/liter) in the entire shortest cost path network for freight transport. Actually, it found that the variation in employment is expected to be substantial for some regions, and negligible for others. For example, in this Spanish case study of regional employment has showed reductions between 16.1% (Rioja) and 1.4% (Madrid region). This variation range seems to be related to either the intensity of freight transport in each region or dependency of regions to transport intensive economic sect ors. In fact, regions with freight transport intensive sectors will lose more jobs while regions with a predominantly service economy undergo a fairly insignificant loss of employment. This paper is focused on evaluating a freight transport vehicle-kilometer charge (€/km) in a non-tolled motorway corridor (A-4) between Madrid-Sevilla (517 Km.). The consequences of the road pricing policy implementation show s that the employment reductions are not as high as the diminution stated in the previous research because this corridor does not affect the whole freight transport system of Spain.

Integrated luminescent chemical microsensors based on GaN LEDs for security applications using smartphones

Development of PCB-integrateable microsensors for monitoring chemical species is a goal in areas such as lab-on-a-chip analytical devices, diagnostics medicine and electronics for hand-held instruments where the device size is a major issue. Cellular phones have pervaded the world inhabitants and their usefulness has dramatically increased with the introduction of smartphones due to a combination of amazing processing power in a confined space, geolocalization and manifold telecommunication features. Therefore, a number of physical and chemical sensors that add value to the terminal for health monitoring, personal safety (at home, at work) and, eventually, national security have started to be developed, capitalizing also on the huge number of circulating cell phones. The chemical sensor-enabled “super” smartphone provides a unique (bio)sensing platform for monitoring airborne or waterborne hazardous chemicals or microorganisms for both single user and crowdsourcing security applications. Some of the latest ones are illustrated by a few examples. Moreover, we have recently achieved for the first time (covalent) functionalization of p- and n-GaN semiconductor surfaces with tuneable luminescent indicator dyes of the Ru-polypyridyl family, as a key step in the development of innovative microsensors for smartphone applications. Chemical “sensoring” of GaN-based blue LED chips with those indicators has also been achieved by plasma treatment of their surface, and the micrometer-sized devices have been tested to monitor O2 in the gas phase to show their full functionality. Novel strategies to enhance the sensor sensitivity such as changing the length and nature of the siloxane buffer layer are discussed in this paper.

Control of integrated unit operations

As a thermal separation method, distillation is one of the most important technologies in the chemical industry. Given its importance, it is no surprise that increasing efforts have been made in reducing its energy inefficiencies. A great deal of research is focused in the design and optimization of the Divided-Wall Column. Its applications are still reduced due to distrust of its controllability. Previous references studied the decentralized control of DWC but still few papers deal about Model Predictive Control. In this work we present a decentralized control of both a DWC column along with its equivalent MPC schema.

Time and space partition platform for safe and secure flight software.

There are a number of research and development activities that are exploring Time and Space Partition (TSP) to implement safe and secure flight software. This approach allows to execute different real-time applications with different levels of criticality in the same computer board. In order to do that, flight applications must be isolated from each other in the temporal and spatial domains. This paper presents the first results of a partitioning platform based on the Open Ravenscar Kernel (ORK+) and the XtratuM hypervisor. ORK+ is a small, reliable real-time kernel supporting the Ada Ravenscar Computational model that is central to the ASSERT development process. XtratuM supports multiple virtual machines, i.e. partitions, on a single computer and is being used in the Integrated Modular Avionics for Space study. ORK+ executes in an XtratuM partition enabling Ada applications to share the computer board with other applications.

An Integrated Approach to Strategic Asset Management

This paper focuses on identifying and analysing the elements of Strategic Management for infrastructure and engineering assets. These elements are contended to involve an understanding of governance, corporate policy, corporate objectives, corporate strategy and interagency collaboration and will in turn, allow the ability determine a broader and more comprehensive framework for engineering asset management, ie a ‘staged approach’ to understanding how assets are managed within organisations. While the assets themselves have often been the sole concern for good management practices, other social and contextual elements have come into the mix in order to promote strategic asset management. The development of an integrated approach to asset management is at the base of the research question. What are the considerations and implications for adopting and implementing an integrated strategic asset management (ISAM) framework? While operational matters have been given prominence, a subset of corporate governance, Asset Governance, details the policies and processes needed to acquire, utilise, maintain and account for an organisation’s assets. Asset governance stems from the organisation’s overarching corporate governance principles; as a result it defines the management context in which engineering asset management is implemented. This aspect will be examined to determine the appropriate relationship between organisational strategic management and strategic asset management to further the theoretical engagement with the maturity of strategy,policy and governance for infrastructure and engineered assets. Asset governance stems from the organisation’s overarching corporate governance principles; as a result it defines the management context in which engineering asset management is implemented. The research proceeds by a document analysis of corporate reports and policy recommendations in terms of infrastructure and engineered assets. The paper concludes that incorporating an integrated asset management framework can promote a more robust conceptualisation of public assets and how they combine to provide a comprehensive system of service outcomes.

HERMES: Towards an Integrated Toolbox to Characterize Functional and Effective Brain Connectivity

The analysis of the interdependence between time series has become an important field of research in the last years, mainly as a result of advances in the characterization of dynamical systems from the signals they produce, the introduction of concepts such as generalized and phase synchronization and the application of information theory to time series analysis. In neurophysiology, different analytical tools stemming from these concepts have added to the ‘traditional’ set of linear methods, which includes the cross-correlation and the coherency function in the time and frequency domain, respectively, or more elaborated tools such as Granger Causality. This increase in the number of approaches to tackle the existence of functional (FC) or effective connectivity (EC) between two (or among many) neural networks, along with the mathematical complexity of the corresponding time series analysis tools, makes it desirable to arrange them into a unified-easy-to-use software package. The goal is to allow neuroscientists, neurophysiologists and researchers from related fields to easily access and make use of these analysis methods from a single integrated toolbox. Here we present HERMES (http://hermes.ctb.upm.es), a toolbox for the Matlab® environment (The Mathworks, Inc), which is designed to study functional and effective brain connectivity from neurophysiological data such as multivariate EEG and/or MEG records. It includes also visualization tools and statistical methods to address the problem of multiple comparisons. We believe that this toolbox will be very helpful to all the researchers working in the emerging field of brain connectivity analysis.