VERIFICACIÓN DE PROGRAMAS EN MODELOS DE COMPUTACIÓN NO CONVENCIONALES .
Autor: SANCHO CAPARRINI FERNANDO.
Año: 2001.
Universidad: SEVILLA.
Centro de lectura: INFORMÁTICA.
Centro de realización: E.T.S. DE INGENIERÍA INFORMÁTICA.
Resumen: La
Computación Natural es una disciplina inspirada en el funcionamiento de los organismos vivos. Tiene como objetivo fundamental la simulación e implementación de los procesos dinámicos que se dan en la Naturaleza y que son susceptibles de ser
interpretados como procedimientos de cálculo.
El objetivo de la memoria es establecer un marco formal que permita la verificación de programas desarrollados en algunos modelos relevantes de computación natural: el modelo sticker y los P sistemas de transición, siendo, el primero de ellos
un modelo de computación molecular, y el segundo un modelo de computación celular. Como ejemplo de aplicación, se presenta el diseño y posterior verificación formal de programas que resuelven, en dichos modelos, algunos problemas clásicos
NP-completos.
Entre las aportaciones que la memoria presenta queremos destacar:
1,- Desarrollo de un método de representación de conjuntos numéricos en el modelo sticker.
2,- Diseño de procedimientos moleculares en el modelo sticker que resuelven problemas de carácter general sobre conjuntos numéricos y que pueden ser usados como subrutinas (problema del rellenado, el del recubrimiento, de la ordenación
cardinal, de las familias disjuntas, y tratamiento de funciones peso sobre conjuntos).
3,- Diseño de las primeras soluciones moleculares a algunos problemas NP-completos (Subset-Sum, de la Mochila en suversión acotada y no acotada, Set-Packing, Exact-Cover) y mejora de una solución molecular del problema del Recubrimiento
Minimal.
4,- Desarrollo de una metodología para la verificación de programas en un modelo de computación molecular con memoria.
5,- Aplicación de la metodología anterior a los programas diseñados en el modelo sticker.
6,- Elaboración de una formalización de los P sistemas de transición.
7,- Primera aproximación a la verificación de P sistemas de transición.
8,- Diseño y verificación de P sistemas de transición que proporcionan soluciones no deterministas, en sentido fuerte, de los problemas SAT y HPP.
> 
