Resumen:
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.
Citación:
---------- APA ----------
Taboada, Fernando Pablo. (2007). Hacia un enfoque híbrido del model checker Zeus. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000752_Taboada
---------- CHICAGO ----------
Taboada, Fernando Pablo. "Hacia un enfoque híbrido del model checker Zeus". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2007.https://hdl.handle.net/20.500.12110/seminario_nCOM000752_Taboada
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000752_Taboada.pdf
Distrubución geográfica
