Catálogo de publicaciones

Compartir en
redes sociales


Navegación

Tipo

Acceso

Plataformas

Temática

Mostrando 10 de 20.620 registro(s)

Filtros temática quitar todos

tesis Acceso Abierto
Agregar a Mi catálogo

Verificación de autómatas temporizados en arquitecturas monoprocesador y multiprocesador

Más información
Autores/as: Fernando Schapachnik ; Víctor Braberman ; Alfredo Olivero

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No requiere 2007 Biblioteca Digital (FCEN-UBA) (SNRD) acceso abierto

Cobertura temática: Ciencias de la computación e información  

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.

Verification of Object-Oriented Software. The KeY Approach: Foreword by K. Rustan M. Leino

Más información

ISBNs: 978-3-540-68977-5 (impreso) 978-3-540-69061-0 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2007 SpringerLink

Cobertura temática: Ciencias de la computación e información - Ingeniería eléctrica, electrónica e informática - Lenguas y literatura  


Verification, Model Checking, and Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings

Más información

ISBNs: 978-3-540-24297-0 (impreso) 978-3-540-30579-8 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2005 SpringerLink

Cobertura temática: Ciencias de la computación e información  


Verification, Model Checking, and Abstract Interpretation: Third International Workshop, VMCAI 2002 Venice, Italy, January 21-22, 2002 Revised Papers

Más información

ISBNs: 978-3-540-43631-7 (impreso) 978-3-540-47813-3 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2006 SpringerLink

Cobertura temática: Ciencias de la computación e información - Ingeniería eléctrica, electrónica e informática - Medicina básica  


Verification, Model Checking, and Abstract Interpretation: 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings

Más información

ISBNs: 978-3-540-31139-3 (impreso) 978-3-540-31622-0 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2006 SpringerLink

Cobertura temática: Ciencias de la computación e información - Ciencias físicas - Ingeniería eléctrica, electrónica e informática  


Verification, Model Checking, and Abstract Interpretation: 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007. Proceedings

Más información

ISBNs: 978-3-540-69735-0 (impreso) 978-3-540-69738-1 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2007 SpringerLink

Cobertura temática: Ciencias de la computación e información - Medicina clínica  


Verified Functional Programming in Agda

Más información

ISBNs: 978-1-970001-27-3 (impreso)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2016 ACM Digital Library

Cobertura temática: Ciencias de la computación e información - Ingeniería eléctrica, electrónica e informática  


revistas Acceso Abierto
Agregar a Mi catálogo

Vestnik Samarskogo Gosudarstvennogo Tehničeskogo Universiteta. Seriâ Fiziko-Matematičeskie Nauki

Más información

ISSNs 1991-8615 (impreso) 2310-7081 (en línea)

Disponibilidad
Institución detectada Período Navegá Descargá Solicitá
No requiere desde dic. 2024 / hasta dic. 2024 Directory of Open Access Journals acceso abierto

Cobertura temática: Matemáticas - Ciencias de la computación e información - Ciencias físicas - Ingeniería de los materiales  


libros Acceso Abierto
Agregar a Mi catálogo

Vetores da doença de Chagas no Brasil

Más información

ISBNs: 9788598203096 (impreso)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No requiere 2014 Directory of Open access Books acceso abierto

Cobertura temática: Ciencias de la computación e información - Ciencias de la salud  


tesis Acceso Abierto
Agregar a Mi catálogo

Viabilidad y estimación de proyectos de explotación de información

Más información
Autores/as: Pablo Pytel ; Ramón García Martínez ; Paola Verónica Britos ; Alejandro Hossian

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No requiere 2014 SEDICI: Repositorio Institucional de la UNLP (SNRD) acceso abierto

Cobertura temática: Ciencias de la computación e información  

Los proyectos de Explotación de Información son un tipo especial de proyecto de Ingeniería en Software que poseen problemas similares al existir cuestiones de gestión que pueden provocar su fracaso. Entre estas cuestiones se destaca la necesidad de establecer si es posible realizar el proyecto, si la solución es la correcta y si es posible cumplir con todas las metas y expectativas del proyecto; así como la cantidad de personas que van a participar en el equipo de trabajo durante el desarrollo del proyecto, y por cuanto tiempo. En este contexto, el presente trabajo de tesis tiene como objetivo proponer, estudiar y validar dos modelos a ser utilizados al inicio de un proyecto de Explotación de Información en el ámbito de las Pequeñas y Medianas Empresas. El primer modelo permite realizar la Evaluación de la Viabilidad del proyecto, mientras que el segundo modelo tiene como objetivo realizar la Estimación del Esfuerzo (medido en cantidad de personas por tiempo) que se requiere para llevar a cabo el proyecto de manera completa.