El hombre que ideó cómo detectar ‘aceitunas envenenadas’ en los programas informáticos
Edmund E. Clarke fue uno de los padres de la técnica de la verificación de modelos, usado en la titánica tarea de encontrar errores en el ‘software’
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.
