Geotechnical Analysis of Contaminated Sand by Light Non-Aquous Phase Liquids

Contaminated soil reuse was investigated, with higher profusion, throughout the early 90’s, coinciding with the 1991 Gulf War, when efforts to amend large crude oil releases began in geotechnical assessment of contaminated soils. Isolated works referring to geotechnical testing with hydrocarbon ground contaminants are described in the state-of-the-art, which have been extended to other type of contaminated soil references. Contaminated soils by light non-aquous phase liquids (LNAPL) bearing capacity reduction has been previously investigated from a forensic point of view. To date, all the research works have been published based on the assumption of constant contaminant saturation for the entire soil mass. In contrast, the actual LNAPLs distribution plumes exhibit complex flow patterns which are subject to physical and chemical changes with time and distance travelled from the release source. This aspect has been considered along the present text. A typical Madrid arkosic soil formation is commonly known as Miga sand. Geotechnical tests have been carried out, with Miga sand specimens, in incremental series of LNAPL concentrations in order to observe the soil engineering properties variation due to a contamination increase. Results are discussed in relation with previous studies and as a matter of fact, soil mechanics parameters change in the presence of LNAPL, showing different tendencies according to each test and depending on the LNAPL content, as well as to the specimen’s initially planned relative density, dense or loose. Geotechnical practical implications are also commented on and analyzed. Variation on geotechnical properties may occur only within the external contour of contamination distribution plume. This scope has motivated the author to develop a physical model based on transparent soil technology. The model aims to reproduce the distribution of LNAPL into the ground due to an accidental release from a storage facility. Preliminary results indicate that the model is a potentially complementary tool for hydrogeological applications, site-characterization and remediation treatment testing within the framework of soil pollution events. A description of the test setup of an innovative three dimensional physical model for the flow of two or more phases, in porous media, is presented herein, along with a summary of the advantages, limitations and future applications for modeling with transparent material. En los primeros años de la década de los años 90, del siglo pasado, coincidiendo con la Guerra del Golfo en 1991, se investigó intensamente sobre la reutilización de suelos afectados por grandes volúmenes de vertidos de crudo, fomentándose la evaluación geotécnica de los suelos contaminados. Se describen, en el estado del arte de esta tésis, una serie de trabajos aislados en relación con la caracterización geotécnica de suelos contaminados con hidrocarburos, descripción ampliada mediante referencias relacionadas con otros tipos de contaminación de suelos. Existen estudios previos de patología de cimentaciones que analizan la reducción de la capacidad portante de suelos contaminados por hidrocarburos líquidos ligeros en fase no acuosa (acrónimo en inglés: LNAPL de “Liquid Non-Aquous Phase Liquid”). A fecha de redacción de la tesis, todas las publicaciones anteriores estaban basadas en la consideración de una saturación del contaminante constante en toda la extensión del terreno de cimentación. La distribución real de las plumas de contaminante muestra, por el contrario, complejas trayectorias de flujo que están sujetas a cambios físico-químicos en función del tiempo y la distancia recorrida desde su origen de vertido. Éste aspecto ha sido considerado y tratado en el presente texto. La arena de Miga es una formación geológica típica de Madrid. En el ámbito de esta tesis se han desarrollado ensayos geotécnicos con series de muestras de arena de Miga contaminadas con distintas concentraciones de LNAPL con el objeto de estimar la variación de sus propiedades geotécnicas debido a un incremento de contaminación. Se ha realizado una evaluación de resultados de los ensayos en comparación con otros estudios previamente analizados, resultando que las propiedades mecánicas del suelo, efectivamente, varían en función del contenido de LNAPL y de la densidad relativa con la que se prepare la muestra, densa o floja. Se analizan y comentan las implicaciones de carácter práctico que supone la mencionada variación de propiedades geotécnicas. El autor ha desarrollado un modelo físico basado en la tecnología de suelos transparentes, considerando que las variaciones de propiedades geotécnicas únicamente deben producirse en el ámbito interior del contorno de la pluma contaminante. El objeto del modelo es el de reproducir la distribución de un LNAPL en un terreno dado, causada por el vertido accidental de una instalación de almecenamiento de combustible. Los resultados preliminares indican que el modelo podría emplearse como una herramienta complementaria para el estudio de eventos contaminantes, permitiendo el desarrollo de aplicaciones de carácter hidrogeológico, caracterización de suelos contaminados y experimentación de tratamientos de remediación. Como aportación de carácter innovadora, se presenta y describe un modelo físico tridimensional de flujo de dos o más fases a través de un medio poroso transparente, analizándose sus ventajas e inconvenientes así como sus limitaciones y futuras aplicaciones.

Condensation in ducts

Phase changing flows are being considered for thermal management in space platforms. The resulting flow patterns are very complicated and extremely sensitive to gravity action. Concerning fluid flow in ducts, the available evidence indicates that although the pressure loss does not depend too much on the fluid flow pattern,the heat transfer (and resulting phase change) does. A simple exercise to illustrate this point is presented in this paper. It deals with condensing flow in straight circular cross-sectional ducts. Two extreme configurations are considered here, one corresponds to a stratified flow and the other to an annular flow. Both types of flow patterns have been extensively considered in the past and from this point of view almost nothing is new in the paper, but past results look conflictive and this could be due to the limitations and computational intricacies of the models used. Thus the problem has been reformulated from the onset and the results are presented as the evolution of the vapor quality (vapor to total mass flow rate) along the duct, in typical cases. The results presented here indicate that within the validity of the present models and the assumed ranges of mass flow rate, duct diameter, thermal conditions and fluid characteristics,the length of the ducts required to achieve complete condensation under zero gravity are an order of magnitude larger than in horizontal tubes under normal terrestrial conditions.

A flexible (C)LP-based approach to the analysis of object-oriented programs

Static analyses of object-oriented programs usually rely on intermediate representations that respect the original semantics while having a more uniform and basic syntax. Most of the work involving object-oriented languages and abstract interpretation usually omits the description of that language or just refers to the Control Flow Graph(CFG) it represents. However, this lack of formalization on one hand results in an absence of assurances regarding the correctness of the transformation and on the other it typically strongly couples the analysis to the source language. In this work we present a framework for analysis of object-oriented languages in which in a first phase we transform the input program into a representation based on Horn clauses. This allows on one hand proving the transformation correct attending to a simple condition and on the other being able to apply an existing analyzer for (constraint) logic programming to automatically derive a safe approximation of the semantics of the original program. The approach is flexible in the sense that the first phase decouples the analyzer from most languagedependent features, and correct because the set of Horn clauses returned by the transformation phase safely approximates the standard semantics of the input program. The resulting analysis is also reasonably scalable due to the use of mature, modular (C)LP-based analyzers. The overall approach allows us to report results for medium-sized programs.

A generic, context sensitive analysis framework for object oriented programs

Abstract interpreters rely on the existence of a nxpoint algorithm that calculates a least upper bound approximation of the semantics of the program. Usually, that algorithm is described in terms of the particular language in study and therefore it is not directly applicable to programs written in a different source language. In this paper we introduce a generic, block-based, and uniform representation of the program control flow graph and a language-independent nxpoint algorithm that can be applied to a variety of languages and, in particular, Java. Two major characteristics of our approach are accuracy (obtained through a topdown, context sensitive approach) and reasonable efficiency (achieved by means of memoization and dependency tracking techniques). We have also implemented the proposed framework and show some initial experimental results for standard benchmarks, which further support the feasibility of the solution adopted.

Nonlinear description of transversal motion in a laminar boundary layer with streaks

The nonlinear streamwise growth of a spanwise periodic array of steady streaks in a flat plate boundary layer is numerically computed using the well known Reduced Navier-Stokes formulation. It is found that the flow configuration changes substantially when the amplitude of the streaks grows and the nonlinear effects come into play. The transversal motion (in the wall normal-spanwise plane), which is normally not considered, becomes non-negligible in the nonlinear regime, and it strongly distorts the streamwise velocity profiles, which end up being quite different from those predicted by the linear theory. We analyze in detail the resulting flow patterns for the nonlinearly saturated streaks, and compare them with available experimental results.

Nonlinear description of transversal motion in a laminar boundary layer with streaks

The nonlinear streamwise growth of a spanwise periodic array of steady streaks in a flat plate boundary layer is numerically computed using the well known Reduced Navier- Stokes formulation. It is found that the flow configuration changes substantially when the amplitude of the streaks grows and the nonlinear effects come into play. The transversal motion (in the wall normal-spanwise plane), which is normally not considered, becomes non-negligible in the nonlinear regime, and it strongly distorts the streamwise velocity profiles, which end up being quite different from those predicted by the linear theory. We analyze in detail the resulting flow patterns for the nonlinearly saturated streaks, and compare them with available experimental results.

Modelling wake effects in large wind farms in complex terrain: the problem, the methods and the issues

Computational fluid dynamic (CFD) methods are used in this paper to predict the power production from entire wind farms in complex terrain and to shed some light into the wake flow patterns. Two full three-dimensional Navier–Stokes solvers for incompressible fluid flow, employing k − ϵ and k − ω turbulence closures, are used. The wind turbines are modeled as momentum absorbers by means of their thrust coefficient through the actuator disk approach. Alternative methods for estimating the reference wind speed in the calculation of the thrust are tested. The work presented in this paper is part of the work being undertaken within the UpWind Integrated Project that aims to develop the design tools for next generation of large wind turbines. In this part of UpWind, the performance of wind farm and wake models is being examined in complex terrain environment where there are few pre-existing relevant measurements. The focus of the work being carried out is to evaluate the performance of CFD models in large wind farm applications in complex terrain and to examine the development of the wakes in a complex terrain environment.

Instabilities in two-liquid layers subject to a horizontal temperature gradient

We study theoretically the stability of two superposed fluid layers heated laterally. The fluids are supposed to be immiscible, the interface undeformable and of infinite horizontal extension. Combined thermocapillary and buoyancy forces give rise to a basic flow when a temperature difference is applied. The calculations are performed for a melt of GaAs under a layer of molten B2 O3 , a configuration of considerable technological importance. Four dif- ferent flow patterns and five temperature configurations are found for the basic state in this system. A linear stability analysis shows that the basic state may be destabilized by oscilla- tory motions leading to the so-called hydrothermal waves. Depending on the relative height of the two layers these hydrothermal waves propagate parallel or perpendicular to the temperature gradient. This analysis reveals that these perturbations can alter significantly the liquid flow in the liquid-encapsulated crystal growth techniques.

Convective instabilities in two superposed horizontal liquid layers heated laterally.

This work is devoted to the theoretical study of the stability of two superposed horizontal liquid layers bounded by two solid planes and subjected to a horizontal temperature gradient. The liquids are supposed to be immiscible with a nondeformable interface. The forces acting on the system are buoyancy and interfacial tension. Four different flow patterns and temperature profiles are found for the basic state. A linear perturbative analysis with respect to two- and three-dimensional perturbations reveals the existence of three kinds of patterns. Depending on the relative height of both liquids several situations are predicted: either wave propa- gation from cold to the hot regions, or waves propagating in the opposite direction or still stationary longitu- dinal rolls. The behavior of three different pairs of liquids which have been used in experiments on bilayers under vertical gradient by other authors have been examined. The instability mechanisms are discussed and a qualitative interpretation of the different behaviors exhibited by the system is provided. In some configurations it is possible to find a codimension-two point created by the interaction of two Hopf modes with different frequencies and wave numbers. These results suggest to consider two liquid layers as an interesting prototype ? nard-Marangoni problem.

Effectiveness for Ddtecting faults within and outside the scope of testing techniques: an independent replication

The verification and validation activity plays a fundamental role in improving software quality. Determining which the most effective techniques for carrying out this activity are has been an aspiration of experimental software engineering researchers for years. This paper reports a controlled experiment evaluating the effectiveness of two unit testing techniques (the functional testing technique known as equivalence partitioning (EP) and the control-flow structural testing technique known as branch testing (BT)). This experiment is a literal replication of Juristo et al. (2013).Both experiments serve the purpose of determining whether the effectiveness of BT and EP varies depending on whether or not the faults are visible for the technique (InScope or OutScope, respectively). We have used the materials, design and procedures of the original experiment, but in order to adapt the experiment to the context we have: (1) reduced the number of studied techniques from 3 to 2; (2) assigned subjects to experimental groups by means of stratified randomization to balance the influence of programming experience; (3) localized the experimental materials and (4) adapted the training duration. We ran the replication at the Escuela Politécnica del Ejército Sede Latacunga (ESPEL) as part of a software verification & validation course. The experimental subjects were 23 master?s degree students. EP is more effective than BT at detecting InScope faults. The session/program andgroup variables are found to have significant effects. BT is more effective than EP at detecting OutScope faults. The session/program and group variables have no effect in this case. The results of the replication and the original experiment are similar with respect to testing techniques. There are some inconsistencies with respect to the group factor. They can be explained by small sample effects. The results for the session/program factor are inconsistent for InScope faults.We believe that these differences are due to a combination of the fatigue effect and a technique x program interaction. Although we were able to reproduce the main effects, the changes to the design of the original experiment make it impossible to identify the causes of the discrepancies for sure. We believe that further replications closely resembling the original experiment should be conducted to improve our understanding of the phenomena under study.

A formalism and method for representing and reasoning with process models authored by subject matter experts

Enabling Subject Matter Experts (SMEs) to formulate knowledge without the intervention of Knowledge Engineers (KEs) requires providing SMEs with methods and tools that abstract the underlying knowledge representation and allow them to focus on modeling activities. Bridging the gap between SME-authored models and their representation is challenging, especially in the case of complex knowledge types like processes, where aspects like frame management, data, and control flow need to be addressed. In this paper, we describe how SME-authored process models can be provided with an operational semantics and grounded in a knowledge representation language like F-logic in order to support process-related reasoning. The main results of this work include a formalism for process representation and a mechanism for automatically translating process diagrams into executable code following such formalism. From all the process models authored by SMEs during evaluation 82% were well-formed, all of which executed correctly. Additionally, the two optimizations applied to the code generation mechanism produced a performance improvement at reasoning time of 25% and 30% with respect to the base case, respectively.

Effectiveness for detecting faults within and outside the scope of testing techniques: an independent replication

The verification and validation activity plays a fundamental role in improving software quality. Determining which the most effective techniques for carrying out this activity are has been an aspiration of experimental software engineering researchers for years. This paper reports a controlled experiment evaluating the effectiveness of two unit testing techniques (the functional testing technique known as equivalence partitioning (EP) and the control-flow structural testing technique known as branch testing (BT)). This experiment is a literal replication of Juristo et al. (2013). Both experiments serve the purpose of determining whether the effectiveness of BT and EP varies depending on whether or not the faults are visible for the technique (InScope or OutScope, respectively). We have used the materials, design and procedures of the original experiment, but in order to adapt the experiment to the context we have: (1) reduced the number of studied techniques from 3 to 2; (2) assigned subjects to experimental groups by means of stratified randomization to balance the influence of programming experience; (3) localized the experimental materials and (4) adapted the training duration. We ran the replication at the Escuela Polite?cnica del Eje?rcito Sede Latacunga (ESPEL) as part of a software verification & validation course. The experimental subjects were 23 master?s degree students. EP is more effective than BT at detecting InScope faults. The session/program and group variables are found to have significant effects. BT is more effective than EP at detecting OutScope faults. The session/program and group variables have no effect in this case. The results of the replication and the original experiment are similar with respect to testing techniques. There are some inconsistencies with respect to the group factor. They can be explained by small sample effects. The results for the session/program factor are inconsistent for InScope faults. We believe that these differences are due to a combination of the fatigue effect and a technique x program interaction. Although we were able to reproduce the main effects, the changes to the design of the original experiment make it impossible to identify the causes of the discrepancies for sure. We believe that further replications closely resembling the original experiment should be conducted to improve our understanding of the phenomena under study.

Histograms of oriented gradients for fast on-board vehicle verification

Histograms of Oriented Gradients (HoGs) provide excellent results in object detection and verification. However, their demanding processing requirements bound their applicability in some critical real-time scenarios, such as for video-based on-board vehicle detection systems. In this work, an efficient HOG configuration for pose-based on-board vehicle verification is proposed, which alleviates both the processing requirements and required feature vector length without reducing classification performance. The impact on classification of some critical configuration and processing parameters is in depth analyzed to propose a baseline efficient descriptor. Based on the analysis of its cells contribution to classification, new view-dependent cell-configuration patterns are proposed, resulting in reduced descriptors which provide an excellent balance between performance and computational requirements, rendering higher verification rates than other works in the literature.

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.

Muscarinic cholinergic regulation of cardiac myocyte ICa-L is absent in mice with targeted disruption of endothelial nitric oxide synthase

Cardiac myocytes have been shown to express constitutively endothelial nitric oxide synthase (eNOS) (nitric oxide synthase 3), the activation of which has been implicated in the regulation of myocyte L-type voltage-sensitive calcium channel current (ICa-L) and myocyte contractile responsiveness to parasympathetic nervous system signaling, although this implication remains controversial. Therefore, we examined the effect of the muscarinic cholinergic agonist carbachol (CCh) on ICa-L and contractile amplitude in isoproterenol (ISO)-prestimulated ventricular myocytes isolated from adult mice, designated eNOSnull mice, with targeted disruption of the eNOS gene. Although both eNOSnull and wild-type (WT) ventricular myocytes exhibited similar increases in ICa-L in response to ISO, there was no measurable suppression of ICa-L by CCh in cells from eNOSnull mice, in contrast to cells from WT mice. These results were reflected in the absence of an effect of CCh on the positive inotropic effect of ISO in eNOSnull myocytes. Also, unlike myocytes from WT animals, eNOSnull myocytes failed to exhibit an increase in cGMP content in response to CCh. Nevertheless, the pharmacologic nitric oxide donors 3-morpholino-sydnonimine and S-nitroso-acetyl-cystein increased cGMP generation and suppressed ISO-augmented ICa-L in eNOSnull cells, suggesting that the signal transduction pathway(s) downstream of eNOS remained intact. Of importance, activation of the acetylcholine-activated K+ channel by CCh was unaffected in atrial and ventricular eNOSnull myocytes. These results confirm the obligatory role of eNOS in coupling muscarinic receptor activation to cGMP-dependent control of ICa-L in cardiac myocytes.