Profiling for run-time checking of computational properties and performance debugging in logic programs

Although several profiling techniques for identifying performance bottlenecks in logic programs have been developed, they are generally not automatic and in most cases they do not provide enough information for identifying the root causes of such bottlenecks. This complicates using their results for guiding performance improvement. We present a profiling method and tool that provides such explanations. Our profiler associates cost centers to certain program elements and can measure different types of resource-related properties that affect performance, preserving the precedence of cost centers in the cali graph. It includes an automatic method for detecting procedures that are performance bottlenecks. The profiling tool has been integrated in a previously developed run-time checking framework to allow verification of certain properties when they cannot be verified statically. The approach allows checking global computational properties which require complex instrumentation tracking information about previous execution states, such as, e.g., that the execution time accumulated by a given procedure is not greater than a given bound. We have built a prototype implementation, integrated it in the Ciao/CiaoPP system and successfully applied it to performance improvement, automatic optimization (e.g., resource-aware specialization of programs), run-time checking, and debugging of global computational properties (e.g., resource usage) in Prolog programs.

Integrating software testing and run-time checking in an assertion verification framework

We have designed and implemented a framework that unifies unit testing and run-time verification (as well as static verification and static debugging). A key contribution of our approach is that a unified assertion language is used for all of these tasks. We first propose methods for compiling runtime checks for (parts of) assertions which cannot be verified at compile-time via program transformation. This transformation allows checking preconditions and postconditions, including conditional postconditions, properties at arbitrary program points, and certain computational properties. The implemented transformation includes several optimizations to reduce run-time overhead. We also propose a minimal addition to the assertion language which allows defining unit tests to be run in order to detect possible violations of the (partial) specifications expressed by the assertions. This language can express for example the input data for performing the unit tests or the number of times that the unit tests should be repeated. We have implemented the framework within the Ciao/CiaoPP system and effectively applied it to the verification of ISO-prolog compliance and to the detection of different types of bugs in the Ciao system source code. Several experimental results are presented that ¡Ilústrate different trade-offs among program size, running time, or levéis of verbosity of the messages shown to the user.

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.

An approach to profiling for run-time checking of computational properties and performance debugging in logic programs.

Although several profiling techniques for identifying performance bottlenecks in logic programs have been developed, they are generally not automatic and in most cases they do not provide enough information for identifying the root causes of such bottlenecks. This complicates using their results for guiding performance improvement. We present a profiling method and tool that provides such explanations. Our profiler associates cost centers to certain program elements and can measure different types of resource-related properties that affect performance, preserving the precedence of cost centers in the call graph. It includes an automatic method for detecting procedures that are performance bottlenecks. The profiling tool has been integrated in a previously developed run-time checking framework to allow verification of certain properties when they cannot be verified statically. The approach allows checking global computational properties which require complex instrumentation tracking information about previous execution states, such as, e.g., that the execution time accumulated by a given procedure is not greater than a given bound. We have built a prototype implementation, integrated it in the Ciao/CiaoPP system and successfully applied it to performance improvement, automatic optimization (e.g., resource-aware specialization of programs), run-time checking, and debugging of global computational properties (e.g., resource usage) in Prolog programs.

Integrating software testing and run-time checking in an assertion verification framework.

We have designed and implemented a framework that unifies unit testing and run-time verification (as well as static verification and static debugging). A key contribution of our approach is that a unified assertion language is used for all of these tasks. We first propose methods for compiling runtime checks for (parts of) assertions which cannot be verified at compile-time via program transformation. This transformation allows checking preconditions and postconditions, including conditional postconditions, properties at arbitrary program points, and certain computational properties. The implemented transformation includes several optimizations to reduce run-time overhead. We also propose a minimal addition to the assertion language which allows defining unit tests to be run in order to detect possible violations of the (partial) specifications expressed by the assertions. This language can express for example the input data for performing the unit tests or the number of times that the unit tests should be repeated. We have implemented the framework within the Ciao/CiaoPP system and effectively applied it to the verification of ISO-prolog compliance and to the detection of different types of bugs in the Ciao system source code. Several experimental results are presented that illustrate different trade-offs among program size, running time, or levels of verbosity of the messages shown to the user.

Checking existing formulas for estimating overtopping rates in harbour breakwaters

The purpose of the research work resulting from various studies undertaken in the CEDEX, as summarized in this article, is to make a comparative analysis of methods for calculating overtopping rates developed by different authors. To this effect, in the first place, existing formulas for estimating the overtopping rate on rubble mound and vertical breakwaters were summarised and analysed. Later, the above mentioned formulas were compared using the results obtained in a series of hydraulic model tests at the CEDEX. The results obtained in the Ferrol outer harbour breakwater and Melilla harbour breakwater tests are presented here. A calculation method based on the neural network theory, developed in the European CLASH Project, was applied to a series of sloping breakwater tests in order to complete this research and the results obtained in the Ferrol outer harbour breakwater test are presented in this article. A series of additional tests was also carried out in a physical model on the standard cross section of the Bilbao harbour sloping breakwater’s cross section, the results of which are under study using the empirical formulas applicable to the cross section, as well as the NN-OVERTOPPING neural network

Abstraction-carrying code: a model for mobile code safety

Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The intended benefit is that the program consumer can locally validate the certificate w.r.t. the "untrustcd" program by means of a certificate checker a process which should be much simpler, efficient, and automatic than generating the original proof. The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both proving programs correct and replacing a costly verification process by an efficient checking proceduri on th( consumer side. In this work we propose Abstraction- Carrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argue that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safely policies which can be defined over different abstract domains. We use an abstraction (or abstract model) of the program computed by standard static analyzers as a certificate. The validity of the abstraction on ihe consumer side is checked in a single pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the area of mobile code safety.

Methodology for the design of offshore wind farms

Although still in an early stage, offshore wind development is now characterized by a boom process. This leads to the necessity of applying an integral management model for the design of offshore wind facilities, being the purpose of the model to achieve technical, economical and environmental viability, all within a sustainable development framework. The foregoing led to the research project exposed in this paper, consisting of drawing up an offshore wind farms methodological proposal; this methodology has a global and/or general nature or point of view whilst searching for optimization of the overall process of operations leading to the design of this type of installations and establishing collated theoretical bases for the further development of management tools. This methodological proposal follows a classical engineering thought scheme: it begins with the alternatives study, and ends with the detailed design. With this in mind, the paper includes the following sections: introduction, methodology used for the research project, conditioning factors, methodological proposal for the design of offshore wind farms, checking the methodological proposal, and conclusions

Comparative analysis of meta-analysis methods: when to use which?

Background: Several meta-analysis methods can be used to quantitatively combine the results of a group of experiments, including the weighted mean difference, statistical vote counting, the parametric response ratio and the non-parametric response ratio. The software engineering community has focused on the weighted mean difference method. However, other meta-analysis methods have distinct strengths, such as being able to be used when variances are not reported. There are as yet no guidelines to indicate which method is best for use in each case. Aim: Compile a set of rules that SE researchers can use to ascertain which aggregation method is best for use in the synthesis phase of a systematic review. Method: Monte Carlo simulation varying the number of experiments in the meta analyses, the number of subjects that they include, their variance and effect size. We empirically calculated the reliability and statistical power in each case Results: WMD is generally reliable if the variance is low, whereas its power depends on the effect size and number of subjects per meta-analysis; the reliability of RR is generally unaffected by changes in variance, but it does require more subjects than WMD to be powerful; NPRR is the most reliable method, but it is not very powerful; SVC behaves well when the effect size is moderate, but is less reliable with other effect sizes. Detailed tables of results are annexed. Conclusions: Before undertaking statistical aggregation in software engineering, it is worthwhile checking whether there is any appreciable difference in the reliability and power of the methods. If there is, software engineers should select the method that optimizes both parameters.

Influence of coiling on the stress relaxation of prestressing steel wires

The possible deleterious effects of coiling and long-term storage of coiled wires on the stress relaxation behaviour of prestressing steel wires has been checked by means of experimental work and a simple analytical model. The results show that if the requirements of standards are fulfilled (minimum coiling diameters), these effects can be neglected. However, some other factors, such as previous residual stresses, long-term storage or storage at high temperatures, can trigger or emphasize this damage to the material. In the authors' opinion, checking the final curvature of the wires after uncoiling prior to prestressing, as required in some standards, is to be recommended.

Obtaining carbonation depth of concrete used two different procedures standard EHE-08

In the Standard EHE 08, for the first time, durability acquires the status of Limit State. Article 8 provides that the term Durability limit state, produced by physical and chemical actions, different loads and actions of structural analysis, which can degrade the concrete and reinforcement to unacceptable limits. The verification of this limit state can be done through a procedure set out in the provisions of the Standard. This procedure is based on the use of tables that, depending on the aggressiveness of the environment in which the structure is the concrete strength and the life of the project, setting the quality of the concrete cover (minimum thickness and maximum water cement ratio of concrete used) and the maximum crack width. This procedure, simple in its application, provides highly secure solutions. In addition, on Annex 9, the Standard EHE 08 offers models for testing the durability limit state in cases of corrosion of reinforcement due to carbonation of concrete or entry of chloride ions. The results obtained with these models are tighter than those obtained with the procedure of the articles. In this paper we use both methods in the study of reinforced concrete structures with potential problems of corrosion of reinforcement due to carbonation of concrete. Later checking the results obtained by both procedures. Results demonstrate that the use of the models listed in Annex 9 of Standard EHE 08 offer cheaper solutions than those obtained using the procedure of the articles

Automated attribute inference in complex service workflows based on sharing analysis

The properties of data and activities in business processes can be used to greatly facilítate several relevant tasks performed at design- and run-time, such as fragmentation, compliance checking, or top-down design. Business processes are often described using workflows. We present an approach for mechanically inferring business domain-specific attributes of workflow components (including data Ítems, activities, and elements of sub-workflows), taking as starting point known attributes of workflow inputs and the structure of the workflow. We achieve this by modeling these components as concepts and applying sharing analysis to a Horn clause-based representation of the workflow. The analysis is applicable to workflows featuring complex control and data dependencies, embedded control constructs, such as loops and branches, and embedded component services.

Aplicaciones de filtrado adaptativo LMS para mejorar la respuesta de acelerómetros

El proyecto, “Aplicaciones de filtrado adaptativo LMS para mejorar la respuesta de acelerómetros”, se realizó con el objetivo de eliminar señales no deseadas de la señal de información procedentes de los acelerómetros para aplicaciones automovilísticas, mediante los algoritmos de los filtros adaptativos LMS. Dicho proyecto, está comprendido en tres áreas para su realización y ejecución, los cuales fueron ejecutados desde el inicio hasta el último día de trabajo. En la primera área de aplicación, diseñamos filtros paso bajo, paso alto, paso banda y paso banda eliminada, en lo que son los filtros de butterworth, filtros Chebyshev, de tipo uno como de tipo dos y filtros elípticos. Con esta primera parte, lo que se quiere es conocer, o en nuestro caso, recordar el entorno de Matlab, en sus distintas ecuaciones prediseñadas que nos ofrece el mencionado entorno, como también nos permite conocer un poco las características de estos filtros. Para posteriormente probar dichos filtros en el DSP. En la segunda etapa, y tras recordar un poco el entorno de Matlab, nos centramos en la elaboración y/o diseño de nuestro filtro adaptativo LMS; experimentado primero con Matlab, para como ya se dijo, entender y comprender el comportamiento del mismo. Cuando ya teníamos claro esta parte, procedimos a “cargar” el código en el DSP, compilarlo y depurarlo, realizando estas últimas acciones gracias al Visual DSP. Resaltaremos que durante esta segunda etapa se empezó a excitar las entradas del sistema, con señales provenientes del Cool Edit Pro, y además para saber cómo se comportaba el filtro adaptativo LMS, se utilizó señales provenientes de un generador de funciones, para obtener de esta manera un desfase entre las dos señales de entrada; aunque también se utilizó el propio Cool Edit Pro para obtener señales desfasadas, pero debido que la fase tres no podíamos usar el mencionado software, realizamos pruebas con el generador de funciones. Finalmente, en la tercera etapa, y tras comprobar el funcionamiento deseado de nuestro filtro adaptativo DSP con señales de entrada simuladas, pasamos a un laboratorio, en donde se utilizó señales provenientes del acelerómetro 4000A, y por supuesto, del generador de funciones; el cual sirvió para la formación de nuestra señal de referencia, que permitirá la eliminación de una de las frecuencias que se emitirá del acelerómetro. Por último, cabe resaltar que pudimos obtener un comportamiento del filtro adaptativo LMS adecuado, y como se esperaba. Realizamos pruebas, con señales de entrada desfasadas, y obtuvimos curiosas respuestas a la salida del sistema, como son que la frecuencia a eliminar, mientras más desfasado estén estas señales, mas se notaba. Solucionando este punto al aumentar el orden del filtro. Finalmente podemos concluir que pese a que los filtros digitales probados en la primera etapa son útiles, para tener una respuesta lo más ideal posible hay que tener en cuenta el orden del filtro, el cual debe ser muy alto para que las frecuencias próximas a la frecuencia de corte, no se atenúen. En cambio, en los filtros adaptativos LMS, si queremos por ejemplo, eliminar una señal de entre tres señales, sólo basta con introducir la frecuencia a eliminar, por una de las entradas del filtro, en concreto la señal de referencia. De esta manera, podemos eliminar una señal de entre estas tres, de manera que las otras dos, no se vean afectadas por el procedimiento. Abstract The project, "LMS adaptive filtering applications to improve the response of accelerometers" was conducted in order to remove unwanted signals from the information signal from the accelerometers for automotive applications using algorithms LMS adaptive filters. The project is comprised of three areas for implementation and execution, which were executed from the beginning until the last day. In the first area of application, we design low pass filters, high pass, band pass and band-stop, as the filters are Butterworth, Chebyshev filters, type one and type two and elliptic filters. In this first part, what we want is to know, or in our case, remember the Matlab environment, art in its various equations offered by the mentioned environment, as well as allows us to understand some of the characteristics of these filters. To further test these filters in the DSP. In the second stage, and recalling some Matlab environment, we focus on the development and design of our LMS adaptive filter; experimented first with Matlab, for as noted above, understand the behavior of the same. When it was clear this part, proceeded to "load" the code in the DSP, compile and debug, making these latest actions by the Visual DSP. Will highlight that during this second stage began to excite the system inputs, with signals from the Cool Edit Pro, and also for how he behaved the LMS adaptive filter was used signals from a function generator, to thereby obtain a gap between the two input signals, but also used Cool Edit Pro himself for phase signals, but due to phase three could not use such software, we test the function generator. Finally, in the third stage, and after checking the desired performance of our DSP adaptive filter with simulated input signals, we went to a laboratory, where we used signals from the accelerometer 4000A, and of course, the function generator, which was used for the formation of our reference signal, enabling the elimination of one of the frequencies to be emitted from the accelerometer. Note that they were able to obtain a behavior of the LMS adaptive filter suitable as expected. We test with outdated input signals, and got curious response to the output of the system, such as the frequency to remove, the more outdated are these signs, but noticeable. Solving this point with increasing the filter order. We can conclude that although proven digital filters in the first stage are useful, to have a perfect answer as possible must be taken into account the order of the filter, which should be very high for frequencies near the frequency cutting, not weakened. In contrast, in the LMS adaptive filters if we for example, remove a signal from among three signals, only enough to eliminate the frequency input on one of the inputs of the filter, namely the reference signal. Thus, we can remove a signal between these three, so that the other two, not affected by the procedure.

Desarrollo de un datalink con el chip CC1110 de Texas Instruments para UAVs

Se trata de estudiar el comportamiento de un sistema basado en el chip CC1110 de Texas Instruments, para aplicaciones inalámbricas. Los dispositivos basados en este tipo de chips tienen actualmente gran profusión, dada la demanda cada vez mayor de aplicaciones de gestión y control inalámbrico. Por ello, en la primera parte del proyecto se presenta el estado del arte referente a este aspecto, haciendo mención a los sistemas operativos embebidos, FPGAs, etc. También se realiza una introducción sobre la historia de los aviones no tripulados, que son el vehículo elegido para el uso del enlace de datos. En una segunda parte se realiza el estudio del dispositivo mediante una placa de desarrollo, verificando y comprobando mediante el software suministrado, el alcance del mismo. Cabe resaltar en este punto que el control con la placa mencionada se debe hacer mediante programación de bajo nivel (lenguaje C), lo que aporta gran versatilidad a las aplicaciones que se pueden desarrollar. Por ello, en una tercera parte se realiza un programa funcional, basado en necesidades aportadas por la empresa con la que se colabora en el proyecto (INDRA). Este programa es realizado sobre el entorno de Matlab, muy útil para este tipo de aplicaciones, dada su versatilidad y gran capacidad de cálculo con variables. Para terminar, con la realización de dichos programas, se realizan pruebas específicas para cada uno de ellos, realizando pruebas de campo en algunas ocasiones, con vehículos los más similares a los del entorno real en el que se prevé utilizar. Como implementación al programa realizado, se incluye un manual de usuario con un formato muy gráfico, para que la toma de contacto se realice de una manera rápida y sencilla. Para terminar, se plantean líneas futuras de aplicación del sistema, conclusiones, presupuesto y un anexo con los códigos de programación más importantes. Abstract In this document studied the system behavior based on chip CC1110 of Texas Instruments, for wireless applications. These devices currently have profusion. Right the increasing demand for control and management wireless applications. In the first part of project presents the state of art of this aspect, with reference to the embedded systems, FPGAs, etc. It also makes a history introduction of UAVs, which are the vehicle for use data link. In the second part is studied the device through development board, verifying and checking with provided software the scope. The board programming is C language; this gives a good versatility to develop applications. Thus, in third part performing a functionally program, it based on requirements provided by company with which it collaborates, INDRA Company. This program is developed with Matlab, very useful for such applications because of its versatility and ability to use variables. Finally, with the implementation of such programs, specific tests are performed for each of them, field tests are performed in several cases, and vehicles used for this are the most similar to the actual environment plain to use. Like implementing with the program made, includes a graphical user manual, so your understanding is conducted quickly and easily. Ultimately, present future targets for system applications, conclusions, budget and annex of the most important programming codes.

Fiabilidad de los sistemas fotovoltaicos autónomos

Los sistemas fotovoltaicos autónomos, es decir, sistemas que carecen de conexión a la red eléctrica, presentan una gran utilidad para poder llevar a cabo la electrificación de lugares remotos donde no hay medios de acceder a la energía eléctrica. El continuo avance en el número de sistemas instalados por todo el mundo y su continua difusión técnica no significa que la implantación de estas instalaciones no presente ninguna problemática. A excepción del panel fotovoltaico que presenta una elevada fiabilidad, el resto de elementos que forman el sistema presentan numerosos problemas y dependencias, por tanto el estudio de las fiabilidades de estos elementos es obligado. En este proyecto se pretende analizar y estudiar detalladamente la fiabilidad de los sistemas fotovoltaicos aislados. Primeramente, el presente documento ofrece una introducción sobre la situación mundial de las energías renovables, así como una explicación detallada de la energía fotovoltaica. Esto incluye una explicación técnica de los diferentes elementos que forman el sistema energético (módulo fotovoltaico, batería, regulador de carga, inversor, cargas, cableado y conectores). Por otro lado, se hará un estudio teórico del concepto de fiabilidad, con sus definiciones y parámetros más importantes. Llegados a este punto, el proyecto aplica la teoría de fiabilidad comentada a los sistemas fotovoltaicos autónomos, profundizando en la fiabilidad de cada elemento del sistema así como evaluando el conjunto. Por último, se muestran datos reales de fiabilidad de programas de electrificación, demostrando la variedad de resultados sujetos a los distintos emplazamientos de las instalaciones y por tanto distintas condiciones de trabajo. Se destaca de esta forma la importancia de la fiabilidad de los sistemas fotovoltaicos autónomos, pues normalmente este tipo de instalaciones se localizan en emplazamientos remotos, sin personal cualificado de mantenimiento cercano ni grandes recursos logísticos y económicos. También se resalta en el trabajo la dependencia de la radiación solar y el perfil de consumo a la hora de dimensionar el sistema. Abstract Stand-alone photovoltaic systems which are not connected to the utility grid. These systems are very useful to carry out the electrification of remote locations where is no easy to access to electricity. The number increased of systems installed worldwide and their continued dissemination technique does not mean that these systems doesn´t fails. With the exception of the photovoltaic panel with a high reliability, the remaining elements of the system can to have some problems and therefore the study of the reliabilities of these elements is required. This project tries to analyze and study the detaila of the reliability of standalone PV systems. On the one hand, this paper provides an overview of the global situation of renewable energy, as well as a detailed explanation of photovoltaics. This includes a technical detail of the different elements of the energy system (PV module, battery, charge controller, inverter, loads, wiring and connectors). In addition, there will be a theoricall study of the concept of reliability, with the most important definitions and key parameters. On the other hand, the project applies the reliability concepts discussed to the stand-alone photovoltaic systems, analyzing the reliability of each element of the system and analyzing the entire system. Finally, this document shows the most important data about reliability of some electrification programs, checking the variety of results subject to different places and different conditions. As a conclussion, the importance of reliability of stand-alone photovoltaic systems because usually these are located in remote locations, without qualified maintenance and financial resources.These systems operate under dependence of solar radiation and the consumption profile.