Verificación Formal de Sistemas basada Formal Software Verification based on Automated Analysisen Análisis Automático.

Identificación y caracterización del problema. Uno de los problemas más importantes asociados con la construcción de software es la corrección del mismo. En busca de proveer garantías del correcto funcionamiento del software, han surgido una variedad de técnicas de desarrollo con sólidas bases matemáticas y lógicas conocidas como métodos formales. Debido a su naturaleza, la aplicación de métodos formales requiere gran experiencia y conocimientos, sobre todo en lo concerniente a matemáticas y lógica, por lo cual su aplicación resulta costosa en la práctica. Esto ha provocado que su principal aplicación se limite a sistemas críticos, es decir, sistemas cuyo mal funcionamiento puede causar daños de magnitud, aunque los beneficios que sus técnicas proveen son relevantes a todo tipo de software. Poder trasladar los beneficios de los métodos formales a contextos de desarrollo de software más amplios que los sistemas críticos tendría un alto impacto en la productividad en tales contextos. Hipótesis. Contar con herramientas de análisis automático es un elemento de gran importancia. Ejemplos de esto son varias herramientas potentes de análisis basadas en métodos formales, cuya aplicación apunta directamente a código fuente. En la amplia mayoría de estas herramientas, la brecha entre las nociones a las cuales están acostumbrados los desarrolladores y aquellas necesarias para la aplicación de estas herramientas de análisis formal sigue siendo demasiado amplia. Muchas herramientas utilizan lenguajes de aserciones que escapan a los conocimientos y las costumbres usuales de los desarrolladores. Además, en muchos casos la salida brindada por la herramienta de análisis requiere cierto manejo del método formal subyacente. Este problema puede aliviarse mediante la producción de herramientas adecuadas. Otro problema intrínseco a las técnicas automáticas de análisis es cómo se comportan las mismas a medida que el tamaño y complejidad de los elementos a analizar crece (escalabilidad). Esta limitación es ampliamente conocida y es considerada crítica en la aplicabilidad de métodos formales de análisis en la práctica. Una forma de atacar este problema es el aprovechamiento de información y características de dominios específicos de aplicación. Planteo de objetivos. Este proyecto apunta a la construcción de herramientas de análisis formal para contribuir a la calidad, en cuanto a su corrección funcional, de especificaciones, modelos o código, en el contexto del desarrollo de software. Más precisamente, se busca, por un lado, identificar ambientes específicos en los cuales ciertas técnicas de análisis automático, como el análisis basado en SMT o SAT solving, o el model checking, puedan llevarse a niveles de escalabilidad superiores a los conocidos para estas técnicas en ámbitos generales. Se intentará implementar las adaptaciones a las técnicas elegidas en herramientas que permitan su uso a desarrolladores familiarizados con el contexto de aplicación, pero no necesariamente conocedores de los métodos o técnicas subyacentes. Materiales y métodos a utilizar. Los materiales a emplear serán bibliografía relevante al área y equipamiento informático. Métodos. Se emplearán los métodos propios de la matemática discreta, la lógica y la ingeniería de software. Resultados esperados. Uno de los resultados esperados del proyecto es la individualización de ámbitos específicos de aplicación de métodos formales de análisis. Se espera que como resultado del desarrollo del proyecto surjan herramientas de análisis cuyo nivel de usabilidad sea adecuado para su aplicación por parte de desarrolladores sin formación específica en los métodos formales utilizados. Importancia del proyecto. El principal impacto de este proyecto será la contribución a la aplicación práctica de técnicas formales de análisis en diferentes etapas del desarrollo de software, con la finalidad de incrementar su calidad y confiabilidad. A crucial factor for software quality is correcteness. Traditionally, formal approaches to software development concentrate on functional correctness, and tackle this problem basically by being based on well defined notations founded on solid mathematical grounds. This makes formal methods better suited for analysis, due to their precise semantics, but they are usually more complex, and require familiarity and experience with the manipulation of mathematical definitions. So, their acceptance by software engineers is rather restricted, and formal methods applications have been confined to critical systems. Nevertheless, it is obvious that the advantages that formal methods provide apply to any kind of software system. It is accepted that appropriate software tool support for formal analysis is essential, if one seeks providing support for software development based on formal methods. Indeed, some of the relatively recent sucesses of formal methods are accompanied by good quality tools that automate powerful analysis mechanisms, and are even integrated in widely used development environments. Still, most of these tools either concentrate on code analysis, and in many cases are still far from being simple enough to be employed by software engineers without experience in formal methods. Another important problem for the adoption of tool support for formal methods is scalability. Automated software analysis is intrinsically complex, and thus techniques do not scale well in the general case. In this project, we will attempt to identify particular modelling, design, specification or coding activities in software development processes where to apply automated formal analysis techniques. By focusing in very specific application domains, we expect to find characteristics that might be exploited to increase the scalability of the corresponding analyses, compared to the general case.

Ciclos económicos en economías abiertas y menos desarrolladas: el papel de los "shocks" en los términos de intercambio.The business cycle in open and less developed economies: the rol of terms-of-trade shocks.

Nuestra preocupación reside en estudiar empíricamente el mecanismo de transmisión internacional de ciclos económicos a economías pequeñas y menos desarrolladas (LDC), evaluando el impacto de los shocks en los términos de intercambio en países dónde existen imperfecciones en el mercado crediticio que imponen severas restricciones en el financiamiento de la inversión doméstica y al crecimiento económico. Primero, analizamos si la cuenta corriente responde de manera asimétrica a movimientos de largo plazo en los términos de intercambio. La hipótesis es que “en los buenos tiempos” cuando se produce una mejora permanente en términos de intercambio (y con ello el nivel de ingreso) los individuos no elevan su consumo en un monto acorde con la mejora de su ingreso (permanente) sino que ahorran una fracción del aumento en su dotación para hacer frente a una reversión en la mejora en los términos de intercambios (aunque ésta sea transitoria) en el futuro. En consecuencia, la cuenta corriente (diferencia entre ingreso y absorción) responde de manera positiva a un shock permanente en los términos de intercambio, ya que el individuo ahorra de manera cautelosa –debido a que sabe que no le prestarán para suavizar consumo - aún suponiendo que en el futuro tendrá una reversión transitoria de su ingreso. Segundo, estudiamos la relación dinámica entre los términos de intercambio y la tasa de interés en la economía pequeña abierta y con imperfecciones en el mercado crediticio (información asimétrica). La hipótesis es que la economía doméstica tiene que soportar una prima de riesgo que eleva el costo de la inversión y retarda el crecimiento (Gertler y Rogoff; 1990). Esta prima de riesgo depende, además, en forma negativa del nivel del colateral que tenga la economía. El colateral es la dotación de recursos naturales, por ejemplo, que la economía posee a los fines garantizar el cumplimiento de las obligaciones contraídas (en el modelo presentado las actividades dónde se invierten son independientes del colateral). La hipótesis establecida indica que los cambios en los términos de intercambio generan un aumento del colateral de la economía y una reducción del riesgo país: aumentos en los términos de intercambio reducen la prima de riesgo de la economía que opera en mercados de capitales con asimetrías de información, y como consecuencia aumentarían los ingresos de capitales. De esta forma, se estaría encontrando una explicación a la denominada “Paradoja de Lucas”. Finalmente, el proyecto estudia la conexión entre dos variables “clave” en la economía de los países emergentes: la relación entre los términos de intercambio y el tipo de cambio real. Argumentamos que los efectos de las mejoras de los términos de intercambio sobre los flujos de capitales externos tienden a ser sobreestimadas si no se consideran los efectos “secundarios” de éstas sobre el tipo de cambio real de la economía pequeña menos desarrollada. En este proyecto se controlan estadísticamente esta relación. La estrategia empírica elegida resulta en aplicar a un panel (constituido por dieciocho países de Latinoamérica) el método generalizado de momentos (GMM) a dos modelos de regresión estadística a los fines de abordar de manera eficiente el problema de la endogeneidad de la variable dependiente que actúa como regresor rezagado. La estrategia de estimación elegida enfatiza el análisis de la relación dinámica de las variables económicas incluidas en el análisis. The paper analyzes the general problem related to the transmission of economic cycles to Small Open Economies. The analysis focuses on terms-of-trade shocks, which are considered one of the major sources of income volatility in developing economies. Specifically, we tackle the problem related to the impact of terms-of-trade shocks in Less Developed SOEs. ‘Less Developed SOEs’ are understood as those countries who have borrowing constraints. First, we put to a test the hypothesis of asymmetric response of current account to terms-of-trade shocks (the impact of the shock on current account differs depending whether it is positive or negative), which originates from considering binding restrictions in international capital markets (Agénor and Aizenman; 2004). Second, we investigate about the main determinants of External Capital Flows (ECF) directed to Developing Countries. We put to a test the Gertler and Rogoff (1990) hypothesis that a “risky rate” arises in that markets because the economy has not sufficient amount of wealth to “collateralize” the capital she needs to borrow to take advantage of the investment opportunities she has and additionally because the lender does not have the chance of observing what the borrowed does with the funds (that is information asymmetry arises because the lender can check the realized output of investment but he can not observe if he really invest in the project or secretly lend abroad). Finally, Following Prasad, E. S., Rajan and R. Subramanian, A (2007) we measure the relationship between external capital flows and domestic currency overvaluation. We run a panel GMM estimation for a set of 18 Latin American Countries during the period 1973-2008.

Sujeto y Política. La constitución de las identidades desde una perspectiva postfundacionalista: hacia la construcción de un marco teórico-metodológico para el análisis histórico-político. Subject and politics. The constitution of political identities from a posfoundational perspective: towards a construction of a theorethico-methodolocal framework for histórico-political analysis.

El proyecto de investigación se dirige a sistematizar un abordaje postfundacionalista de las identidades políticas en vistas a la construcción de un marco teórico-metodológico para el análisis histórico-político. Se parte de la creciente relevancia en las ciencias sociales de la cuestión de la “identidad” para indagar la singularidad del marco teórico adoptado en su estudio. Así, el postfundacionalismo da cuenta de una teoría de las subjetividades políticas que parte de procesos de identificación que suponen una articulación singular entre relativa estructuralidad y agencia. El sujeto emerge en un contexto nunca plenamente suturado ni plenamente abierto, sino a través de un anudamiento de diversas dimensiones reales, simbólicas e imaginarias. Esta visión es altamente productiva para generar conclusiones relevantes en el campo de la ciencia política y del análisis histórico político comparado. This research project seeks to systematise from a postfundationalist view of political identities a theoretico-methodological framework for historico political analysis. The project starts from the increasing relevance of the quistion of 'identity' for contremporary social sciences. Poststructuralism provides an insight of processes of identification that supposes a singular articulation between relative structurality and agency. The subject emerges in a neither fully structured nor fully opened context but through a knotting process of different registers: real, symblic and imaginary. This vision, we believe, is highly productive to generate meaningful conclusions in the field of political science and comparative political analysis.

Análisis comparativo de la pérdida de tejido dentinario radicular en distintos procedimientos para el retiro de postes de fibra (in-vitro). Parte 2.

El retiro de postes del interior de un conducto, puede ser un obstáculo importante en el retratamiento endodóntico y conducir a menudo a la solución quirúrgica o extracción de la pieza por la dificultad del procedimiento, sin debilitar, perforar o fracturar la raíz, por este motivo, para la remoción de un postes el clínico debe pensar en riesgos y beneficios antes de comenzar a trabajar. En relación a la bibliografía consultada sobre retiro de postes del interior del conducto radicular, coincidimos con distintos autores, que si se accede a la cámara pulpar, se elimina todo el muñón coronario y se logra exponer el postes, existe una variedad de técnicas que podrían retirar el postes de manera exitosa y segura para las estructuras dentinarias remanentes. En el caso de los postes de fibra, motivo de nuestro estudio, la similitud de estos en cuanto a la densidad como el color con el tejido dentinario, dificulta la remoción del muñón coronario con la consecuente exposición de postes. Este proyecto, desea establecer pautas de proyección precisas, que el odontólogo general pueda poner en práctica.

Análisis sobre la adaptación, ajuste y su consecuente retención en postes intraradiculares pre-formados no metálicos y en postes post-formados metálicos. Estudio comparativo.

Uno de los objetivos concretos de los remanentes radiculares tratados endodonticamente, es de servir como elemento de anclaje para una futura restauración protética. Si bien, todo tratamiento con pernos trae aparejado un cierto grado de debilitamiento tisular, es vital que este tipo de prótesis adapten y ajusten correctamente, ya que de ellas depende la estabilidad y la permanencia de la consecuente corona en boca. Son muchas las causas que nos pueden llevar a la falta de ajuste y adaptación de nuestras restauraciones, pero la técnica elegida para la preparación de la cavidad radicular, además del momento y el material con el que esta hecho el poste son 2 items fundamentales, para estudiar esta problemática. Actualmente existe un interesante debate a cerca de las ventajas de uno u otro sistema, en general esa discusión se centra en el análisis de las propiedades de uno u otro sistema, por ejemplo su modulo de elasticidad, su radiopacidad, su resistencia a la fractura, a la fatiga, su ventaja estética, etc. Pero hay un detalle, que por lo menos para nosotros es vital, la retención. En cuanto al diseño metodológico elegido para llevar a cabo este trabajo, se utilizaran 40 porciones radiculares a las que se les practicarán (con el mismo instrumento) cavidades con la finalidad de albergar postes intraradiculares. A las primeras 20 (codificadas) se le tomarán impresiones sectorizadas siguiendo posteriormente el protocolo correspondiente para la confección de postes post formados metálicos (colados) por método indirecto (Método COPISMY), luego de ser obtenidos, estos postes colados serán cementados a presión controlada sobre sus respectivas porciones radiculares. A las segundas 20 porciones (codificadas) se le cementarán también a presión controlada, postes prefabricados no metálicos, siguiendo los mismos pasos que para los colados. Posteriormente todas las muestras serán incluidas en cubos de resina transparente con la finalidad de practicarles cortes transversales para su posterior observación, medición y captura de imagen. Luego todos los valores numéricos obtenidos, serán sometidos a un estricto estudio estadístico para tratar de determinar si existen entre ambos grupos diferencias que puedan ser consideradas estadísticamente significativas.

Análisis de componentes de la inmunidad innata en infecciones virales: implicancias en la patogénesis.

El estudio de células del sistema inmune innato en infecciones virales se ha centrado principalmente en las células dendríticas y las células NK. Los objetivos de este proyecto de investigación son evaluar el nivel de apoptosis de neutrófilos y las vías de activación de muerte celular en la infección por Virus de la Inmunodeficiencia Humana (VIH) y caracterizar la respuesta inmune inducida en monocitos/macrófagos infectados in vitro con el Encefalitis San Luis virus (ESLV). En individuos con infección por VIH se evaluará la apoptosis (anexina y citomorfología), la expresión de moléculas de adhesión y de receptor Toll-like (TLR) en neutrófilos. Además, se determinará la concentración sérica de citocinas pro-inflamatorias y anti-inflamatorias y de moléculas pro-apoptóticas y anti-apoptóticas. La infección por ESLV será realizada en una línea celular mieloide en la que se detectaran los antígenos virales a distintos días post-infección viral (inmunofluorescencia y citometría de flujo). Además, se determinará la expresión de antígenos de superficie y TLR. En sobrenadantes de cultivos de monocitos infectados con diferentes genotipos de ESLV a distintos días post-infección serán cuantificada la concentración de citocinas y determinada la apoptosis de monocito/macrófagos infectados (anexina y citomorfología). Este proyecto posibilitará una mayor comprensión de la regulación de la apoptosis en la infección por VIH, conocimiento que podrá ser de utilidad para avanzar en investigaciones futuras para el entendimiento de los mecanismos y la regulación de la apoptosis de componentes del sistema inmune innato. En la infección por ESLV el conocimiento de las características de la activación del macrófago cuando es infectado por este virus, los inmunomoduladores liberados y el impacto de la infección sobre la apoptosis de ésta célula podrían orientar hacia posibles blancos para el diseño futuro de estrategias terapéuticas o profilácticas contra esta infección.

Aplicación del análisis y prevención de falla al desarrollo regional de componentes mecánicos.

En el anterior período de dos años, se ha estudiado la aplicación del método científico al análisis de falla de componentes, como una etapa de formación y capacitación en el método utilizado para la investigación de roturas o fallas de piezas o sistemas mecánicos. Ante la tendencia al desarrollo local de componentes, reemplazo de importaciones, se evidencia que no siempre ésta acción se realiza verificando todos los aspectos del elemento a desarrollar. Tanto el diseño, la materia prima, el método de producción, deben ser analizados detalladamente por su influencia en el comportamiento de cada elemento. Particularmente, en la pequeña y mediana empresa, que no dispone de respaldo técnico suficiente para cubrir todos los aspectos de un desarrollo, existe la necesidad de recurrir a proveedores externos por asesoramiento. La experiencia acumulada en el Análisis de Falla, ofrece un enfoque crítico ante los diferentes factores intervinientes en un componente que permiten predecir, con buena aproximación, los puntos débiles que posee tanto un diseño como un método de producción y de esta forma, aportar al desarrollo exitoso del producto.

Tetraploidía en Ceratophrys (Anura, Leptodactylidae), análisis del registro fósil

It has been confirmed the existence of the tetraploid counterpart of the genus Ceratophrys Wied, 1824 (extint at the present time) in Argentina and Brazil since the Pliocene, and the apparition of the octaploidy in the Upper Pleistocene - Holocene. Fossil material of the diploid form, distinctive of the Chacoan District, has been reported from the horizons of the Montehermosense Formation in south-east of the province of Buenos Aires, Argentina. The coexistence of diploid-tetraploid and tetraploid-octaploid forms in the same province was documented.

Estructura de la comunidad de macroinvertebrados del arroyo Achiras (Córdoba, Argentina): análisis previo a la construcción de una presa

La regulación de ríos y arroyos mediante diques modifica parámetros que influyen directamente sobre la biota. En la cuenca endorreica Achiras-del Gato ha finalizado recientemente la construcción de una presa de mediana envergadura que alterará las características limnológicas del sistema y la estructura de las comunidades bentónicas. Este estudio aporta los primeros registros del macrobentos de este sistema lótico y analiza la variación espacio-temporal de la estructura de la comunidad en tramos pedemontanos del arroyo Achiras. Durante un año, antes de la construcción de la presa, se colectaron muestras de zoobentos y se registraron variables abióticas en correderas y rabiones de dos sitios del arroyo, uno situado río arriba del área del dique y otro aguas abajo de la misma. Para cada sitio, hábitat y estación del año se determinó abundancia, frecuencia, riqueza taxonómica, Índice de Shannon y equidad, y se analizaron mediante ANOVA de una y tres vías. Los atributos de las comunidades de referencia se complementaron con la determinación de taxa exclusivos e indicadores y detectores ecológicos. En el primer sitio se registraron 73 taxa, Simulium fue más abundante y Leptohyphes eximius Eaton, 1882, más frecuente. En el segundo se hallaron 75 taxa, Caenis fue más abundante y Cricotopus sp. 3 más frecuente. La abundancia y la riqueza fueron significativamente mayores en primavera, y la diversidad en rabiones de invierno. Se determinó que los atributos de la comunidad estuvieron afectados por la época de muestreo. El arroyo Achiras posee un régimen hídrico freático-pluvial, con caudales bajos en invierno y altos en verano, por lo que se esperan cambios en la biota nativa y la integridad del sistema en respuesta a la reducción de la variabilidad hidráulica cuando el funcionamiento de la presa altere el caudal natural.

Regulación de la distribución eléctrica en España: análisis económico de una década, 1987-1997

A principis dels anys 80 es va implementar a Espanya un sistema de regulació pel sector elèctric conegut com a Marco Legal Estable, que pretenia donar una solució a la situació de precarietat econòmica i financera per la que passava la indústria en aquests moments. Aquest marc legal es basava en un sitema multiproducte, en el que es retribuïa a les empreses no pels costos efectivaments 'incurridos', sino per uns costos estàndards calculats pel regulador d'igual manera per a totes les empreses. En aquest treball s'analitzan les conseqüències que va tenir l'aplicació d'aquest sistema de regulació en l'activitat de distribució elèctrica.

Aplicación del DEA en el análisis de beneficios en un sistema integrado verticalmente hacia adelante

En el presente trabajo se diseñan tres modelos DEA a partir de un sistema de producción cuyos componentes están colocados en un arreglo en serie que se integran verticalmente hacia adelante. El primer modelo busca optimizar los beneficios del sistema agregado, así como la mejora de los mismos en cada uno de los subsistemas. En el segundo de los modelos, además del objetivo anterior, se incluyen restricciones de transferencia de los recursos específicos asociados a cada subsistema, y en el tercer modelo se estima el intervalo de variación para los precios de transferencia de los inputs intermedios entre ambos subsistemas. Los modelos han sido programados y simulados en el software GAMS a partir de datos generados por una función de producción Cobb-Douglas para los inputs intermedios y los outputs finales.

Innovación tecnológica y resultado exportador: un análisis empírico aplicado al sector textil-confección español

En los últimos años, la relación entre tecnología y resultado exportador ha sido objeto de algunos estudios centrados en explicar la relación existente entre los distintos indicadores de las actividades tecnológicas y la performance internacional de las empresas. Sin embargo, la mayoría de las investigaciones centradas en este tema tienden a aproximar la estrategia innovadora de una empresa a partir de sus gastos en actividades de I+D cuando, en realidad, el concepto de innovación tecnológica podría resultar más amplio que la mera realización formal de actividades de I+D. En este trabajo en primer lugar se identifican aquellos factores que aproximan, de una forma más exhaustiva, las actividades de innovación tecnológica que realiza una empresa y, en segundo lugar, se averiguará su relación con el resultado exportador de la misma. Los resultados que se obtienen son satisfactorios ya que demuestran que la probabilidad y la intensidad exportadora de las empresas españolas del sector textil-confección dependen no sólo de sus inversiones en I+D, sino también de otras variables vinculadas a su estrategia innovadora.

Opción de responsabilidad limitada y opción de abandonar: una integración para el análisis del coste de capital

El objetivo de este documento es formalizar el valor de las acciones de una empresa endeudada, la responsabilidad limitada de los accionistas de una sociedad anónima y la rentabilidad exigida en un horizonte perpetuo, aplicando la teoría de opciones. El modelo que se elabora parte del establecido por Fisher Black y Myron Scholes en 1973 sobre el valor de las acciones de una empresa endeudada en un horizonte monoperiódico. En este modelo se encuentra un problema: la limitación del horizonte a un solo período. El modelo que se desarrolla en este documento, se basa en que el horizonte de la empresa es, en principio, ilimitado, y es frecuente que se mantenga un determinado grado de endeudamiento a lo largo de su vida. Es decir, se considera el endeudamiento de la empresa de horizonte perpetuo. Como consecuencia, los accionistas pueden declarar la quiebra en cualquier momento independientemente del vencimiento de la deuda, dejando la empresa en manos de los acreedores. Basándose en este modelo de horizonte perpetuo, se introduce la opción de abandonar. Se utiliza el valor de venta que tiene el activo de la empresa en el mercado, los accionistas lo comparan con el valor de las deudas, y deciden si es más rentable seguir con la empresa o vender los elementos del activo en el mercado. Para la valoración, se utiliza la fórmula deducida por Merton (1990) de la opción de venta americana perpetua. También se utiliza las opciones de barrera. Una vez valorada la responsabilidad limitada de los accionistas en un horizonte perpetuo, se puede calcular el interés efectivo en condiciones de riesgo.

Modelo para la idenfiticación de grupos estratégicos basado en el análisis envolvente de datos: aplicación al sector bancario español

Este trabajo explora la formación de grupos estratégicos en el Sector Bancario Español, a partir de una definición alternativa de grupo estratégico (GE). Un GE se define como un conjunto de empresas capaces de responder del mismo modo a perturbaciones. La capacidad de respuesta, o capacidad de adaptar la estrategia competitiva, se define a partir de las relaciones marginales (RM) entre las variables estratégicas (la pendiente de la frontera en un punto), y sirve de base para examinar la presencia de barreras a la movilidad. El Análisis Envolvente de Datos (DEA) es la herramienta utilizada para el cómputo de las RM, aunque su uso genera dos problemas que son solucionados en este trabajo; la multiplicidad de RM para las empresas situadas en la frontera (líderes estratégicos), y la imposibilidad de encontrar RM para las empresas situadas por debajo de la misma (seguidores estratégicos).