Todos los programas informáticos contienen errores; incluso los que controlan la industria aeronáutica o militar tienen fallos en el producto final. Esta situación es especialmente preocupante debido a la cada vez mayor dependencia de la programación en procesos tan importantes como los mecanismos de voto informático, las tecnologías médicas o las aplicaciones que deciden si una persona cumple o no la ley. Un equipo de la Universidad de Barcelona (UB) participa en un proyecto de cuatro años de duración que impulsa un nuevo paradigma dentro de la industria del software: el desarrollo por primera vez en España de un software a gran escala sin errores. El proyecto ‘Software Fallo 0’ aplicará una innovadora metodología de programación para evaluar los datos recogidos por el tacógrafo, un instrumento que monitoriza la actividad de cada vehículo para detectar cuándo se incumple la normativa. Actualmente un software no verificado lleva a cabo esta tarea evaluadora y, como cualquier software, comete errores que han supuesto grandes pérdidas a empresas del sector, e incluso fuertes agravios a los derechos de las personas.
“El método para conseguir este software sin errores supone no solamente un cambio abismal en la calidad del producto final, sino también un cambio en el paradigma de programación, ya que la programación tradicional usa un tipo de arquitectura que es la responsable de gran parte de los errores o bugs”, explica Joost Joosten, investigador del Instituto de Matemáticas de la UB, que lidera el proyecto. “La media de la industria del software suele situarse entre los 15 y los 50 errores por cada mil líneas de código. El software verificado formalmente garantiza cero errores”, recuerda el investigador.
La primera fase del proyecto es la creación de un software capaz de reproducir las leyes de transporte de mercancías por carretera a partir de las regulaciones de transporte de la Unión Europea, Estados Unidos, Brasil y Canadá, países en los que el problema tecnológico en este campo se encuentra exactamente en el mismo punto. La metodología para lograr este objetivo consiste en escribir especificaciones formales, en este caso sobre las leyes del transporte, en vez de escribir directamente el software, y en trasladar estas especificaciones a un lenguaje lógico-matemático del que se extraería el software definitivo sin fallos.

“A través de este proceso se extrae directamente un programa informático que garantiza el seguimiento de dichas especificaciones basadas en la ley. La clave que marca la diferencia es que este código se extrae de demostraciones matemáticas. Dichas demostraciones aseguran al cien por cien la corrección del código con respecto a las especificaciones detalladas al principio del proceso”, detalla Joost Joosten.
La metodología parte del paradigma de programación funcional, que suele utilizarse en los sectores en los que la fiabilidad es crítica. Posteriormente, el objetivo es llevar el estándar de seguridad un paso más allá y convertir el programa en un código verificado formalmente, y por tanto sin errores, y certificado mediante un proceso lógico-matemático. “La principal diferencia entre el software verificado formalmente y el software tradicional es que este último se prueba solamente sobre casos particulares, en un proceso que se lleva a cabo a posteriori del desarrollo del programa. En cambio, la verificación formal tiene como objetivo verificar el conjunto total de ejecuciones posibles del programa. Por eso, el procedimiento por el cual se verifica formalmente un software es totalmente distinto, pues debe acompañarle la fuerza de las demostraciones matemáticas exactas. De hecho, el código resultante es el producto de dichas demostraciones, y por lo tanto es un proceso de prueba a priori”, destaca el investigador.

La verificación formal ha despertado recientemente el interés de la NASA, que próximamente celebrará su 11 Simposio sobre Métodos Formales, y ya se ha implementado en otros proyectos. Uno de los primeros fue el metro de París sin conductor, RATP. Sus informes indican que la verificación formal del software reveló errores que las fases intensivas de pruebas no habían revelado antes. Sin embargo, frente a la metodología empleada en París, la de este proyecto, que usa un asistente de demostración llamado Coq, es más ambiciosa, al ser más costosa pero a la vez más potente, es decir, capaz de llevar la verificación formal a ámbitos más complejos. Algunos proyectos de éxito que usan esta misma metodología son CompCert, un compilador del lenguaje de programación C verificado formalmente usando Coq, y el sistema operativo eChronos RTOS, verificado formalmente usando el asistente de demostración Isabelle.
Detrás de todas estas técnicas está la teoría de la demostración avanzada, que es una rama de la lógica matemática. “Lo que hacemos es demostrar matemáticamente, usando una lógica que se llama lógica constructiva, que existe un algoritmo con tal o cual propiedad, en este caso las especificaciones obtenidas de la ley del transporte. Al hacerlo, el algoritmo extraído vendrá con un certificado de que cumple con las especificaciones. Este proceso de certificación es largo, pero todos los pasos que se usan para completarlo son muy simples y la corrección se puede verificar con Coq, un programa que sirve como asistente de demostración. De esta forma, se comprueban los muchos pero simples pasos que confirman que el software es correcto”, resume Joost Joosten.
El resultado del proyecto constituirá un gran avance, ya que al no producir errores se eliminará la posibilidad de sanciones erróneas por fallos del software que evalúa los datos del tacógrafo, lo cual reducirá procesos administrativos y judiciales y generará seguridad jurídica tanto a los profesionales del transporte como a los cuerpos de seguridad de los estados.
Esta iniciativa, que cuenta con un presupuesto total que supera los 2.200.000 euros, está incluida en la convocatoria Retos Colaboración del Ministerio de Ciencia e Innovación y Universidades, cuyo objetivo es la financiación de proyectos en cooperación entre empresas y organismos de investigación.
Además de la Fundación Bosch i Gimpera de la Universidad de Barcelona, en el consorcio del proyecto también participan Guretruck, una empresa que ofrece a entidades servicios de ingeniería informática y jurídica relacionados con el mundo del transporte, y Formal Vindications, una empresa especializada en la verificación formal de especificaciones técnicas y de software.
Este proyecto, con número de expediente RTC-2017-6740-7, está cofinanciado por el Fondo Europeo de Desarrollo Regional (FEDER) de la Unión Europea, cuyo objetivo es promover el desarrollo tecnológico, la innovación y una investigación de calidad. (Fuente: UB)