Infrastructure and Workflow for the Formal Evaluation of Semantic Search Technologies

This paper describes an infrastructure for the automated evaluation of semantic technologies and, in particular, semantic search technologies. For this purpose, we present an evaluation framework which follows a service-oriented approach for evaluating semantic technologies and uses the Business Process Execution Language (BPEL) to define evaluation workflows that can be executed by process engines. This framework supports a variety of evaluations, from different semantic areas, including search, and is extendible to new evaluations. We show how BPEL addresses this diversity as well as how it is used to solve specific challenges such as heterogeneity, error handling and reuse

Formal verification of safety protocol in train control system

In order to satisfy the safety-critical requirements, the train control system (TCS) often employs a layered safety communication protocol to provide reliable services. However, both description and verification of the safety protocols may be formidable due to the system complexity. In this paper, interface automata (IA) are used to describe the safety service interface behaviors of safety communication protocol. A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN. A case study of using this method to describe and verify a safety communication protocol is included. The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks, livelocks and several mandatory consistency properties. A prototype of safety protocols is also developed based on the presented formally verifying method.

Non-linear Control of an Autonomous Ground Vehicle

In this paper, in order to select a speed controller for a specific non-linear autonomous ground vehicle, proportional-integral-derivative (PID), Fuzzy, and linear quadratic regulator (LQR) controllers were designed. Here, in order to carry out the tuning of the above controllers, a multicomputer genetic algorithm (MGA) was designed. Then, the results of the MGA were used to parameterize the PID, Fuzzy and LQR controllers and to test them under laboratory conditions. Finally, a comparative analysis of the performance of the three controllers was conducted.

Virtual Learning Environments In Faculties Of Education In Spain: Changes On Student Attitude

This paper presents some results of a R+D project entitled “e-Learning system for Practical Training of University students in Education Faculties (ForELearn)”, developed in Spain by the Universidad de Granada and the Universidad Politécnica de Madrid and funded by the Spanish Ministry of Education. In a first phase, through the use of AulaWeb Learning Management System, a set of adaptations and improvements of this software application have been done for the design and development of an experimental course of Practicum supervision. Next, the implementation of this course by means of a group of face to face and online seminars provides experimental data for the analysis and discussion about the point of view of users (preservice teachers) that have tracked their practice supervision with AulaWeb.

Analytical solution to the one-dimensional non-uniform absorption of solar radiation in uncoated and coated single glass panes

The analytical solution to the one-dimensional absorption–conduction heat transfer problem inside a single glass pane is presented, which correctly takes into account all the relevant physical phenomena: the appearance of multiple reflections, the spectral distribution of solar radiation, the spectral dependence of optical properties, the presence of possible coatings, the non-uniform nature of radiation absorption, and the diffusion of heat by conduction across the glass pane. Additionally to the well established and known direct absorptance αe, the derived solution introduces a new spectral quantity called direct absorptance moment βe, that indicates where in the glass pane is the absorption of radiation actually taking place. The theoretical and numerical comparison of the derived solution with existing approximate thermal models for the absorption–conduction problem reveals that the latter ones work best for low-absorbing uncoated single glass panes, something not necessarily fulfilled by modern glazings.

Non-destructive measurements of the optical properties of apples by means of time-resolved reflectance

Time-resolved reflectance is proposed and effectively used for the nondestructive measurement of the optical properties in apples. The technique is based on the detection of the temporal dispersion of a short laser pulse injected into the probed medium. The time-distribution of re-emitted photons interpreted with a solution of the Diffusion equation yields the mean values of the absorption and reduced scattering coefficients of the medium. The proposed technique proved valuable for the measurement of the absorption and scattering spectra of different varieties of apples. No major variations were observed in the experimental data when the fruit was peeled, proving that the measured optical properties are referred to the pulp. The depth of probed volume was determined to be about 2 cm. Finally, the technique proved capable to follow the change in chlorophyll absorption during storage.

Non-destructive measurements of the optical properties of apples by means of time-resolved reflectance

Time-resolved reflectance is proposed and effectively used for the nondestructive measurement of the optical properties in apples. The technique is based on the detection of the temporal dispersion of a short laser pulse injected into the probed medium. The time-distribution of re-emitted photons interpreted with a solution of the Diffusion equation yields the mean values of the absorption and reduced scattering coefficients of the medium. The proposed technique proved valuable for the measurement of the absorption and scattering spectra of different varieties of apples. No major variations were observed in the experimental data when the fruit was peeled, proving that the measured optical properties are referred to the pulp. The depth of probed volume was determined to be about 2 cm. Finally, the technique proved capable to follow the change in chlorophyll absorption during storage.

Non-periodic driving of coupled oscillators:a spherical swing

Nonlinearly coupled, damped oscillators at 1:1 frequency ratio, one oscillator being driven coherently for efficient excitation, are exemplified by a spherical swing with some phase-mismatch between drive and response. For certain damping range, excitation is found to succeed if it lags behind, but to produce a chaotic attractor if it leads the response. Although a period-doubhng sequence, for damping increasing, leads to the attractor, this is actually born as a hard (as regards amplitude) bifurcation at a zero growth-rate parametric line; as damping decreases, an unstable fixed point crosses an invariant plane to enter as saddle-focus a phase-space domain of physical solutions. A second hard bifurcation occurs at the zero mismatch line, the saddle-focus leaving that domain. Times on the attractor diverge when approaching either fine, leading to exactly one-dimensional and noninvertible limit maps, which are analytically determined.

Influence of temperature and moisture content in Non-destructive values of Scots pine (Pinus sylvestris L.)

Good results evaluating material properties using non-destructive testing (NDT) techniques have been achieved for decades. Several studies to understand the influence of temperature and moisture content on NDT have concluded different effects. In this study, NDT parameters were measured on the principal structural Spanish sawn timber species, Scots pine (Pinus sylvestris L.). NDT were conducted on 216 specimens of nominal dimensions 20 by 20 by 400 mm. Specimens were divided into several groups and studied at six different temperatures and four different moisture contents. Commercial equipment and techniques applied were Sylvatest Duo (ultrasonic wave technique), Steinkamp BPV (ultrasonic wave technique), and Grindo Sonic Mk5 "Industrial" (vibration analysis technique). Differences in NDT values within specimens at different temperatures and moisture contents were obtained. Main results of this study and relationships that describe changes in NDT values by effect of temperature and moisture content are presented.

Non-Destructive Identification of Woolly Peaches combining Mechanical Impact Response and NIR Spectroscopy.

Woolliness (mealiness in other fruits) is a negative attribute of peach sensory texture that is a physiological disorder associated with inadequate cold storage. It is characterised by lack of crispness and juiciness without variation in the tissue water content (Harker and Hallet, 1992). Many attempts have been made to develop destructive instrumental procedures to detect mealiness and woolliness. Non-destructive procedures attempted include using nuclear magnetic resonance (Sonego et al., 1995). However, this technique has economical limitations and is not practical at present. Non-destructive impact tests and NIR are non-destructive techniques which have been used to assess internal characteristics of fruits (Chen and Sun, 1991). The objective of this study was to develop a novel non-destructive procedure to identify woolly peaches by combining impact and NIR approaches.

UWB doublet generation employing non-linear effects of a Semiconductor Optical Amplifier Mach-Zehnder inteferometer

In this article, a novel method to generate an ultra-wideband (UWB) doublet using the cross-phase modulation (XPM) effect is proposed and experimentally demonstrated. The main component of the submitted architecture is a SOA-Mach-Zehnder interferometer (MZI) pumped with a modulated Gaussian pulse. Maximum and minimum conversion points are analyzed through the systems transfer function in order to determinate the most effective operation stage. By tuning different values for the SOAs currents, it is possible to identify a conversion step in which the input pulse is enough large to saturate the SOAMZI, leading to the generation of a UWB doublet pulse.

Ensayo no destructivo de soldaduras en pernos conectores mediante inspección acústica = Non-destructive test of welding headed studs through acoustic emission

Los pernos conectores aportan múltiples ventajas de uso, entre las que se encuentra el elevado margen de seguridad que ofrecen sus soldaduras ejecutadas mediante arco eléctrico. Estas soldaduras, aunque ampliamente fiables, son difícilmente comprobadas mediante ensayos no destructivos. Aparte de la inspección visual, que aporta gran información sobre la calidad de ejecución de la soldadura, el resto de ensayos no destructivos (líquidos penetrantes, partículas magnéticas, ultrasonidos, radiografías, etc.) resultan inviables en estos elementos. Por otro lado, los ensayos acústicos de piezas metálicas han existido siempre. Su comprobación se basaba en el análisis por medio de ¿un oído fino¿ del sonido resultante tras ser golpeado el elemento a evaluar. Con estas premisas se plantea el presente estudio de inspección de las soldaduras en pernos conectores mediante su espectro acústico. Analíticamente, la investigación se ha centrado en el cálculo informático de los primeros modos propios de vibración mediante elementos finitos. Se han modelizado diferentes grados de penetración de la soldadura mediante la modificación de las condiciones de contorno. Se ha observado que variando el número de movimientos coaccionados en los nodos pertenecientes a la soldadura se produce una reducción en su frecuencia de vibración.

UWB Monocycle Generator based on the non-linear effects of an SOA-integrated structure

In this letter, we propose and experimentally demonstrate a novel and single structure to generate ultra-wideband (UWB) pulses by means of the cross-phase modulation present in a semiconductor optical amplifier unified structure. The key components of this system is an integrated Mach-Zehnder interferometer with two semiconductor optical amplifiers and an optical processing unit. The fusion of these two components permits the generation and customization of UWB monocycle pulses. The polarity of the output pulses is easily modified through the single selection of a specific input port. Moreover, the capacity of transmitting several data sequences is demonstrated and the potentiality to adapt the system to different modulation formats is analyzed.

Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures

Los tipos de datos concurrentes son implementaciones concurrentes de las abstracciones de datos clásicas, con la diferencia de que han sido específicamente diseñados para aprovechar el gran paralelismo disponible en las modernas arquitecturas multiprocesador y multinúcleo. La correcta manipulación de los tipos de datos concurrentes resulta esencial para demostrar la completa corrección de los sistemas de software que los utilizan. Una de las mayores dificultades a la hora de diseñar y verificar tipos de datos concurrentes surge de la necesidad de tener que razonar acerca de un número arbitrario de procesos que invocan estos tipos de datos de manera concurrente. Esto requiere considerar sistemas parametrizados. En este trabajo estudiamos la verificación formal de propiedades temporales de sistemas concurrentes parametrizados, poniendo especial énfasis en programas que manipulan estructuras de datos concurrentes. La principal dificultad a la hora de razonar acerca de sistemas concurrentes parametrizados proviene de la interacción entre el gran nivel de concurrencia que éstos poseen y la necesidad de razonar al mismo tiempo acerca de la memoria dinámica. La verificación de sistemas parametrizados resulta en sí un problema desafiante debido a que requiere razonar acerca de estructuras de datos complejas que son accedidas y modificadas por un numero ilimitado de procesos que manipulan de manera simultánea el contenido de la memoria dinámica empleando métodos de sincronización poco estructurados. En este trabajo, presentamos un marco formal basado en métodos deductivos capaz de ocuparse de la verificación de propiedades de safety y liveness de sistemas concurrentes parametrizados que manejan estructuras de datos complejas. Nuestro marco formal incluye reglas de prueba y técnicas especialmente adaptadas para sistemas parametrizados, las cuales trabajan en colaboración con procedimientos de decisión especialmente diseñados para analizar complejas estructuras de datos concurrentes. Un aspecto novedoso de nuestro marco formal es que efectúa una clara diferenciación entre el análisis del flujo de control del programa y el análisis de los datos que se manejan. El flujo de control del programa se analiza utilizando reglas de prueba y técnicas de verificación deductivas especialmente diseñadas para lidiar con sistemas parametrizados. Comenzando a partir de un programa concurrente y la especificación de una propiedad temporal, nuestras técnicas deductivas son capaces de generar un conjunto finito de condiciones de verificación cuya validez implican la satisfacción de dicha especificación temporal por parte de cualquier sistema, sin importar el número de procesos que formen parte del sistema. Las condiciones de verificación generadas se corresponden con los datos manipulados. Estudiamos el diseño de procedimientos de decisión especializados capaces de lidiar con estas condiciones de verificación de manera completamente automática. Investigamos teorías decidibles capaces de describir propiedades de tipos de datos complejos que manipulan punteros, tales como implementaciones imperativas de pilas, colas, listas y skiplists. Para cada una de estas teorías presentamos un procedimiento de decisión y una implementación práctica construida sobre SMT solvers. Estos procedimientos de decisión son finalmente utilizados para verificar de manera automática las condiciones de verificación generadas por nuestras técnicas de verificación parametrizada. Para concluir, demostramos como utilizando nuestro marco formal es posible probar no solo propiedades de safety sino además de liveness en algunas versiones de protocolos de exclusión mutua y programas que manipulan estructuras de datos concurrentes. El enfoque que presentamos en este trabajo resulta ser muy general y puede ser aplicado para verificar un amplio rango de tipos de datos concurrentes similares. Abstract Concurrent data types are concurrent implementations of classical data abstractions, specifically designed to exploit the great deal of parallelism available in modern multiprocessor and multi-core architectures. The correct manipulation of concurrent data types is essential for the overall correctness of the software system built using them. A major difficulty in designing and verifying concurrent data types arises by the need to reason about any number of threads invoking the data type simultaneously, which requires considering parametrized systems. In this work we study the formal verification of temporal properties of parametrized concurrent systems, with a special focus on programs that manipulate concurrent data structures. The main difficulty to reason about concurrent parametrized systems comes from the combination of their inherently high concurrency and the manipulation of dynamic memory. This parametrized verification problem is very challenging, because it requires to reason about complex concurrent data structures being accessed and modified by threads which simultaneously manipulate the heap using unstructured synchronization methods. In this work, we present a formal framework based on deductive methods which is capable of dealing with the verification of safety and liveness properties of concurrent parametrized systems that manipulate complex data structures. Our framework includes special proof rules and techniques adapted for parametrized systems which work in collaboration with specialized decision procedures for complex data structures. A novel aspect of our framework is that it cleanly differentiates the analysis of the program control flow from the analysis of the data being manipulated. The program control flow is analyzed using deductive proof rules and verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, our techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. The verification conditions correspond to the data manipulation. We study the design of specialized decision procedures to deal with these verification conditions fully automatically. We investigate decidable theories capable of describing rich properties of complex pointer based data types such as stacks, queues, lists and skiplists. For each of these theories we present a decision procedure, and its practical implementation on top of existing SMT solvers. These decision procedures are ultimately used for automatically verifying the verification conditions generated by our specialized parametrized verification techniques. Finally, we show how using our framework it is possible to prove not only safety but also liveness properties of concurrent versions of some mutual exclusion protocols and programs that manipulate concurrent data structures. The approach we present in this work is very general, and can be applied to verify a wide range of similar concurrent data types.

Non contact inspection of the fatigue damage state of carbon fiber reinforced polymer by optical surface roughness measurements

This work presents the evaluation of a new non-contact technique to assess the fatigue damage state of CFRP structures by measuring surface roughness parameters. Surface roughness and stiffness degradation have been measured in CFRP coupons cycled with constant amplitude loads, and a Pearson?s correlation of 0.79 was obtained between both variables. Results suggest that changes on the surface roughness measured in strategic zones of components made of the evaluated CFRP, could be indicative of the level of damage due to fatigue loads. This methodology could be useful for other FRP due to similarities in the fatigue damage process.