Imagen de cubierta local
Imagen de cubierta local
Imagen de Google Jackets

Implementación de técnicas de derivación de contraejemplos en el model checker PRISM / Matías L. Marenchino.

Por: Colaborador(es): Detalles de publicación: [S.l. : s.n. ], 2011.Descripción: vi, 63 h. : il. (algunas col.) ; 30 cmTema(s): Recursos en línea: Disponible en líneaNota de disertación: Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2011. Resumen: 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.
Etiquetas de esta biblioteca: No hay etiquetas de esta biblioteca para este título.
Existencias
Tipo de ítem Biblioteca actual Signatura Copia número Estado Notas Fecha de vencimiento Código de barras Reserva de ítems
Trabajo Especial de Grado Trabajo Especial de Grado FaMAF Secc. Tesis y Trabajos especiales Trabajo Especial Computación CAJA 11 - 20841 1 Disponible Disponible también en línea 20841
Total de reservas: 0

Incluye índice de figuras y de tablas.

Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2011.

Incluye referencias bibliográficas: h. 61-63.

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.

Disponible en línea

cc Bajo una Licencia Creative Commons Atribución-NoComercial-SinDerivadas 2.5 Argentina CC BY-NC-ND

https://creativecommons.org/licenses/by-nc-nd/2.5/ar/

Haga clic en una imagen para verla en el visor de imágenes

Imagen de cubierta local


Nuestras Redes Sociales

facebook Instagram

Horario de la Biblioteca: lunes a viernes de 8:30 a 18:30hs

Av. Medina Allende s/n , Ciudad Universitaria, Córdoba, Argentina

Tel: +54 351 5353701 int. 41127 (Atención al Público) int. 41151 (Dirección)

biblio@famaf.unc.edu.ar (Dirección)

publicofamaf@gmail.com (Atención al público)