UR comunicación.-

El grupo de investigación está integrado por Julio Rubio, Jónathan Heras y María Poza, por parte de la Universidad de La Rioja; mientras que por parte del Centro de Investigación Biomédica de La Rioja (CIBIR) participan Miguel Morales –coordinador–, Gadea Mata y Germán Cuesto.

Un avance de este estudio fue premiado, recientemente, con la Perla AICA «a la mejor aplicación industrial del Álgebra Computacional», entregado durante la Jornada sobre Aplicaciones Industriales del Álgebra Computacional (AICA 2011) celebrada en la Universidad de Granada. Los resultados también se han presentado en el Congreso Álgebra Computacional en Topología Algebraica y sus Aplicaciones en Houston (EE UU).

La Unidad de Plasticidad Sináptica Estructural, dirigida por el doctor Miguel Morales, mostró su interés en la automatización del proceso de estudio de imágenes biomédicas, de las neuronas en este caso, que hasta ahora se hacía de forma manual.

El ojo humano interpreta una imagen digital (ya sea un TAC, una ecografía u otras) ayudándose solo de su capacidad visual para completar información insuficiente o borrosa que aparece en la imagen. Sin embargo, cuando una imagen se procesa con un programa informático, el ordenador solo “ve” un conjunto de píxeles sin ninguna estructura.

Estos programas tienen que aplicar técnicas complicadas para intentar emular lo que el ojo humano ve y el cerebro interpreta. Posteriormente es necesario comprobar con los expertos que los resultados obtenidos por el ordenador son coherentes con sus expectativas. Por tanto, se trata de diseñar un programa que obtenga los mismos resultados visualmente y a través del ordenador y, a su vez, asegurar la corrección de ese programa.

En este sentido, el objetivo global del trabajo en curso es asegurar la corrección de programas informáticos relacionados con el cálculo científico, centrándose actualmente en el campo de la biomedicina, ámbito en el que interesa especialmente que los resultados sean correctos.

La corrección de un programa se asegura aplicando lo que se denominan métodos formales de la ingeniería del software. Los investigadores de la UR plantean la corrección de un programa concreto como un enunciado de un teorema matemático. Así, cuando demuestran el teorema logran asegurar la corrección; y para demostrar los teoremas de forma segura utilizan otros programas informáticos especializados en esa tarea.

Aunque el proyecto está actualmente en fase de desarrollo, los investigadores de la Universidad de La Rioja ya han conseguido tener una versión certificada (con corrección asegurada) de un programa de procesamiento de imágenes digitales; si bien aún no es lo suficientemente eficaz como para aplicarlo a imágenes biomédicas reales (que son muy voluminosas). En cambio, han logrado programas que procesan datos reales, pero cuya certificación continúa siendo objeto de investigación.

En la batalla entre eficiencia (reducir el tiempo de procesamiento) y la fiabilidad (asegurar que el programa está libre de errores al 100%), los programas rápidos son mucho más complejos pero es más fácil introducir errores en ellos. Por lo tanto, los investigadores de la UR trabajan con dos versiones de los programas: una en producción, eficaz, y otra de laboratorio, más lenta, pero con corrección asegurada al 100%; luego comparan los resultados de ambas para mejorar la confianza en la versión rápida. Hasta el momento no han aparecido discrepancias.