Search

Se evaluó el perfil de cinco ácidos grasos en muestras del músculo Longissimus dorsi de 120 bovinos provenientes de 40 empresas ganaderas de trópico bajo, ubicadas en zonas declaradas libres de aftosa por vacunación y productoras de canales de alta calidad. Respecto del perfil de ácidos grasos de cadena larga se encontró que el promedio general del extracto etéreo fue de 7,41 ± 3,61% con un cv alto (48,80%); además, para esta variable se establecieron diferencias (P< 0,001) en cuanto al tipo de forraje y el suplemento utilizado para la alimentación de los animales, el tipo racial y entre empresas ganaderas; así mismo, hubo diferencias (P< 0,005) en cuanto el efecto de la condición sexual, la clasificación de la canal y el uso de hormonas. Para el total de ácidos grasos se encontró un promedio de 58,11 ± 8,44% distribuido con valores promedio para los ácidos grasos saturados de 30,61 ± 4,96% y para los ácidos grasos insaturados de 27,49 ± 4,23%, de los cuales el 22,87 ± 4,04% está compuesto por ácidos grasos monoinsaturados y el 4,61 ± 0,79% por ácidos grasos poliinsaturados. Con relación a los valores de extracto etéreo se encontró el mayor porcentaje en la raza Brangus (17,68 ± 3,75%), seguido por animales Cebú x Bos taurus y Cebú Brahman, con valores de 7,51 ± 4,76 y 7,30 ± 5,07%, respectivamente; el tipo racial Romosinuano puro y los cruces de Cebú con Romosinuano y Pardo Suizo presentaron los menores valores para esta variable.

Dentro del área Metropolitana de Medellín, la administración central de Sabaneta, cuenta con los mayores ingresos per cápita (dos millones de pesos anuales en 2013), cuatro veces más que Caldas y tres que Copacabana, Barbosa, Bello y Girardota; Le siguieron Medellín, con $1.5 millones, y Envigado e Itagüí con un promedio de $1.2 millones. Sin embargo la mejor dinámica en el recaudo, la presentó el municipio de la Estrella (73% entre 2009-2013); mientras que Bello lo redujo en 26%. Los recursos de Sabaneta, se sustentan en su esfuerzo fiscal; en la certificación en educación otorgada en 2010 (lo que le permitió elevar el gasto por alumno matriculado en educación pública en 163% entre 2009 y 2013.) y, aunque temporales, en los ingresos por ventas de terrenos y otros aportes de cofinanciación. Su gasto total por habitante, fue el más alto. Destinó hacia la Formación Bruta de Capital, un promedio de $804.600 pesos por habitante, seguido por Medellín ($348.400). En Salud pública, en 2013, ejecutó un promedio de $1.2 millones por cada afiliado al régimen subsidiado que cubrieron el 9,4% de la población. Classification JEL: H2, H11, H71, H72, H74, H75, H76

Dentro del area Metropolitana de Medellin, la administracion central de Sabaneta, cuenta con los 05res ingresos per capita (dos millones de pesos anuales en 2013), cuatro veces mas que Caldas y tres que Copacabana, Barbosa, Bello y Girardota; Le siguieron Medellin, con $1.5 millones, y Envigado e Itagui con un promedio de $1.2 millones. Sin embargo la mejor dinamica en el recaudo, la presento el municipio de la Estrella (73% entre 2009-2013); mientras que Bello lo redujo en 26%. Los recursos de Sabaneta, se sustentan en su esfuerzo fiscal; en la certificacion en educacion otorgada en 2010 (lo que le permitio elevar el gasto por alumno matriculado en educacion publica en 163% entre 2009 y 2013.) y, aunque temporales, en los ingresos por ventas de terrenos y otros aportes de cofinanciacion. Su gasto total por habitante, fue el mas alto. Destino hacia la Formacion Bruta de Capital, un promedio de $804.600 pesos por habitante, seguido por Medellin ($348.400). En Salud publica, en 2013, ejecuto un promedio de $1.2 millones por cada afiliado al regimen subsidiado que cubrieron el 9,4% de la poblacion.

This paper presents DAIDALUS (Detect and Avoid Alerting Logic for Unmanned Systems), a reference implementation of a detect and avoid concept intended to support the integration of Unmanned Aircraft Systems into civil airspace. DAIDALUS consists of self-separation and alerting algorithms that provide situational awareness to UAS remote pilots. These algorithms have been formally specified in a mathematical notation and verified for correctness in an interactive theorem prover. The software implementation has been verified against the formal models and validated against multiple stressing cases jointly developed by the US Air Force Research Laboratory, MIT Lincoln Laboratory, and NASA. The DAIDALUS reference implementation is currently under consideration for inclusion in the appendices to the Minimum Operational Performance Standards for Unmanned Aircraft Systems presently being developed by RTCA Special Committee 228.

• Overview of HITL DAA research and development work conducted at NASA Langley Research Center in support of the UAS in the NAS project • Three HITL experiments, CAS-1 and CAS-2 and CASSAT were briefly described, all part of the research plan designed to address interoperability and acceptability questions associated with the integration of UAS with manned aircraft operations in non-segregated airspace • Next steps in the research plan will address the impact of imperfect surveillance on SS algorithm performance and pilot's acceptability • Much research remains to be done to develop and validate the technology and operations needed for UAS integration without affecting the safety of the NAS.

Recursive branch and bound algorithms are often used, either rigorouslyor non-rigorously, to refine and isolate solutions to global optimizationproblems or systems of equations and inequalities involving nonlinearfunctions. The presented software library, Kodiak, integrates numericand symbolic computation into a generic framework for the solution of suchproblems over hyper-rectangular variable and parameter domains. Thecorrectness of both the generic branch and bound algorithm and the self-validating enclosure methods used, namely interval arithmetic and, for polynomials and rational functions, Bernstein expansion, has beenformally verified. The algorithm has three main instantiations, forsystems of equations and inequalities, for constrained global optimization, and for the computation of equilibria and bifurcation sets for systems ofordinary differential equations. For the latter category, and to enablethe computation of bisection heuristics to reduce the branching factor, advantage is taken of the partial derivatives of the constraint functions, which are symbolically manipulated. Pavings (unions of box subsets)for a continuum of solutions to underdetermined systems mayalso be produced. The capabilities of the software tool are outlined, andcomputational examples are presented.

El asma es la enfermedad crónica más frecuente en la niñez y conduce a múltiples complicaciones, fenómeno que en la actualidad representa un problema de salud pública. El reporte de síntomas bronco-obstructivos es mucho mayor que el diagnóstico médico de asma durante la infancia, hecho que sugiere que hay una tendencia a no reconocer que los niños en esta edad sufren de esta enfermedad y por tanto eventualmente se ocasiona retraso en su tratamiento. El rechazo a clasificar a los pacientes como asmáticos, la falta de un consenso diagnóstico, los múltiples fenotipos, la flexibilidad de las escalas de severidad y el desconocimiento del asma en la infancia como una enfermedad intermitente pero potencialmente grave, son factores del manejo médico que podrían favorecer una alta morbilidad. Esta revisión plantea la necesidad de ser más contundentes en el diagnóstico del asma en la infancia, sin caer en retrasos que permitan iniciar un tratamiento oportuno y adecuado.

In air traffic management, conflict detection algorithms are used to determine whether or not aircraft are predicted to lose horizontal and vertical separation minima within a time interval assuming a trajectory model. In the case of linear trajectories, conflict detection algorithms have been proposed that are both sound, i.e., they detect all conflicts, and complete, i.e., they do not present false alarms. In general, for arbitrary nonlinear trajectory models, it is possible to define detection algorithms that are either sound or complete, but not both. This paper considers the case of nonlinear aircraft trajectory models based on polynomial functions. In particular, it proposes a conflict detection algorithm that precisely determines whether, given a lookahead time, two aircraft flying polynomial trajectories are in conflict. That is, it has been formally verified that, assuming that the aircraft trajectories are modeled as polynomial functions, the proposed algorithm is both sound and complete.

Accuracy and correctness are central issues in numerical analysis. To address these issues, several self-validated computation methods have been proposed in the last fifty years. Their common goal is to provide rigorously correct enclosures for calculated values, sacrificing a measure of precision for correctness. Perhaps the most widely adopted enclosure method is interval arithmetic. Interval arithmetic performs well in a wide range of cases, but often produces excessively large overestimations, unless the domain is reduced in size, e.g., by subdivision. Many extensions of interval arithmetic have been developed in order to cope with this problem. Among them, affine arithmetic provides tighter estimations by taking into account linear correlations between operands. This paper presents a formalization of affine arithmetic, written in the Prototype Verification System (PVS), along with a formally verified branch-and-bound procedure implementing that model. This procedure and its correctness property enables the implementation of a PVS strategy for automatically computing upper and lower bounds of real-valued expressions that are provably correct up to a user-specified precision.

This paper explores a new approach to validating software implementations that have been produced from formally-verified algorithms. Although visual inspection gives some confidence that the implementations faithfully reflect the formal models, it does not provide complete assurance that the software is correct. The proposed approach, which is based on animation of formal specifications, compares the outputs computed by the software implementations on a given suite of input values to the outputs computed by the formal models on the same inputs, and determines if they are equal up to a given tolerance. The approach is illustrated on a prototype air traffic management system that computes simple kinematic trajectories for aircraft. Proofs for the mathematical models of the system’s algorithms are carried out in the Prototype Verification System (PVS). The animation tool PVSio is used to evaluate the formal models on a set of randomly generated test cases. Output values computed by PVSio are compared against output values computed by the actual software. This comparison improves the assurance that the translation from formal models to code is faithful and that, for example, floating point errors do not greatly affect correctness and safety properties.

Safety assessment of new air traffic management systems is a main issue for civil aviation authorities. Standard techniques such as testing and simulation have serious limitations in new systems that are significantly more autonomous than the older ones. In this paper, we present an innovative approach for establishing the correctness of conflict detection systems. Fundamental to our approach is the concept of trajectory, and how we represent a continuous physical trajectory by a continuous path in the x-y plane constrained by physical laws and operational requirements. From the model of trajectories, we extract, and formally prove, high-level properties that can serve as a framework to analyze conflict scenarios. We use the AILS (Airborne Information for Lateral Spacing) alerting algorithm as a case study of our approach.

For the study of nonlinear dynamic systems, it is important to locate the equilibria and bifurcations occurring within a specified computational domain. This paper proposes a new approach for solving these problems and compares it to the numerical continuation method. The new approach is based upon branch and bound and utilizes rigorous enclosure techniques to yield outer bounding sets of both the equilibrium and local bifurcation manifolds. These sets, which comprise the union of hyper-rectangles, can be made to be as tight as desired. Sufficient conditions for the existence of equilibrium and bifurcation points taking the form of algebraic inequality constraints in the state-parameter space are used to calculate their enclosures directly. The enclosures for the bifurcation sets can be computed independently of the equilibrium manifold, and are guaranteed to contain all solutions within the computational domain. A further advantage of this method is the ability to compute a near-maximally sized hyper-rectangle of high dimension centered at a fixed parameter-state point whose elements are guaranteed to exclude all bifurcation points. This hyper-rectangle, which requires a global description of the bifurcation manifold within the computational domain, cannot be obtained otherwise. A test case, based on the dynamics of a UAV subject to uncertain center of gravity location, is used to illustrate the efficacy of the method by comparing it with numerical continuation and to evaluate its computational complexity.

Con base en el trabajo etnográfico que supone de acompañamiento de familiares de personas desaparecidas, el artículo analiza cómo, históricamente, la racionalización de la muerte, un fenómeno típicamente occidental, ha devenido en procesos de exclusión y de doble negación del otro: de su vida y de su muerte. El ensayo finaliza con algunas consideraciones deliberadamente inconclusas sobre las representaciones mediáticas sobre la muerte y la desaparición forzada. Based on ethnographic work involved accompanying relatives of missing persons, the article analyzes how, historically, the rationalization of death, a typically Western phenomenon, has developed in a process of exclusion and double negation of the other:both his own life and his death. The essay ends with some deliberately unfinished thoughts about media representations of death and forced disappearance

This paper proposes a mathematical definition of an aircraft-separation criterion for kinematic-based horizontal maneuvers. It has been formally proved that kinematic maneu- vers that satisfy the new criterion are independent and coordinated for repulsiveness, i.e., the distance at closest point of approach increases whether one or both aircraft maneuver according to the criterion. The proposed criterion is currently used in NASA's Airborne Coordinated Resolution and Detection (ACCoRD) set of tools for the design and analysis of separation assurance systems.

The FAA-sponsored Sense and Avoid Workshop for Unmanned Aircraft Systems (UAS) defines the concept of sense and avoid for remote pilots as "the capability of a UAS to remain well clear from and avoid collisions with other airborne traffic." Hence, a rigorous definition of well clear is fundamental to any separation assurance concept for the integration of UAS into civil airspace. This paper presents a family of well-clear boundary models based on the TCAS II Resolution Advisory logic. For these models, algorithms that predict well-clear violations along aircraft current trajectories are provided. These algorithms are analogous to conflict detection algorithms but instead of predicting loss of separation, they predict whether well-clear violations will occur during a given lookahead time interval. Analytical techniques are used to study the properties and relationships satisfied by the models.

This paper presents a formalization in higher-order logic of a generic algorithm that is used in automated strategies for solving global optimization problems. It is a generalization of numerical branch and bound algorithms that compute the minimum of a function on a given domain by recursively dividing the domain and computing estimates for the range of the function on each sub-domain. The correctness statement of the algorithm has been proved in the Prototype Verification System PVS theorem prover. This algorithm can be instantiated with specific functions for performing particular global optimization methods. The correctness of the instantiated algorithms is guaranteed by simple properties that need to be verified on the specific input functions. The use of the generic algorithm is illustrated with an instantiation that yields an automated strategy in PVS for estimating the maximum and minimum values of real-valued functions.

This paper presents an algorithm for checking temporal precedence properties of nonlinear switched systems. This class of properties subsume bounded safety and capture requirements about visiting a sequence of predicates within given time intervals. The algorithm handles nonlinear predicates that arise from dynamics-based predictions used in alerting protocols for state-of-the-art transportation systems. It is sound and complete for nonlinear switch systems that robustly satisfy the given property. The algorithm is implemented in the Compare Execute Check Engine C2E2 using validated simulations. As a case study, a simplified model of an alerting system for closely spaced parallel runways is considered. The proposed approach is applied to this model to check safety properties of the alerting logic for different operating conditions such as initial velocities, bank angles, aircraft longitudinal separation, and runway separation.

Typed λ-terms are used as a compact and linear representation of proofs in intuitionistic logic. This is possible since the Curry-Howard isomorphism relates proof-trees with typed λ-terms. The proofs-as-terms principle can be used to verify the validity of a proof by type checking the λ term extracted from the complete proof-tree. In this paper we present a proof synthesis method for dependent-type systems where typed open terms are built incrementally at the same time as proofs are done. This way, every construction step, not just the last one, may be type checked. The method is based on a suitable calculus where substitutions as well as meta-variables are first-class objects. Copyright 2001 Elsevier Science B.V.

We present a dependent-type system for a λ-calculus with explicit substitutions. In this system, meta-variables, as well as substitutions, are first-class objects. We show that the system enjoys properties like type uniqueness, subject reduction, soundness, confluence, and weak normalization.

El lector apreciará en este texto una semblanza sobre Mario Cárdenas Ayaipoma, quien llegara a ser ex director general del Archivo Histórico del Archivo General de la Nación del Perú y presidente de la Asociación Peruana de Archiveros. Este repaso lleno de afecto por su trayectoria abordará, además de sus primeros años de formación, su paso por importantes instituciones relacionados a los estudios archivísticos. Cabe destacar que el texto cuenta con un post scriptum donde se relata acontecimientos recientes relacionados a este importante archivero peruano.

The Traffic Alert and Collision Avoidance System (TCAS) is a family of airborne systems designed to reduce the risk of mid-air collisions between aircraft. TCAS~II, the current generation of TCAS devices, provides resolution advisories that direct pilots to maintain or increase vertical separation when aircraft distance and time parameters are beyond designed system thresholds. This paper presents a mathematical model of the TCAS~II Resolution Advisory (RA) logic that assumes accurate aircraft state information. Based on this model, an algorithm for RA detection is also presented. This algorithm is analogous to a conflict detection algorithm, but instead of predicting loss of separation, it predicts resolution advisories. It has been formally verified that for a kinematic model of aircraft trajectories, this algorithm completely and correctly characterizes all encounter geometries between two aircraft that lead to a resolution advisory within a given lookahead time interval. The RA detection algorithm proposed in this paper is a fundamental component of a NASA sense and avoid concept for the integration of Unmanned Aircraft Systems in civil airspace.

Este articulo analiza la evolucion entre 2007 y 2011, de las cifras fiscales de las seis ciudades con 05res ingresos en 2011 en Colombia: Bogota, Medellin, Cali, Barranquilla, Cartagena y Bucaramanga. La ciudad que registro 05res progresos en terminos de esfuerzo fiscal en el periodo analizado fue Barranquilla, seguida de Bucaramanga. Mas recientemente, Cartagena tambien incremento en forma destacable sus ingresos propios. Cuando se califica el desempeno fiscal con base en la magnitud del gasto por habitante que sea sostenible para las ciudades, Medellin se resalta en el primer lugar, seguida relativamente de cerca de Bogota. Barranquilla y Cartagena vendrian despues, con cierta distancia de las dos primeras; posteriormente Bucaramanga, y finalmente, y con un desempeno bastante pobre, Cali.

Numerical algorithms lie at the heart of many safety-critical aerospace systems. The complexity and hybrid nature of these systems often requires the use of interactive theorem provers to verify that these algorithms are logically correct. Usually, proofs involving numerical computations are conducted in the infinitely precise realm of the field of real numbers. However, numerical computations in these algorithms are often implemented using floating point numbers. The use of a finite representation of real numbers introduces uncertainties as to whether the properties verified in the theoretical setting hold in practice. This short paper describes work in progress aimed at addressing these concerns. Given a formally proven algorithm, written in the Program Verification System (PVS), the Frama-C suite of tools is used to identify sufficient conditions and verify that under such conditions the rounding errors arising in a C implementation of the algorithm do not affect its correctness. The technique is illustrated using an algorithm for detecting loss of separation among aircraft.

El presente artículo reúne las reflexiones esbozadas por el autor sobre el papel del convencionalismo y su aplicación en el campo del Derecho interno nacional de los países firmantes, específicamente en lo referido al contexto colombiano. Se hace un recorrido por la Convención Americana sobre Derechos Humanos “Pacto de San José de Costa Rica” y se revisan las disposiciones y efectos que en materia de tributación contienen dichos convenios.

Our previous work presented an approach for developing high confidence algorithms for recovering aircraft from loss of separation situations. The correctness theorems for the algorithms relied on several key assumptions, namely that state data for all local aircraft is perfectly known, that resolution maneuvers can be achieved instantaneously, and that all aircraft compute resolutions using exactly the same data. Experiments showed that these assumptions were adequate in cases where the aircraft are far away from losing separation, but are insufficient when the aircraft have already lost separation. This paper describes the results of this experimentation and proposes a new criteria specification for loss of separation recovery that preserves the formal safety properties of the previous criteria while overcoming some key limitations. Candidate algorithms that satisfy the new criteria are presented.

This paper analyzes priority rules, such as those in Part 91.113 of the Federal Aviation Regulations. Such rules determine which of two aircraft should maneuver in a given conflict scenario. While the rules in 91.113 are well accepted, other concepts of operation for NextGen, such as self separation, may allow for different priority rules. A mathematical framework is presented that can be used to analyze a general set of priority rules and enables proofs of important properties. Specific properties considered in this paper include safety, effectiveness, and stability. A set of rules is said to be safe if it ensures that it is never the case that both aircraft have priority. They are effective if exactly one aircraft has priority in every situation. Finally, a set of rules is called stable if it produces compatible results even under small changes to input data.

The International Energy Agency (IEA) predicts an important increment of primary energy demand until 2030. The electricity generation sector expects that world’s demand gets duplicated, which would mean the installation of new plants up to an additional global capacity of 5,000 GWe. This huge increment of the demand, together with other economic factors, will give fossil fuels (coal, gas and oil) a key role within the energy field.

The Prototype Verification System (PVS) is an interactive verification environment that combines a strongly typed specification language with a classical higher-order logic theorem prover. The PVS type system supports: predicate subtypes, dependent types, abstract data types, compound types such as records, unions, and tuples, and basic types such as numbers, Boolean values, and strings. The PVS theorem prover includes decision procedures for a variety of theories such as linear arithmetic, propositional logic, and temporal logic. This paper surveys advanced PVS features, including: types for specifications, implicit induction, iterations, rapid prototyping, strategy writing, and computational reflection. These features are illustrated with simple examples taken from NASA PVS developments.

The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL's Formal Interactive Verification Environment (PLEXIL5), a graphical interface to the formal executable semantics of PLEXIL. Among its main features, PLEXIL5 provides model checking of plans with support for formula editing and visualization of counterexamples, interactive simulation of plans at different granularity levels, and random initialization of external environment variables. The formal verification capabilities of PLEXIL5 are illustrated by means of a human-automation interaction model.

En una era disgustada con los politicos y los diversos instrumentos de democracia directa, El publico fantasma de Walter Lippmann no ha perdido un apice de actualidad. Esta obra nos muestra al Lippmann mas critico de la democracia americana. De sentimiento antipopulista, este libro defiende el elitismo como una opcion intelectual seria y distintiva que cuenta con una larga tradicion en America. La vision desmitificadora del sistema americano de Lippmann resuena en el presente. Walter Lippmann (Nueva York, 1889-1974), estudio en Harvard y en 1914, comenzo a colaborar, invitado por Herbert Croly, en la revista politica semanal New Republic. Durante la I Guerra Mundial trabajo con el presidente Woodrow Wilson en su programa de 14 puntos para la Paz y el nuevo orden mundial. En 1918 fue nombrado capitan de la inteligencia militar. Acabada la guerra, escribio asiduamente en Vanity Fair y pronto paso a trabajar en la redaccion de un gran periodico de la familia Pulitzer, New York World, cuya pagina editorial dirigira desde marzo de 1924. Al cerrarse el World, en septiembre de 1931, inicio su labor periodistica en el New York Herald Tribune, donde alcanzaria enorme fama con su columna Today and Tomorrow. Su labor como periodista la compagino con la publicacion de varios ensayos de exito, como Public Opinion (1922), del que The Phantom Public seria una continuacion. Su prestigio profesional, y sus sagaces analisis de la politica internacional. Le convirtieron en consejero aulico de todos los grandes presidentes democratas de EE.UU. (Wilson, Roosevelt, Kennedy...). Tras la II Guerra Mundial acaparo la atencion internacional con sus pioneros articulos sobre la "Guerra fria" (1947), defendio el espacio de influencia sovietico en Europa y se mostro critico con la politica norteamericana en temas como el McCarthysmo o la guerra de Vietnam. Convertido en un periodista de referencia, desde 1963 prosiguio sus celebres columnas en el Washington Post y Newsweek.

Metal vinyl acetate (MVAc) colloids were obtained by cocondensation at 77 K of the monomer with several metals such as: Pd, Ag, Au, Zn, Cd, Ga, In, Ge, Sn, Sb and Bi. Some of these colloids are stable for months at room temperature (Au, Ag, Pd). The colloids were polymerized with different amounts of initiator (2,2′-azoisobutyronitrile) at 65°C, and a wide range of viscosity-average molecular weights (104 < Mv < 106) were obtained depending upon the metal used. The particle size of these clusters dispersed in the polymer matrix is around 1400 A. The polymers are stable even at 320°C, and the metal content is ranging from 0,01 to 0,96 wt.-%. The color of the polymers depends upon the metal used.

La histoplasmosis, micosis sistémica y endémica en una amplia zona de las Américas, es causada por el hongo dimórfico Histoplasma capsulatum. Tradicionalmente, el diagnóstico de esta entidad se realiza por métodos microbiológicos directos y biopsias que emplean una variedad de coloraciones especiales tales como Wright, Giemsa y plata metenamina, entre otras, así como por cultivo; este último representa el estándar de oro. Se emplean, igualmente, métodos indirectos que incluyen la detección de anticuerpos y antígenos. Los valores de sensibilidad y especificidad en ambos métodos son variables, y los resultados dependen, a su vez, de la forma clínica de la enfermedad que presente el paciente y de su estado inmune. Recientemente, la biología molecular ha permitido introducir nuevas herramientas que han sido utilizadas para la detección e identificación de H.capsulatum, una de ellas es la PCR anidada que se caracteriza por sus altos niveles de sensibilidad y especificidad. De igual forma, estas técnicas moleculares han permitido realizar análisis evolutivos, estudios de diversidad genética y un sinnúmero de estudios de epidemiología molecular, a partir de los cuales se ha logrado recopilar información valiosa sobre la variabilidad genética de este microorganismo. En esta revisión se describen los métodos de laboratorio convencionales y las técnicas moleculares más empleadas para el diagnóstico de la histoplasmosis; así como también algunas de sus aplicaciones en la epidemiología y biología molecular de este hongo.Histoplasma capsulatum is the causative agent of histoplasmosis, a systemic and endemic mycosis widely distributed in the Americas. Diagnosis of histoplasmosis is traditionally accomplished by means of direct preparations and biopsies stained by especial methods, as well as by isolation of fungus in culture; the latter is considered the gold standard. Indirect methods, including immunological tests to detect antibodies and/or antigens, are also valuable; both direct and indirect methods present sensitivity and specificity ranges that vary depending on the clinical form of the disease and the immune status of the host. Recently, molecular biology has allowed implementing new tools to detect and identify H. capsulatum, and several molecular tests, such as nested-PCR, are being used for the diagnosis of histoplasmosis, and so provide high sensitivity and specificity values. In addition, these molecular techniques have made it possible to perform evolution analysis, genetic diversity research, and molecular epidemiology, thus compiling valuable information on the genetic variability of this microorganism. In this review, the conventional and molecular methods employed for the diagnosis of histoplasmosis have been described, as have some of the applications of these molecular techniques to this fungal pathogen's epidemiology and molecular biology.

In air traffic management, conflict prevention information refers to the guidance maneuvers, which if taken, ensure that an aircraft's path is conflict-free. These guidance maneuvers take the form of changes to track angle or ground speed. Conflict prevention information may be assembled into prevention bands that advise the crew on maneuvers that should not be taken. Unlike conflict resolution systems, which presume that the aircraft already has a conflict, conflict prevention systems show conflicts for any maneuver, giving the pilot confidence that if a maneuver is made, then no near-term conflicts will result. Because near-term conflicts can lead to safety concerns, strong verification of information correctness is required. This paper presents a mathematical framework to analyze the correctness of algorithms that produce conflict prevention information incorporating an arbitrary number of traffic aircraft and with both a near-term and intermediate-term lookahead times. The framework is illustrated with a formally verified algorithm for 2-dimensional track angle prevention bands.

The Automation for Operations project (A4O), which is part of NASA’s Exploration Technology Development Program, aims at advancing automation technology in support of spacecraft operations. Procedures that encode the means by which spacecraft systems are operated are a critical target of automation technology. In this paper, we present a static verification tool for NASA’s Procedure Representation Language (PRL), a XMLbased notation for specifying manual and autonomous operation procedures. The tool checks PRL files for valid syntactical structure and semantics, ensures that procedures are invoked correctly, consults a system-representation database to validate usage constraints, and, finally, verifies the consistency of logical conditions using a constraint solver. All these checks are implemented statically, i.e., at the moment when procedures are being created, before they are deployed and executed. The tool has been fully integrated into the Procedure Integrated Development Environment (PRIDE), a PRL authoring and editor environment developed by NASA.

The marriage of model checking and planning faces two seemingly diverging alternatives: the need for a planning language expressive enough to capture the complexity of real-life applications, as opposed to a language simple, yet robust enough to be amenable to exhaustive verification and validation techniques. In an attempt to reconcile these differences, we have designed an abstract plan description language, ANMLite, inspired from the Action Notation Modeling Language (ANML). We present the basic concepts of the ANMLite language as well as an automatic translator from ANMLite to the model checker SAL (Symbolic Analysis Laboratory). We discuss various aspects of specifying a plan in terms of constraints and explore the implications of choosing a robust logic behind the specification of constraints, rather than simply propose a new planning language. Additionally, we provide an initial assessment of the efficiency of model checking to search for solutions of planning problems. To this end, we design a basic test benchmark and study the scalability of the generated SAL models in terms of plan complexity.

This paper presents PLEXIL5, PLEXIL's formal interacting visual environment, a graphical environment providing an user-friendly interface to the formal operational semantics of PLEXIL. PLEXIL is a synchronous plan execution language developed by NASA to support autonomous space operations. PLEXIL5 serves as a testbed for designers, developers and users of PLEXIL's executive system to validate, maintain, and debug the implementation of the system against the formal semantics of the language. The executable formal semantics of PLEXIL is an executable rewriting logic theory in Maude's language., Este documento presenta PLEXIL5, el entorno visual interactivo formal de PLEXIL, un entorno gráfico que proporciona una interfaz fácil de usar para la semántica operativa formal de PLEXIL. PLEXIL es un lenguaje de ejecución de planes sincrónicos desarrollado por la NASA para respaldar las operaciones espaciales autónomas. PLEXIL5 sirve como banco de pruebas para diseñadores, desarrolladores y usuarios del sistema ejecutivo de PLEXIL para validar, mantener y depurar la implementación del sistema contra la semántica formal del lenguaje. La semántica formal ejecutable de PLEXIL es una teoría lógica de reescritura ejecutable en el lenguaje de Maude.

are combined. Formal methods achieve this by using symbolic methods of analysis, and it is the computational complexity of these symbolic methods that limits and complicates their application. Recently, new methods and tools for symbolic analysis have been developed that are far more ecient and eective in practice than earlier methods. These include solvers for “satisfiability modulo theories” (SMT solvers) and methods for using these to analyze discrete and hybrid (i.e., mixed discrete and continuous) systems. In addition, new ways to apply these capabilities have been developed, such as their use for test generation, and controller synthesis, in addition to analysis. In this paper, we outline these new methods, and describe a project to extend and apply them in combination to issues in verification and testing of diagnostic and monitoring systems.

In this chapter we investigate real-time extensions for evolutionary mobile robot learning. The learning performance is measured in navigation experiments of complex environments as performed in a Kephera mobile robot simulator (YAKS). All these experiments are done in the context of our recently introduced motivation based interface that provides an intuitive human-robot communications mechanism (Arredondo et al., 2006). This motivation interface has been used in a variety of behavior based navigation and environment recognition tasks (Freund et al., 2006). Our first heuristic introduces active battery level sensors and recharge zones, which are used as soft deadlines to improve robot behavior for reaching survivability in environment exploration. Based on our previously defined model, we also propose a hard deadline based hybrid controller for a mobile robot, combining behavior-based and mission-oriented control mechanisms. These methods are implemented and applied in action sequence based environment exploration tasks in a YAKS mobile robot simulator. We validate our techniques with several sets of configuration parameters on different scenarios. We consider soft-deadlines as a dangerous but not critical battery charge level which affect a robot's fitness. Hard-deadlines are considered as a possible (because of partial knowledge) point where, if the robot does not recharge his battery, an unrecoverable final freezing state is possible. Our tests include action sequence based environment exploration tasks. These experiments show a significant improvement in robot responsiveness regarding survivability and environment exploration when using these real-time based methods. The rest of the chapter is organized as follows. In Section 2 a description of our soft-computing based navigation model is given. In Section 3 real-time extensions of our model are presented. In Section 4 we show the experimental setup and test results. Finally, in Section 5 some conclusions and future work are drawn.

The TPHOLs International Conference serves as a venue for the presentation of work in theorem proving in higher-order logics and related areas in deduction, formal specification, software and hardware verification, and other applications. Fourteen papers were submitted to Track B (Work in Progress), which are included in this volume. Authors of Track B papers gave short introductory talks that were followed by an open poster session. The FCM 2002 Workshop aimed to bring together researchers working on the formalisation of continuous mathematics in theorem proving systems with those needing such libraries for their applications. Many of the major higher order theorem proving systems now have a formalisation of the real numbers and various levels of real analysis support. This work is of interest in a number of application areas, such as formal methods development for hardware and software application and computer supported mathematics. The FCM 2002 consisted of three papers, presented by their authors at the workshop venue, and one invited talk.

Highly accurate positioning systems and new broadcasting technology have enabled air traffic management concepts where the responsibility for aircraft separation resides on pilots rather than on air traffic controllers. The Formal Methods Group at the National Institute of Aerospace and NASA Langley Research Center has proposed and formally verified an algorithm, called KB3D, for distributed three dimensional conflict resolution. KB3D computes resolution maneuvers where only one component of the velocity vector, i.e., ground speed, vertical speed, or heading, is modified. Although these maneuvers are simple to implement by a pilot, they are not necessarily optimal from a geometrical point of view. In general, optimal resolutions require the combination of all the components of the velocity vector. In this paper, we propose a two dimensional version of KB3D, which we call KB2D, that computes resolution maneuvers that are optimal with respect to ground speed and heading changes. The algorithm has been mechanically verified in the Prototype Verification System (PVS). The verification relies on algebraic proof techniques for the manipulation of the geometrical concepts relevant to the algorithm as well as standard deductive techniques available in PVS.

We provide sufficient conditions that formally guarantee that the floating-point computation of a polynomial evaluation is faithful. To this end, we develop a formalization of floating-point numbers and rounding modes in the Program Verification System (PVS). Our work is based on a well-known formalization of floating-point arithmetic in the proof assistant Coq, where polynomial evaluation has been already studied. However, thanks to the powerful proof automation provided by PVS, the sufficient conditions proposed in our work are more general than the original ones.

In this paper we investigate real-time adaptive extensions of our fuzzy logic based approach for providing biologically based motivations to be used in evolutionary mobile robot learning. The main idea is to introduce active battery level sensors and recharge zones to improve robot behavior for reaching survivability in environment exploration. In order to achieve this goal, we propose an improvement of our previously defined model, as well as a hybrid controller for a mobile robot, combining behavior-based and mission-oriented control mechanism. This method is implemented and tested in action sequence based environment exploration tasks in a Khepera mobile robot simulator. We investigate our technique with several sets of configuration parameters and scenarios. The experiments show a significant improvement in robot responsiveness regarding survivability and environment exploration.

Verification of programs relies on reasoning about the computations they perform. In engineering programs, many of these computations are non-linear. Although predicate abstraction enables model checking of programs with large state spaces, the decision procedures that currently support predicate abstraction are not able to handle such non-linear computations. In this paper, we propose an approach to model checking a class of data-flow properties for engineering programs that contain non-linear products and transcendental functions. The novelty of our approach is the integration of interval constraint solving techniques into the automated predicate discovery/predicate abstraction process, which extends the expressive power of predicate abstraction-based model checking. Using this approach, we construct a prototype model checker for C programs called VISA (Verification of Industrial-Strength Applications). VISA is built on top of Berkeley's BLAST and University of Nantes' Realpaver. We successfully apply VISA to scientific computation libraries and avionics applications to verify the absence of certain runtime arithmetic errors.

In test generation based on model-checking, white-box test criteria are represented as trap conditions written in a temporal logic. A model checker is used to refute trap conditions with counter-examples. From a feasible counter-example test inputs are then generated. The major problems of applying this approach to engineering applications derive from the fact that engineering programs have an infinite state space and non-linear numerical computations. Our solution is to combine predicate abstraction (which reduces the state space) with a numerical decision procedure (which supports predicate abstraction by solving non-linear constraints) based on interval analysis. We have developed a prototype and applied it to MC/DC (Modified Condition/Decision Coverage) test case generation. We have used the prototype on a number of C modules taken from a conflict detection and avoidance system and from a Boeing 737 autopilot simulator. The modules range from tens of lines up to thousands of lines in size. Our experience shows that although in theory the inclusion of a decision procedure for non-linear arithmetic may lead to non-terminating behavior and false positives (as abstraction-based model checking already does), our prototype is able to automatically produce feasible counterexamples with only a few exceptions. Furthermore, the process runs with acceptable execution times, without requiring any other knowledge of the specification, and without tampering with the original C programs.