Browsing by Author "D'Argenio, Pedro Ruben"
Now showing items 1-18 of 18
-
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 ... -
Automatización de técnicas de división por importancia para la simulación de eventos raros
Budde, Carlos Esteban (2017-05)Existen muchas técnicas para estudiar y verificar descripciones formales de sistemas probabilistas. La simulación de Monte Carlo por eventos discretos ofrece una alternativa para la generalidad de procesos estocásticos ... -
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 ... -
MaskD : a tool for measuring masking fault-tolerance
Putruele, Luciano; Demasi, Ramiro Adrián; Castro, Pablo Francisco; D'Argenio, Pedro Ruben (2022-03-30)We present MaskD, an automated tool designed to measure the level of fault-tolerance provided by software components. The tool focuses on measuring masking fault-tolerance, that is, the kind of fault-tolerance that allows ... -
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 ... -
Playing against fair adversaries in stochastic games with total rewards
Castro, Pablo Francisco; D'Argenio, Pedro Ruben; Demasi, Ramiro Adrián; Putruele, Luciano (2022)We investigate zero-sum turn-based two-player stochastic games in which the objective of one player is to maximize the amount of rewards obtained during a play, while the other aims at minimizing it. We focus on games in ... -
Rare event simulation with fully automated Importance splitting
Budde, Carlos Esteban; D'Argenio, Pedro Ruben; Hermanns, Holger (2015)Probabilistic model checking is a powerful tool for analysing probabilistic systems but it can only be efficiently applied to Markov models. Monte Carlo simulation provides an alternative for the generality of stochastic ... -
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 ... -
Smart sampling for lightweight verification of Markov decision processes
D'Argenio, Pedro Ruben; Legay, Axel; Sedwards, Sean; Traonouez, Louis-Marie (2015)Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent ... -
Sobre la verificación automática de autómatas probabilistas distribuidos con información parcial
Giro, Sergio Sebastián (2010-03)En esta tesis desarrollamos algoritmos y técnicas de análisis basadas en model checking para analizar la corrección de sistemas distribuidos con características aleatorias y no deterministas. Una contribución importante ... -
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 ... -
A theory for the semantics of stochastic and non-deterministic continuous systems
Budde, Carlos Esteban; D'Argenio, Pedro Ruben; Sánchez Terraf, Pedro Octavio; Wolovick, Nicolás (2014)The description of complex systems involving physical or biological components usually requires to model complex continuous behavior induced by variables such as time, distance, speed, temperature, alkalinity of a solution, ... -
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, ...