Implementación de técnicas de derivación de contraejemplos en el model checker PRISM
Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2011.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | bachelorThesis |
| Language: | spa |
| Published: |
2011
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/50 |
| _version_ | 1801215479365238784 |
|---|---|
| author | Marenchino, Matías Leandro |
| author2 | D'Argenio, Pedro Ruben |
| author_facet | D'Argenio, Pedro Ruben Marenchino, Matías Leandro |
| author_sort | Marenchino, Matías Leandro |
| collection | Repositorio Digital Universitario |
| description | Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2011. |
| format | bachelorThesis |
| id | rdu-unc.50 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2011 |
| record_format | dspace |
| spelling | rdu-unc.502022-10-13T11:34:24Z Implementación de técnicas de derivación de contraejemplos en el model checker PRISM Marenchino, Matías Leandro D'Argenio, Pedro Ruben Software Program Verification Model checking probabilista Contraejemplos Cadena de Markov de tiempo discreto Proceso de decisión de Markov Lógica LTL PRISM Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2011. 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. 2011-09-05T19:32:57Z 2011-09-05T19:32:57Z 2011-03-18 bachelorThesis http://hdl.handle.net/11086/50 spa Atribución-NoComercial-SinDerivadas 2.5 Argentina http://creativecommons.org/licenses/by-nc-nd/2.5/ar/ |
| spellingShingle | Software Program Verification Model checking probabilista Contraejemplos Cadena de Markov de tiempo discreto Proceso de decisión de Markov Lógica LTL PRISM Marenchino, Matías Leandro Implementación de técnicas de derivación de contraejemplos en el model checker PRISM |
| title | Implementación de técnicas de derivación de contraejemplos en el model checker PRISM |
| title_full | Implementación de técnicas de derivación de contraejemplos en el model checker PRISM |
| title_fullStr | Implementación de técnicas de derivación de contraejemplos en el model checker PRISM |
| title_full_unstemmed | Implementación de técnicas de derivación de contraejemplos en el model checker PRISM |
| title_short | Implementación de técnicas de derivación de contraejemplos en el model checker PRISM |
| title_sort | implementacion de tecnicas de derivacion de contraejemplos en el model checker prism |
| topic | Software Program Verification Model checking probabilista Contraejemplos Cadena de Markov de tiempo discreto Proceso de decisión de Markov Lógica LTL PRISM |
| url | http://hdl.handle.net/11086/50 |
| work_keys_str_mv | AT marenchinomatiasleandro implementaciondetecnicasdederivaciondecontraejemplosenelmodelcheckerprism |