Una nueva estructura de datos basada en BDDs para el model checking temporizada

Mostrar todas las versiones(2)

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 repres...

Descripción completa

Detalles Bibliográficos
Autor principal: Pavese, Esteban José
Otros Autores: Schapachnik, Fernando Pablo
Formato: Tesis de grado publishedVersion
Lenguaje:Español
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2006
Materias:
SISTEMAS DE TIEMPO REAL
ARBOLES DE DECISION
VERIFICACION DE MODELOS
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000261_Pavese
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id seminario:seminario_nCOM000261_Pavese
record_format dspace
spelling seminario:seminario_nCOM000261_Pavese2025-05-09T18:44:55Z Una nueva estructura de datos basada en BDDs para el model checking temporizada Pavese, Esteban José Schapachnik, Fernando Pablo Olivero, Alfredo SISTEMAS DE TIEMPO REAL ARBOLES DE DECISION VERIFICACION DE MODELOS 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 Fil: Pavese, Esteban José. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2006 info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion application/pdf spa info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000261_Pavese
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Español
orig_language_str_mv spa
topic SISTEMAS DE TIEMPO REAL
ARBOLES DE DECISION
VERIFICACION DE MODELOS
spellingShingle SISTEMAS DE TIEMPO REAL
ARBOLES DE DECISION
VERIFICACION DE MODELOS
Pavese, Esteban José
Una nueva estructura de datos basada en BDDs para el model checking temporizada
topic_facet SISTEMAS DE TIEMPO REAL
ARBOLES DE DECISION
VERIFICACION DE MODELOS
description 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
author2 Schapachnik, Fernando Pablo
author_facet Schapachnik, Fernando Pablo
Pavese, Esteban José
format Tesis de grado
Tesis de grado
publishedVersion
author Pavese, Esteban José
author_sort Pavese, Esteban José
title Una nueva estructura de datos basada en BDDs para el model checking temporizada
title_short Una nueva estructura de datos basada en BDDs para el model checking temporizada
title_full Una nueva estructura de datos basada en BDDs para el model checking temporizada
title_fullStr Una nueva estructura de datos basada en BDDs para el model checking temporizada
title_full_unstemmed Una nueva estructura de datos basada en BDDs para el model checking temporizada
title_sort una nueva estructura de datos basada en bdds para el model checking temporizada
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2006
url https://hdl.handle.net/20.500.12110/seminario_nCOM000261_Pavese
work_keys_str_mv AT paveseestebanjose unanuevaestructuradedatosbasadaenbddsparaelmodelcheckingtemporizada
_version_ 1831983591922335744

Ejemplares similares