TERMINADA".
Matias Lee
"El que dice Agosto, dice Septiembre..."
Anónimo. :P
Autores: Matias Lee - Maximiliano Combina.
Clasificación: D.2.4 Software/Program Verification.
Palabras claves: Model Checking, Model Checking cuantitativo, teoría de autómatas, verificación formal, SSS Reducer, Rapture, ltl2dstar.
Version PDF: aquí.
Defensa del trabajo: Septiembre 2006.
Si necesitas una versión completa del trabajo desarrollado, comunicate via mail.
Matias Lee agradece a la Agencia Córdoba Ciencia el apoyo recibido a través del programa ConCiencia.
El estudio de la corrección de los sistemas es de suma importancia debido a que las
fallas en estos sistemas pueden tener consecuencias catastróficas.
Este trabajo contribuye a extender la técnica de Model Checking Cuantitativo
desarrollada por Luca De Alfaro en
[este paper],
el cual presenta un algoritmo para calcular
la probabilidad máxima de que una propiedad expresada en LTL sea satisfecha por
un sistema con componentes probabilísticas y/o no determinísticas.
Este algoritmo reduce el problema del cálculo de la probabilidad máxima
a un problema de alcanzabilidad.
Utilizando un enfoque similar, hemos desarrollado un algoritmo para el cálculo
de la probabilidad mínima.
Además, hemos creado una herranienta para el cálculo de dicha probabilidad
en un sistema bajo estudio. Esta herramienta se basa en la implementación
de nuestros resultados y la integración
de estos con otras aplicaciones ya existentes, entre ellas,
Rapture, un model checker de
probabilidad cuantitativa.