Tesis:
Diseño y verificación de algoritmos para el tratamiento difuso de imágenes digitales en teledetección y seguridad
- Autor: LÓPEZ LÓPEZ, María Victoria
- Título: Diseño y verificación de algoritmos para el tratamiento difuso de imágenes digitales en teledetección y seguridad
- Fecha: 2004
- Materia: Sin materia definida
- Escuela: E.T.S. DE INGENIEROS DE TELECOMUNICACION
- Departamentos: MATEMATICA APLICADA A LAS TECNOLOGIAS DE LA INFORMACION
- Acceso electrónico:
- Director/a 1º: MARTIN GARCIA, Lorenzo Javier
- Resumen: En esta memoria se analizan procesos de especificación, diseño, implementación y corrección de algoritmos nítidos y difusos, así como el proceso de derivación de algoritmos correctos a partir de especificaciones formales.Partiendo de la lógica proposicional y la lógica de primer orden clásicas, se aborda el problema de la expresión y valoración de especificaciones formales de algoritmos en el contexto difuso, lo que nos obliga a realizar un estudio del tratamiento de predicados borrosos en el análisis de objetivos. De este modo, se aborda el problema de la especificación formal mostrando la utilidad del rigor lógico-matemático para expresar las propiedades que ofrecen los datos de entrada en la resolución de problemas que se plantean libres de ambigüedades mediante predicados lógicos. En este trabajo se muestran las técnicas de diseño de algoritmos. En el paradigma imperativo se estudia el diseño desde la intuición y desde la especificación mediante la construcción de asertos invariantes que conducen a la implementación de algoritmos correctos (derivación algorítmica). También se estudia la verificación de algoritmos surgidos de las ideas e intuición del programador cuando el código no se relaciona mediante transformaciones directas con la especificación planteada. En ambos casos se muestra una gran colección de ejemplos que constituyen una base para el programador que podrá utilizar a modo de "plantillas" en otros desarrollos.En cuanto al paradigma funcional, en primer lugar se estudian técnicas de inmersión, que conducen a algoritmos depurados mediante transformaciones relacionadas con los asertos que constituyen la especificación de los algoritmos. Se distinguen tipos de recursión en función del número de llamadas recursivas (lineal o múltiple) y también en función del modo de la ejecución de las operaciones en cada etapa del proceso (algoritmos recursivos finales y no finales). Se estudian inmersiones por eficiencia tanto utilizando parámetros de entrada acumuladores, como mediante parámetros de salida conjugando diversos objetivos. Por último se estudia la verificación formal de los algoritmos recursivos lineales y múltiples.En este trabajo se plantea el problema de los algoritmos difusos en implementaciones iterativa y recursiva abordándose el problema de la verificación y valoración de este tipo de algoritmos como generalización de los procesos y técnicas descritas en el caso nítido.Para finalizar el trabajo, se han estudiado problemas que en la actualidad se plantean desde el punto de vista difuso para el tratamiento de imágenes digitales. Por una parte, el problema de la clasificación de este tipo de imágenes mediante modelizaciones con grafos difusos obliga al tratamiento de imágenes digitales. Por una parte, el problema de la clasificación de este tipo de imágenes mediante modelizaciones con grafos difusos obliga al tratamiento de las especificaciones con una lógica y una semántica adecuada. Una vez clasificada una imagen para el estudio de alguna característica se plantean diversos problemas de decisión asociados. En el marco de la clasificación no supervisada se requiere la intervención de un experto que ayude al sistema a decidir cuándo una clasificación es aceptable al menos en cierto grado.Surge entonces la necesidad de evaluar no sólo los resultados sino también el proceso que conduce a estos. Realizamos depuraciones en el diseño de los algoritmos de decisión-clasificación buscando una mejor valoración de los procesos. En este análisis será imprescindible el uso de las técnicas desarrolladas anteriormente. Finalmente diseñamos algoritmos adecuados en el tratamiento de imágenes para su cifrado y descifrado garantizando una transmisión segura y de calidad.Como resultado de las últimas aplicaciones conseguimos algoritmos depurados y correctos en grado suficiente respecto a semánticas apropiadas para su evaluación dentro del contexto de la lógica difusa.En cuanto a la complejidad algorítmica temporal y espacial de los diseños obtenidos se ha comprobado que las técnicas de diseño propuestas conducen a algoritmos notablemente mejores en comparación con otros diseños generados mediante la intuición del programador.