El hombre que ide¨® c¨®mo detectar ¡®aceitunas envenenadas¡¯ en los programas inform¨¢ticos

Encontrar errores en los programas inform¨¢ticos es una tarea tit¨¢nica con una curiosa historia. Uno de los padres de la t¨¦cnica del model checking (verificaci¨®n de modelos) para el an¨¢lisis y detecci¨®n de dichos fallos fue el profesor Edmund E. Clarke, fallecido de covid el pasado diciembre. Pero el equipo de investigaci¨®n que lideraba debi¨® compartir la gloria con el dirigido en Francia por Joseph Siffakis porque ambos grupos llegaron a resultados similares de forma simult¨¢nea. Una coincidencia que se explica por el hecho de que en aquellos a?os no hab¨ªa internet y el acceso a los art¨ªculos de las conferencias y revistas se demoraba en el tiempo. De forma salom¨®nica, el premio Turing de 2002 (el equivalente al Nobel de la Inform¨¢tica) fue concedido a ambos equipos por sus trabajos sobre las citada verificaci¨®n de modelos.

Aunque en los ¨²ltimos a?os, gran parte de los programas inform¨¢ticos que utilizamos en nuestros dispositivos est¨¢ formado por componentes que se sabe que funcionan bien, hay otras que tienen que escribirse manualmente, porque son espec¨ªficas de la aplicaci¨®n que estamos realizando o porque requieren de la inteligencia humana y no se pueden automatizar.

La complejidad del software hace que contenga errores, esto es un hecho. Se ha cuantificado que por cada 1000 l¨ªneas de c¨®digo hay de promedio una l¨ªnea incorrecta, o si ya hemos hecho un esfuerzo grande de an¨¢lisis sobre el c¨®digo, la proporci¨®n puede llegar a un error por cada 10 000 l¨ªneas de c¨®digo.

Para imaginarnos la envergadura de la tarea de buscar errores en un c¨®digo enorme, podemos pensar en un gran olivo. Tiene un tronco s¨®lido, que representa la estructura sobre la que se sostiene el software, pero luego tiene muchas ramas, cada una de las cuales tiene otras ramas m¨¢s peque?as que tambi¨¦n pueden ramificarse una y otra vez hasta que encontramos los frutos, las aceitunas. Supongamos que queremos buscar todas las aceitunas que, por alguna raz¨®n, son defectuosas, o incluso peor, imaginemos que alguna pudiera estar envenenada y es vital encontrarla. Podr¨ªamos utilizar un procedimiento de fuerza bruta, ir ramita por ramita buscando aceitunas defectuosas o venenosas, pero este m¨¦todo ser¨ªa muy tedioso y nos llevar¨ªa much¨ªsimo tiempo. Tambi¨¦n podr¨ªamos echar una ojeada al ¨¢rbol para ver si, por casualidad, vemos alguna aceituna mala. Pero este m¨¦todo tampoco nos convence, porque, si no encontramos ninguna, no podemos tener la certeza de que el ¨¢rbol est¨¦ sano.

La tarea de encontrar un error en un software complejo se parece a la b¨²squeda de la aceituna envenenada. Durante su ejecuci¨®n, el software va recorriendo caminos que son como ramas en el ¨¢rbol. Pero, a priori, no podemos saber qu¨¦ camino se seleccionar¨¢. Por eso, podemos imaginarnos el impacto que supuso, en los a?os 80, el descubrimiento de m¨¦todos autom¨¢ticos para rastrear todas las ramas del ¨¢rbol de manera eficiente. Como era de esperar, ambos, los grupos de Clarke y de Siffakis se basaron en trabajos de investigadores que es precedieron, como es el caso de Zohar Manna y Amir Pnueli, que definieron la l¨®gica temporal en los 70. Esta l¨®gica permite describir el error a buscar (la aceituna envenenada) y, al mismo tiempo, ayuda a los algoritmos de verificaci¨®n de modelos a realizar la b¨²squeda de manera eficiente, podando (simb¨®licamente) aquellas ramas en las que ya se sabe que no hay aceitunas malas, lo que acelera enormemente la b¨²squeda.

Mar¨ªa del Mar Gallardo Melgarejo es catedr¨¢tica del ¨¢rea de Lenguajes y Sistemas Inform¨¢ticos del Departamento de Lenguajes y Ciencias de la Computaci¨®n de la ETSI inform¨¢tica de la Universidad de M¨¢laga.

Cr¨®nicas del Intangible es un espacio de divulgaci¨®n sobre las ciencias de la computaci¨®n, coordinado por la sociedad acad¨¦mica SISTEDES (Sociedad de Ingenier¨ªa de Software y de Tecnolog¨ªas de Desarrollo de Software). El intangible es la parte no material de los sistemas inform¨¢ticos (es decir, el software), y aqu¨ª se relatan su historia y su devenir. Los autores son profesores de las universidades espa?olas, coordinados por Ricardo Pe?a Mar¨ª (catedr¨¢tico de la Universidad Complutense de Madrid) y Macario Polo Usaola (profesor titular de la Universidad de Castilla-La Mancha).

Puedes seguir a EL PA?S TECNOLOG?A en Facebook y Twitter.