Catálogo de publicaciones

Los sistemas de tiempo real están presentes en dispositivos embebidos, teléfonos celulares, controladores de vuelo, etc. Su complejidad es cada vez mayor, y cada vez cumplen funciones más críticas, donde las consecuencias de sus fallas son cada vez más graves. Por estos motivos tiene sentido realizar un análisis riguroso sobre ellos, que permita asegurar que sus diseños cumplen ciertas propiedades deseables. A este tipo de análisis se le suele llamar verificación automática o model checking. Un formalismo muy difundido para realizar esta tarea es el de los autómatas temporizados, una extensión de la teoría clásica de autómatas que permite trabajar con tiempo denso. Si bien las técnicas basadas en este tipo de autómatas se conocen desde hace un par de décadas, sufren aún de problemas de escalabilidad, lo que dificulta una utilización mayor en casos reales. Esta tesis analiza diversos mecanismos para acelerar la verificación de autómatas temporizados, tanto en el (clásico) ambiente monoprocesador, como así también en arquitecturas distribuidas. Durante el transcurso de la misma se construyó el model checker Zeus, que se utiliza para la experimentación. Luego de presentar la motivación e introducción al tema, se presentan los conceptos básicos del formalismo y las estructuras de datos más utilizadas en este tipo de herramientas. Se destacan los dos algoritmos tradicionales de verificación, forward y backwards. A continuación, se explora la paralelización del algoritmo backwards: se presenta una prueba de corrección de una versión distribuida y asincrónica del mismo, se la implementa, y se experimenta también con una versión sincrónica y con otra que reparte la carga de trabajo sobre los procesadores de manera dinámica. Se analizan los resultados obtenidos y se argumenta que son cercanos a óptimos utilizando la unidad de distribución de trabajo actual: la asignación de nodos del autómata a procesadores. Luego se aborda la paralización del algoritmo forward junto con una estrategia para la redistribución dinámica de trabajo entre los procesadores. Después de demostrar su corrección, se analizan varios casos de estudio sobre distintas configuraciones, obteniéndose resultados positivos pero no óptimos, y comprobándose que aún queda mucho por investigar con respecto a la distribución de este algoritmo, y planteándose varias posibles líneas de investigación. En el capítulo siguiente se compara el presente trabajo con otros del área, y se argumenta que ciertos resultados positivos obtenidos por otros investigadores tienen como causa no la paralización en sí sino ciertos efectos colaterales de la misma, que tal vez podrían reproducirse en un monoprocesador. A continuación se presenta trabajo realizado en pos de obtener una nueva estructura de datos. En ese marco, se introducen los rCDDs (restricted Clock Difference Diagrams) junto con casos de estudio en los que estos mejoran los tiempos de ejecución hasta en un treinta por ciento. El siguiente capitulo explora dos optimizaciones también validas para el caso monoprocesador. La primera consiste en computar rangos posibles para los valores de las estructuras de datos y de esa manera reacomodarlas para detectar antes ciertas condiciones de corte de operaciones utilizadas con mucha frecuencia. Los resultados muestran mejoras de hasta un diecisiete por ciento en los tiempos de ejecución. La segunda consiste en computar una aproximación al hipervolumen de los poliedros representados por las estructuras de datos, de manera tal de evitar O(n2) comparaciones al costo de O(1). Esta técnica logra una reducción de tiempo de hasta casi un veinte por ciento. El anteúltimo capítulo presenta VInTiMe, una herramienta gráfica que permite describir diseños de tiempo real, especificar sus propiedades de manera amigable, y verificarlas utilizando el model checker distribuido Zeus, de manera sencilla. Constituye un esfuerzo por acercar los métodos formales al usuario no tan experimentado. Finalmente, se exponen las conclusiones del trabajo, donde se argumenta la dificultad de decidir de antemano qué optimizaciones y/o parámetros serán más convenientes para un caso de estudio dado, y se proponen ideas alternativas para atacar el problema.

La Ley de Concursos y Quiebras establece un mecanismo de reconocimiento de los créditos denominado proceso de verificación, el cual tiene como propósito comprobar la existencia y monto de los créditos, como así también determinar si los mismos son quirografarios o privilegiados. El objetivo del presente trabajo es analizar particularidades de la verificación de los créditos correspondientes al Fisco, ya sea a nivel nacional, provincial y municipal. Asimismo se incluye doctrina y jurisprudencia relacionada con distintos aspectos que hacen del Fisco uno de los principales acreedores en los procesos concursales: su carácter de sujeto de derecho público y la posesión o no de prerrogativas especiales en el proceso de verificación; su presencia en la casi totalidad de los procesos concursales; la existencia de leyes con disposiciones contrapuestas a la norma concursal; la relevancia del Fisco en el conjunto de los acreedores y su papel a la hora de la obtención por parte del deudor de las mayorías necesarias para lograr el acuerdo; entre otros.

La verificación acotada de software usando SAT consiste en la traducción del programa junto con las anotaciones provistas por el usuario a una fórmula proposicional. Luego de lo cual la fórmula es analizada en busca de violaciones a la especificación usando un SAT-solver. Si una violación es encontrada, una traza de ejecución exponiendo el error es exhibida al usuario. Alloy es un lenguaje formal relacional que nos permite automáticamente analizar especificiaciones buscando contraejemplos de aserciones con la ayuda de un SAT-solver off-the-shelf. Las contribuciones de la presente tesis son principalmente dos. Por un lado, se presenta una traducción desde software anotado en lenguaje JML al lenguaje Alloy. Para conseguir esto, se presenta: • DynAlloy, una extensión al lenguaje de especificación Alloy para describir propiedades dinámicas de los sistemas usando acciones. Extendemos la sintaxis de Alloy con una notación para escribir aserciones de correctitud parcial. La semántica de estas aserciones es una adaptación del precondición liberal más débil de Dijsktra. • DynJML, un lenguaje de especificación orientado a objetos que sirve de representación intermedia para facilitar la traducción de JML a DynAlloy. • TACO, un prototipo que implementa la traducción de JML a DynAlloy. En segundo lugar, introducimos una técnica novedosa, general y complementamente automatizable para analizar programas Java secuenciales anotados con JML usando SAT. Esta técnica es especialmente beneficiosa cuando el programa opera con estructuras de datos complejas. Para esto, se instrumenta el modelo Alloy con un predicado de ruptura de simetrías que nos permite el cómputo paralelo y automatizado de cotas ajustadas para los campos Java.

La finalidad del tema elegido, pretende plasmar en estas páginas, una síntesis de las distintas particularidades que presenta el incidente de verificación tardía. En primer término se efectuará una descripción del proceso concursal desde sus orígenes, planteando las distintas alternativas que presenta y sus aspectos generales. Se desarrollarán con amplitud algunos conceptos de las situaciones particulares que hacen al incidente, planteando las posturas doctrinarias y de jurisprudencia más relevantes. En segundo término, se abordarán cuestiones específicas que hacen al rol del síndico y su incidencia frente al proceso. A continuación se desarrollará el tema de la imposición de costas, señalando el encuadre que la Ley de Concursos y Quiebras le da a la misma. En todos los temas analizados, se seguirá una metodología de desarrollo uniforme, presentando en primer lugar el marco legal, para efectuar luego su comparación con expresiones doctrinarias y jurisprudenciales.

Las colaboraciones inter-organizacionales permiten nuevas formas de gestión basadas en la cooperación. Los sistemas de información que brindan soporte a la gestión de estas acciones de colaboración requieren definir modelos y especificaciones de procesos de negocio colaborativos (PNCs) que representan el comportamiento explícito de la colaboración. En base a técnicas formales y a los conceptos del desarrollo dirigido por modelos, en esta tesis se proponen métodos y herramientas que permiten determinar el correcto comportamiento de los modelos de PNCs y, a partir de dichos modelos, generar especificaciones de PNCs cuyo comportamiento está alineado con el de los modelos. Se propone el lenguaje formal Redes de Interacción Global (GI-Nets) y un método de transformación para definir modelos formales de PNCs con GI-Nets a partir de modelos conceptuales de PNCs. Se definen dos métodos de verificación que permiten determinar si un modelo de PNC satisface un conjunto de propiedades que determinan su correcto comportamiento. El primer método, basado en GI-Nets, propone la propiedad de Solidez de Interacción Global de una GI-Net como principal criterio de verificación. Este método permite detectar el lugar específico donde existe un bloqueo en un modelo de PNC. El segundo método, basado en anti-patrones de comportamiento, provee un enfoque para especificar en forma sistemática los anti-patrones de cualquier lenguaje de PNCs. Este método detecta el lugar de un bloqueo y determina el conjunto de elementos que lo produce. Ambos métodos pueden ser utilizados con cualquier lenguaje de PNCs y dan soporte a la verificación de PNCs con constructores complejos. Se define un método formal de transformación de modelos que permite generar en forma automática una especificación de PNC cuyo comportamiento esté alineado con el definido en el modelo conceptual del PNC a partir del cual fue generada. Esto implica que el comportamiento de la especificación será correcto si el comportamiento del modelo del PNC es correcto, y viceversa. El método se utiliza para generar especificaciones de PNCs basadas en tecnologías de servicios Web a partir de modelos conceptuales de PNCs. Finalmente, se presentan las herramientas desarrolladas para la formalización, verificación y transformación de modelos y especificaciones de PNCs, y se utilizan las mismas para evaluar y validar los métodos propuestos en la tesis.

VERTMAIN es un emprendimiento para la fabricación y comercialización de vasos descartables innovadores, construidos en papel con film de bio-plástico, 100% biodegradable y compostable, que luego de su uso pueden ser depositados en composteras hogareñas para su procesamiento. Luego de 8 a 12 semanas, se transforma en humus que puede ser utilizado como fertilizante y abono. Este producto surge de la necesidad de dar respuesta a la problemática del residuo plástico, la contaminación por su bajo reciclaje y separación, comprometen los recursos naturales y a las próximas generaciones. Actualmente este tipo de tecnología no se ofrece en la Argentina. Los principales países del mundo ya están aplicándola. Consideramos que hay un potencial de crecimiento por reemplazo tecnológico hacia nuevos materiales eco-friendly, el cual a su vez estará forzado, no sólo por estrategias de compañías sustentables, sino también por los consumidores más conscientes, que elegirán consumir productos de compañías que los adopten. A esto se suma, que los gobiernos comienzan a prohibir paulatinamente el uso de plástico en los productos desechables. Actualmente están en tratamiento en Argentina distintas iniciativas al respecto, que desarrollaremos en el presente trabajo. Ofreceremos dos líneas de productos para bebidas frías y calientes. Nuestro mercado son los vasos descartables, en especial vasos de polipapel, en el cual estimamos un nicho de mercado B2B que estaría dispuesto a pagar un costo extra de 19% y 30% según línea de producto. Principalmente nos orientamos a organizaciones con políticas sustentables, certificadas en el medio ambiente, y que quieran formar parte de la comunidad que busca una economía circular, reduciendo los desechos, transformándolos en nuevos recursos. Estimamos ingresos por ventas al quinto año en us$ 5 millones. Nuestra estrategia de crecimiento será Lean StartUp (Blank, 2013), iniciando con productos certificados importados, y luego según los resultados fabricaremos localmente con una inversión inicial de us$ 91.000. Priorizaremos el aprendizaje, realizar múltiples interacciones para consolidar un modelo de negocio exitoso, cuyo ROIC será de 25% promedio en los primeros dos años, creciendo a un 43% interanual, y recuperando la inversión en dos años y medio.

VERTMAIN es un emprendimiento para la fabricación y comercialización de vasos descartables innovadores, construidos en papel con film de bio-plástico, 100% biodegradable y compostable, que luego de su uso pueden ser depositados en composteras hogareñas para su procesamiento. Luego de 8 a 12 semanas, se transforma en humus que puede ser utilizado como fertilizante y abono. Este producto surge de la necesidad de dar respuesta a la problemática del residuo plástico, la contaminación por su bajo reciclaje y separación, comprometen los recursos naturales y a las próximas generaciones. Actualmente este tipo de tecnología no se ofrece en la Argentina. Los principales países del mundo ya están aplicándola. Consideramos que hay un potencial de crecimiento por reemplazo tecnológico hacia nuevos materiales eco-friendly, el cual a su vez estará forzado, no sólo por estrategias de compañías sustentables, sino también por los consumidores más conscientes, que elegirán consumir productos de compañías que los adopten. A esto se suma, que los gobiernos comienzan a prohibir paulatinamente el uso de plástico en los productos desechables. Actualmente están en tratamiento en Argentina distintas iniciativas al respecto, que desarrollaremos en el presente trabajo. Ofreceremos dos líneas de productos para bebidas frías y calientes. Nuestro mercado son los vasos descartables, en especial vasos de polipapel, en el cual estimamos un nicho de mercado B2B que estaría dispuesto a pagar un costo extra de 19% y 30% según línea de producto. Principalmente nos orientamos a organizaciones con políticas sustentables, certificadas en el medio ambiente, y que quieran formar parte de la comunidad que busca una economía circular, reduciendo los desechos, transformándolos en nuevos recursos. Estimamos ingresos por ventas al quinto año en us$ 5 millones. Nuestra estrategia de crecimiento será Lean StartUp (Blank, 2013), iniciando con productos certificados importados, y luego según los resultados fabricaremos localmente con una inversión inicial de us$ 91.000. Priorizaremos el aprendizaje, realizar múltiples interacciones para consolidar un modelo de negocio exitoso, cuyo ROIC será de 25% promedio en los primeros dos años, creciendo a un 43% interanual, y recuperando la inversión en dos años y medio.

Tesis (Doctora en Ciencias Químicas) - - Universidad Nacional de Córdoba. Facultad de Ciencias Químicas, 2020

Se parte del caso de Fashion Revolution para indagar (nuevas) formas de interacción y maneras de encontrarnos habilitadas por Internet. Ahondamos el vínculo Comunicación/Digitalidad/Cultura, reconociendo que analizar los procesos que lo implican es la manera estratégica que tenemos para reflexionar sobre la actual circulación de sentidos; Se retoman así particularidades del contexto porque la comprensión de las (nuevas) maneras de vincularnos no puede darse sin el reconocimiento del momento histórico en que se desarrollan. Indagar las posibilidades que brinda la cotidianidad nos permitió pensar en los diseños de las prácticas de reunión y organización contemporáneas que, trabajando en un escenario que no discierne lo online de lo offline, ofrecen formas para acción colectiva en pos de una transformación. De esta manera, Fashion Revolution se volvió un objeto de investigación rico. En su propuesta de transformación, que hemos descrito como inserta en una matriz neoliberal, encontramos vestigios de posibles modificaciones que nos permiten depositar esperanza en la intención de un trabajo colectivo cuyo discurso logra pararse en el lugar de los/as otros/as y cuya interpelación se hace desde el reconocimiento de los/las sujetos como actores y actrices claves en los procesos transformadores. Allí la digitalidad se erige como habilitador de posibilidades. Sin embargo, la esperanza depositada en el proceso se desvanece en el análisis de las prácticas locales, debido a un reconocimiento de una tensión global-local que responde al contexto de inserción. El recorrido transitado profundiza las dinámicas de la comunicación digital desde lugares complejos, historizándolas y reconociendo sus lógicas; asumiendo finalmente que no hay más limitaciones que las que imponemos desde nuestra cultura.

Tesis (Doctor en Ciencia Químicas) - - Universidad Nacional de Córdoba, 2009.