Registro:
| Documento: | Tesis de Grado |
| Título: | Un lenguaje visual para la especificación y verificación automática de requerimientos de tiempo real complejos |
| Autor: | Alfonso, Alejandra |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la web: | 2025-06-12 |
| Fecha de defensa: | 2003-05-05 |
| Fecha en portada: | 5 de Mayo de 2003 |
| Grado Obtenido: | Grado |
| Título Obtenido: | Licenciado en Ciencias de la Computación |
| Departamento Docente: | Departamento de Computación |
| Director: | Olivero, Alfredo; Braberman, Víctor Adrián |
| Idioma: | Español |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/seminario_nCOM000238_Alfonso |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000238_Alfonso.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/seminario/document/seminario_nCOM000238_Alfonso |
| Ubicación: | Dep.COM 000238 |
| 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. Alfonso, Alejandra. (2003). Un lenguaje visual para la especificación y verificación automática de requerimientos de tiempo real complejos. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/seminario_nCOM000238_Alfonso |
Resumen:
La construcción de sistemas de tiempo real libres de fallas es un objetivo perseguido por muchas actividades industriales debido al alto costo monetario y en vidas humanas que pueden provocar los desperfectos en los sistemas que éstas utilizan. Si bien existen numerosas herramientas para modelización de sistemas y verificación automática de propiedades sobre los mismos, la transferencia al ámbito industrial es lenta. Una de las razones fundamentales para este fenómeno es la poca usabilidad de los lenguajes de especificación existentes, basados en formalismos lógicos difíciles de entender y de usar por diseñadores no familiarizados con ese tipo de herramientas. Nuestra propuesta consiste en brindar una notación gráfica y de alto nivel para especificar requerimientos de sistemas concurrentes y de tiempo real, de forma tal de abstraer a los diseñadores y desarrolladores de los formalismos matemáticos subyacentes y aun así brindarles el poder de las herramientas de verificación formal automática. Este trabajo sienta las bases para un lenguaje gráfico de especificación de propiedades basado en patrones de eventos, que permiten describir de forma simple y abstracta ciertos aspectos de las ejecuciones de un sistema. Por ejemplo, el orden en que deben ocurrir los eventos, la separación en el tiempo entre dos eventos, el conjunto de eventos que no deben ocurrir entre dos puntos de la ejecución, etc. El lenguaje de nuestros patrones está basado en órdenes parciales de eventos y su semántica está inspirada en el concepto de pattern matching. Patrones de mal comportamiento, es decir, en la descripción de comportamientos que invalidarían requerimientos críticos del sistema. Demostramos que contando con un modelo del sistema expresado con autómatas temporizados, el problema de "model-checking" de patrones de mal comportamiento puede ser reducido al problema clásico de verificación de autómatas temporizados. Dado que este último problema se sabe decidible, concluimos que el chequeo de patrones de mal comportamiento también lo es. Por otro lado, utilizamos esta reducción para construir un algoritmo de verificación automática de patrones de eventos basada en las herramientas existentes para model-checking de autómatas temporizados. Este algoritmo constituye el corazón de un prototipo de verificador de patrones de eventos que desarrollamos en Java.
Citación:
---------- APA ----------
Alfonso, Alejandra. (2003). Un lenguaje visual para la especificación y verificación automática de requerimientos de tiempo real complejos. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000238_Alfonso
---------- CHICAGO ----------
Alfonso, Alejandra. "Un lenguaje visual para la especificación y verificación automática de requerimientos de tiempo real complejos". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2003.https://hdl.handle.net/20.500.12110/seminario_nCOM000238_Alfonso
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000238_Alfonso.pdf
Distrubución geográfica
