Hacia un enfoque híbrido del model checker Zeus

Mostrar todas las versiones(2)

Los sistemas de tiempo real son aquellos en los que existen restricciones de tiempo cuyo cumplimiento es esencial para su corrección. En general, están formados por varios componentes que interactúan entre sí y suelen llevar a cabo tareas críticas. El desarrollo de este tipo de sistemas es cada vez...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Taboada, Fernando Pablo
Otros Autores:	Schapachnik, Fernando Pablo
Formato:	Tesis de grado publishedVersion
Lenguaje:	Español
Publicado:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2007
Acceso en línea:	https://hdl.handle.net/20.500.12110/seminario_nCOM000752_Taboada https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000752_Taboada_oai
Aporte de:	Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires

id	I28-R145-seminario_nCOM000752_Taboada_oai
record_format	dspace
spelling	I28-R145-seminario_nCOM000752_Taboada_oai2025-08-20 Schapachnik, Fernando Pablo Taboada, Fernando Pablo 2007 Los sistemas de tiempo real son aquellos en los que existen restricciones de tiempo cuyo cumplimiento es esencial para su corrección. En general, están formados por varios componentes que interactúan entre sí y suelen llevar a cabo tareas críticas. El desarrollo de este tipo de sistemas es cada vez más creciente y lógicamente se requiere que tengan altos niveles de calidad. En este sentido, en las últimas dos décadas han surgido diferentes formalismos para representarlos, así como para describir propiedades sobre su comportamiento. Uno de los más exitosos ha sido el de los autómatas temporizados [AD94] , nacido como extensión a la teoría de autómatas, agregando la posibilidad de incorporar restricciones de tiempo. Los model checkers temporizados son programas que dada una especificación sobre un sistema de tiempo real y propiedades sobre este último, determinan de manera automática si éstas se cumplen o no. Esta verificación suele ser muy costosa en términos computacionales, tanto en tiempo como en espacio, lo que limita una adopción más amplia. Son ejemplos de model checkers temporizados UPP AAL [BLL95] y KRONOS [DOT96]. Es por este motivo que gran parte del desarrollo e investigación en esta área está focalizado en obtener herramientas que permitan manejar problemas de mayor tamaño de manera más eficiente. En los últimos años ha crecido el interés en desarrollar model checkers distribuidos o paralelos de manera de aumentar la escalabilidad de los mismos. En este trabajo partimos del model checker distribuido Zeus [SCH02] y proponemos un esquema híbrido (además de distribuido, paralelo) en donde se busca aprovechar la presencia de arquitecturas con más de un procesador con memoria compartida. Fil: Taboada, Fernando Pablo. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000752_Taboada spa Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar Hacia un enfoque híbrido del model checker Zeus info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000752_Taboada_oai
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-145
collection	Repositorio Digital de la Universidad de Buenos Aires (UBA)
language	Español
orig_language_str_mv	spa
description	Los sistemas de tiempo real son aquellos en los que existen restricciones de tiempo cuyo cumplimiento es esencial para su corrección. En general, están formados por varios componentes que interactúan entre sí y suelen llevar a cabo tareas críticas. El desarrollo de este tipo de sistemas es cada vez más creciente y lógicamente se requiere que tengan altos niveles de calidad. En este sentido, en las últimas dos décadas han surgido diferentes formalismos para representarlos, así como para describir propiedades sobre su comportamiento. Uno de los más exitosos ha sido el de los autómatas temporizados [AD94] , nacido como extensión a la teoría de autómatas, agregando la posibilidad de incorporar restricciones de tiempo. Los model checkers temporizados son programas que dada una especificación sobre un sistema de tiempo real y propiedades sobre este último, determinan de manera automática si éstas se cumplen o no. Esta verificación suele ser muy costosa en términos computacionales, tanto en tiempo como en espacio, lo que limita una adopción más amplia. Son ejemplos de model checkers temporizados UPP AAL [BLL95] y KRONOS [DOT96]. Es por este motivo que gran parte del desarrollo e investigación en esta área está focalizado en obtener herramientas que permitan manejar problemas de mayor tamaño de manera más eficiente. En los últimos años ha crecido el interés en desarrollar model checkers distribuidos o paralelos de manera de aumentar la escalabilidad de los mismos. En este trabajo partimos del model checker distribuido Zeus [SCH02] y proponemos un esquema híbrido (además de distribuido, paralelo) en donde se busca aprovechar la presencia de arquitecturas con más de un procesador con memoria compartida.
author2	Schapachnik, Fernando Pablo
author_facet	Schapachnik, Fernando Pablo Taboada, Fernando Pablo
format	Tesis de grado Tesis de grado publishedVersion
author	Taboada, Fernando Pablo
spellingShingle	Taboada, Fernando Pablo Hacia un enfoque híbrido del model checker Zeus
author_sort	Taboada, Fernando Pablo
title	Hacia un enfoque híbrido del model checker Zeus
title_short	Hacia un enfoque híbrido del model checker Zeus
title_full	Hacia un enfoque híbrido del model checker Zeus
title_fullStr	Hacia un enfoque híbrido del model checker Zeus
title_full_unstemmed	Hacia un enfoque híbrido del model checker Zeus
title_sort	hacia un enfoque híbrido del model checker zeus
publisher	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate	2007
url	https://hdl.handle.net/20.500.12110/seminario_nCOM000752_Taboada https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000752_Taboada_oai
work_keys_str_mv	AT taboadafernandopablo haciaunenfoquehibridodelmodelcheckerzeus
_version_	1843127025628348416

Hacia un enfoque híbrido del model checker Zeus

Ejemplares similares