Implementación de técnicas de derivación de contraejemplos en el model checker PRISM
Ver/Descargar
Fecha
2011-03-18Autor
Marenchino, Matías Leandro
Director/a
D'Argenio, Pedro Ruben
Metadatos
Mostrar el registro completo del ítemResumen
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 el presente trabajo se implementan nuevas técnicas para la generación de contraejemplos en PRISM. Estos métodos son útiles tanto para cadenas de Markov de tiempo discreto como para procesos de decisión de Markov. Inicialmente agrupamos
los contraejemplos en caminos finitos que contienen información similar a la hora de hacer debugging. Se implementa también una evolución de tal método, describiendo las componentes fuertemente conexas mediante expresiones regulares reducidas.