Browsing Trabajos Especiales de Licenciatura en Ciencias de la Computación by Author "D'Argenio, Pedro Ruben"
Now showing items 1-14 of 14
-
Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM
Zandarin, Nicolás Hugo (2010-12-17)En este trabajo se presenta una adaptación al model checking simbólico de un método de reducción de estados, el cual, tiene como objetivo reducir el costo de los cálculos numéricos involucrados en el model checking ... -
Análisis multiobjetivo sobre DTNs
Torrella, Ulises Nicolás (2023-06-14)En este trabajo se aborda el desafío de la comunicación espacial e interplanetaria a través del uso de redes tolerantes a demoras (DTNs) con un enfoque basado en procesos de decisión de Markov (MDPs). Se emplea la verificación ... -
CLOUSEAU: verificación de propiedades de seguridad en protocolos distribuidos con probabilidades
Waquim, Pedro Eduardo (2014-03-20)Presentamos una herramienta para analizar propiedades de seguridad en protocolos distribuidos. La herramienta está construida sobre los schedulers llamados fuertemente distribuidos, donde el secreto también es considerado. ... -
Enrutamiento multiobjetivo en redes tolerantes a demoras
Martinez Picech, Benjamin Maximiliano (2024-04-26)Las redes tolerantes a demoras (DTN) han sido propuestas y estudiadas como un protocolo acorde al problema de la comunicación en redes que cambian a lo largo del tiempo. Un plan de contacto se construye a partir de la ... -
Falluto2.0 un model checker para la verificación automática de sistemas tolerantes a fallas
Monti, Raúl Enrique (2013-03)Los sistemas computacionales juegan roles determinantes en muchas áreas de nuestra vida cotidiana. En algunos casos la dependencia hacia estos sistemas es crítica, y el mal funcionamiento de los mismos puede acarrear grandes ... -
Implementación de técnicas de derivación de contraejemplos en el model checker PRISM
Marenchino, Matías Leandro (2011-03-18)El model checking es un método de verificación formal que permite verificar automáticamente si un modelo cumple una especificación. PRISM constituye una herramienta para realizar model checking de tipo probabilista. En ... -
Juegos estocásticos con objetivo compuesto: recompensas totales sujetas a alcanzabilidad prioritaria
Feltes, Joaquín Ignacio (2024-05-10)El propósito de este trabajo es estudiar juegos estocásticos de dos jugadores con multiobjetivo. Uno de los objetivos es de alcanzabilidad de un conjunto de estados considerados exitosos y el otro es de recompensa total ... -
OFFBEAT : una extensión de PRISM para el análisis de sistemas temporizados tolerantes a fallas
Bordenabe, Nicolas Emilio (2011-03-28)Los sistemas tolerantes a fallas son aquellos que son capaces de seguir operando luego de la ocurrencia de una o más fallas. Una falla puede provocar cambios no deseados en el estado interno del sistema, y para que el ... -
Reducción de orden parcial en model checking probabilista simbólico
Ferrer Fioriti, Luis María (2010)El problema fundamental de los model checkers es la explosión exponencial del espacio de estados que se produce al agregar nuevas componentes o variables. El problema se exacerba en los model checkers probabilistas dado ... -
Simulación de eventos raros con Importance Splitting, extendiendo FIG con Fixed Effort y Fixed Sucess
Hunicken Berardo, Matías José (2018-12-03)Un problema que surge al hacer simulación para validar sistemas críticos es cuando el evento a analizar exhibe una probabilidad muy baja. En este trabajo nos enfocamos en la técnica de Importance splitting (división por ... -
TEO : una herramienta para la optimización de la probabilidad de ejecución de casos de prueba en tiempo real
Miretti, Gabriel Leonardo (2010)En las pruebas de sistemas de tiempo real, y en particular los que tienen comportamiento estocástico, es muy importante que éstas se ejecuten con la mayor probabilidad posible. El objetivo de este trabajo final es implementar ... -
Verificación en tiempo de ejecución con Streams
Romero, Santiago Gabriel (2010)La verificación en tiempo de ejecución es una de las técnicas utilizadas con el objetivo de garantizar la corrección, seguridad y confiabilidad de los sistemas de software que ha recibido gran atención en los últimos años. ... -
Verificación formal de código binario
Arch, David Daniel (2015)Los buffer overflow son una de las vulnerabilidades mas frecuentes que se encuentran en el software que utilizamos diariamente. El análisis de este tipo de vulnerabilidades se hace tedioso y complejo cuando solo se tiene ... -
Verificación formal de protocolos distribuidos
Naser Pastoriza, Alejandro José (2019)En esta tesis probamos la correctitud de tres protocolos distribuidos. Primero, el algoritmo Single Decree Paxos que resuelve el problema de llegar a un acuerdo, o alcanzar consenso, entre un conjunto de procesos. Segundo, ...