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.
