Reducción de subárboles repetidos en eCDDs para el model checking temporizado

Pérez, Gervasio Daniel

Navegar

Documento Últimos publicados Autor Año Título Obtenido - Año Departamento - Año Director y Director Asistente Jurado Consejero de Estudios Palabras Clave

Colección

Datos Estadísticas

Tesis de Grado

Pérez, Gervasio Daniel. "Reducción de subárboles repetidos en eCDDs para el model checking temporizado" . (2009). Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.

Registro Resumen Citación Estadísticas

Registro:

Documento:	Tesis de Grado
Disciplina:	computacion
Título:	Reducción de subárboles repetidos en eCDDs para el model checking temporizado
Autor:	Pérez, Gervasio Daniel
Editor:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Publicación en la web:	2022-07-05
Fecha de defensa:	2009-06-10
Fecha en portada:	2009-06-06
Grado Obtenido:	Grado
Título Obtenido:	Licenciado en Ciencias de la Computación
Director:	Schapachnik, Fernando Pablo; Pavese, Esteban José
Idioma:	Español
Formato:	PDF
Handle:	http://hdl.handle.net/20.500.12110/seminario_nCOM000359_Perez
PDF:	https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000359_Perez.pdf
Registro:	https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000359_Perez
Ubicación:	Dep.COM 000359
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. Pérez, Gervasio Daniel. (2009). Reducción de subárboles repetidos en eCDDs para el model checking temporizado. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000359_Perez

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 desde un estado inicial determinado. Esta verificación es costosa, y a veces prohibitiva, en términos de tiempo y memoria, debido al problema de la explosion combinatoria de estados. 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 explosion. En este trabajo se estudia la presencia de redundancia interna en una estructura de datos presentada en [Pav06], basada en árboles de decisión. Primero cuantificamos dicha redundancia y luego implementamos un método para hacer aliasing de las partes repetidas de la estructura, efectivamente reduciendo el espacio consumido.

Citación:

---------- APA ----------

Pérez, Gervasio Daniel. (2009). Reducción de subárboles repetidos en eCDDs para el model checking temporizado. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000359_Perez

---------- CHICAGO ----------

Pérez, Gervasio Daniel. "Reducción de subárboles repetidos en eCDDs para el model checking temporizado". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2009.https://hdl.handle.net/20.500.12110/seminario_nCOM000359_Perez

Estadísticas:

Descargas mensuales

Total de descargas desde :

https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000359_Perez.pdf