Ángel de la guarda

Un investigador trabaja en un traductor de Java a un lenguaje lógico para la detección de errores y como asistente para programadores. Viajará a Redmond becado por Microsoft. 01 de Septiembre 2011
Ángel de la guarda

Juan Pablo Galeotti se dio cuenta a tiempo de que no era lo suyo. Se había anotado en la carrera de Administración en la Facultad de Ciencias Económicas de la Universidad de Buenos Aires (UBA). Tras dos años, abandonaba ese claustro para recalar en la Facultad de Ciencias Exactas. “Desconocía que lo que hoy hago era posible en la Argentina. Pensé que que no se podía trabajar en innovación, en pensar problemas y en desarrollar soluciones”, explica. Galeotti, de 29 años, finalmente se graduó en Ciencias de la Computación, se especializó en ingeniería de software aplicada y actualmente transita su doctorado —dirigido por Marcelo Frías— dentro del grupo de Métodos Formales Relacionales del departamento de Computación de la UBA. Pero también estudió actuación y participó de algunas obras de teatro, aunque ahora está “retirado de las tablas”. De hecho, asegura que la buena docencia y la actuación “son muy parecidas”, porque en ambos casos hay un público para “capturar”.

El investigador resultó ganador del Programa de Investigación y Doctorados para Becarios de Microsoft y viajará el mes que viene a la sede de la firma en Redmond, Estados Unidos. “Me interesa establecer un vínculo con la gente que trabaja en Microsoft Research porque es gente de primerísimo nivel, a la que he leído, y que marca punta en algunos temas”, dice. Allí continuará trabajando en su trabajo de formación doctoral, cuya idea básica es la búsqueda de errores (bugs) en programas, a partir de una herramienta desarrollada en el grupo de Métodos Formales Relacionales del departamento de Computación de Exactas.

“Mi motivación proviene de mi trabajo como programador. Cuando empecé a estudiar conocí un mundo en el cual se usa la computadora para tratar de ayudar al programador, a encontrar errores en los programas y darles un soporte a quienes trabajan en ellos, como una especie de ángel de la guarda”, explica Galeotti.

La herramienta en cuestión es DynAlloy, una extensión del lenguaje lógico Alloy (http://alloy.mit.edu) desarrollada por el citado grupo de la UBA. DynAlloy es usada como una suerte de “model-checker” que permite ver si una propiedad de buen funcionamiento se cumple o no.

Según el investigador, “se trata de tomar un programa, traducirlo a un lenguaje lógico y chequear si cumple o no con determinadas propiedades deseables, es decir, que no tiene errores, ‘bugs’… En caso de que no pueda determinar si está bien o mal, que al menos proporcione automáticamente casos de tests para determinarlo”. Y añade: “La idea es que el programador cuente con una herramienta fácil de usar, como una especie de corrector ortográfico que le diga ‘mirá, acá puede haber un error’, o ‘cuidado, acá puede haber una falla de seguridad’”.

El traductor
Con este objetivo, el grupo del que participa Galeotti desarrolló JAT (Java Automated Testing), una herramienta que “traduce” secuencias del lenguaje Java a DynAlloy. Se trata de una herramienta que todavía está en la etapa de prototipo, y que están extendiendo para capturar aspectos como herencia o polimorfismo. “Casi todo salvo Reflection; lo que queremos es poder trabajar con modelos DynAlloy que provienen de problemas reales”, amplía.

Y agrega: “Estamos trabajando en cómo hacer para trabajar con modelos DynAlloy muy grandes. Una de las ideas es usar abstracción: tomar el modelo y traducirlo en otro modelo más abstracto, ir refinándolo cada vez más mediante la verificación de los contraejemplos que va dando esa abstracción. Por ejemplo, tengo un programa, me olvido de todas las variables y sólo me quedo con las verdaderas o falsas. Y busco un contraejemplo sobre ese programa. Pero, como se hizo una abstracción del programa, puede ser espurio, puede no tener que ver con la realidad, y entonces hay que trabajar sobre eso. A veces es como tratar de meter un camello en el ojo de una aguja, porque se usa algo muy limitado para problemas reales, pero puede llegar a ser útil para el trabajo de un programador, sobre todo si logramos una interfaz simple”.

Galeotti ejemplifica cómo desearía que funcione: “De igual manera que el compilador dice ‘acá falta una coma’, que diga ‘acá no se cumple la condición que usted quiere que se cumpla siempre’. O, al menos, que diga: ‘Cuidado, acá me parece que quizás no se cumple la condición’. Y que, por otro lado, que cuando encuentre algo, genere un gráfico pequeño, fácil de ver, que señale: ‘Quizás cuando se ejecute esta entrada pueda haber un problema’”.

Según lo planeado, este “ángel de la guarda” debería funcionar en un segundo plano, mientras el programador está trabajando en el código, usando la capacidad ociosa del procesador y analizando la parte de código ya estabilizada y tratando de buscar cosas. Y reutilizando lo que ya conoce, para que no esté todo el tiempo conservando una suerte de “caché” de cosas que ya sabe que están bien o que están mal. “Y en un futuro, quién sabe, usando muchas computadoras, usando grid”, aventura Galeotti, quien asegura que tanto el desarrollo de este traductor como el “know how” son de carácter público. “Lo mejor que nos puede pasar como científicos es que las ideas que uno genera sean aplicadas por cualquiera”, asegura.  A un mes de viajar al laboratorio de Microsoft Research en Redmond, donde seguirá profundizando en estos temas —aunque continuará trabajando en el traductor de Java y no con .NET—, Galeotti hace hincapié en que el objetivo es una herramienta que no necesite de un usuario experto. “Que sea como la computadora: un montón de complejidad y de conocimientos acumulados metidos en un paquete. Que uno la enciende, agarra el mouse y listo, funciona”.

Aplicaciones a futuro
Acerca de las potenciales aplicaciones de DynAlloy, Juan Pablo Galeotti, investigador del grupo de Métodos Formales Relacionales del Departamento de Computación de Exactas, asegura que podrían surgir muchas. Por ejemplo, facilitar un mejor aprovechamiento de los recursos de procesamiento del hardware o para análisis de código malicioso. En este último caso, “los virus atacan puertas abiertas en, por caso, uso de protocolos de drivers. Entonces, se lo podría usar para chequear que un programa obedece al protocolo que tiene que obedecer”, explica. También en el área de la criptografía: “Se buscaría verificar que un algoritmo criptográfico funciona bien. Porque son algoritmos que en general tienen poco rango, es decir, poco espacio, pero mucho tiempo de ejecución. Y entonces, en ese caso, podría venir como anillo al dedo”.

 



¿Te gustó la nota?

Comparte tus comentarios

Sé el primero en comentar