Registro:
| Documento: | Tesis de Grado |
| Disciplina: | computacion |
| Título: | Una nueva estructura de datos basada en BDDs para el model checking temporizada |
| Autor: | Pavese, Esteban José |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2024-08-30 |
| Fecha de defensa: | 2006 |
| Fecha en portada: | 2006 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Schapachnik, Fernando Pablo; Olivero, Alfredo |
| Idioma: | Español |
| Palabras clave: | SISTEMAS DE TIEMPO REAL; ARBOLES DE DECISION; VERIFICACION DE MODELOS |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000261_Pavese |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000261_Pavese.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000261_Pavese |
| Ubicación: | Dep.COM 000261 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Pavese, Esteban José. (2006). Una nueva estructura de datos basada en BDDs para el model checking temporizada. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000261_Pavese |
Resumen:
Los sistemas de tiempo real son por naturaleza críticos. Sus fallas pueden resultar en serias pérdidas, tanto materiales como también de vidas humanas. Además, en general están descriptos por la interacción de varios componentes y resulta muy difícil asegurar que determinadas propiedades (que representan de alguna manera requisitos o condiciones deseables del sistema) se cumplan. Hoy en día, existen herramientas denominadas model checkers (por ejemplo, UPPAAL, HyTech, KRONOS) utilizadas para expresar y verificar propiedades sobre este tipo de sistemas. Una de las propiedades más requerida es la de establecer si cierto conjunto de estados del sistema es o no alcanzable. Lamentablemente, esta verificación es costosa, y a veces prohibitiva, tanto en términos de tiempo como de memoria, debido al problema de la explosión combinatoria de estados. Por otra parte, recientemente se ha estudiado el uso de estructuras de decisión como posible alternativa a las representaciones clásicas utilizadas en la verificación, de forma de lograr reducir, en cierto grado, los efectos de tal explosión. En este trabajo se presenta una nueva estructura de datos, basada en arbóles de decisión, que apunta a reducir el tiempo y espacio requeridos para estas verificaciones. Además, se realiza una implementación de la misma, integrándola al model checker Zeus, y con ella se verifican algunos ejemplos de la literatura, obteniéndose resultados promisorios
Citación:
---------- APA ----------
Pavese, Esteban José. (2006). Una nueva estructura de datos basada en BDDs para el model checking temporizada. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000261_Pavese
---------- CHICAGO ----------
Pavese, Esteban José. "Una nueva estructura de datos basada en BDDs para el model checking temporizada". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2006.https://hdl.handle.net/20.500.12110/seminario_nCOM000261_Pavese
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000261_Pavese.pdf
Distrubución geográfica
