Titulo: “Model Checking Cuantitativo, con un enfoque de la teoría de autómatas”
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.