Verificación de programas en modelos de computación no convencionales

• Autores: Fernando Sancho Caparrini
• Directores de la Tesis: Mario de Jesús Pérez Jiménez (dir. tes.)
• Lectura: En la Universidad de Sevilla ( España ) en 2002
• Idioma: español
• Tribunal Calificador de la Tesis: Carlos Martín Vide (presid.) , Alfonso Rodríguez-Patón Aradas (secret.) , Gheorghe Paun (voc.) , José Antonio Alonso Jiménez (voc.) , Víctor Mitrana (voc.)
• Enlaces
  • Tesis en acceso abierto en: Idus
• 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 transic