Un equipo de la Universidad de Barcelona (Catalunya, España), junto con las empresas Formal Vindications y Guretruck, ha desarrollado un sistema para conseguir programas informáticos libres de errores. Con métodos de la lógica matemática, esta tecnología revolucionaria hace posible un software infalible que logra una correspondencia exacta entre lo que ejecuta y las instrucciones que se le han dado. El primer resultado de este proyecto es una biblioteca informática de tiempo formalmente verificada que permite realizar conversiones horarias de alta precisión y que se prevé aplicar en los tacógrafos, instrumentos de vital importancia para la regulación legal de la industria del transporte. El trabajo está liderado por Joost Joosten, profesor del Departamento de Filosofía e investigador del Instituto de Matemática de la UB.
Los programas informáticos necesitan a menudo una gestión muy precisa del tiempo para procesar aspectos como la hora de comienzo de un evento, la fecha límite de una gestión legal o el tiempo de conducción máximo permitido a los transportistas. En ese proceso, el software depende de los sellados de tiempo, el mecanismo digital que permite demostrar que unos datos electrónicos se han producido en una fecha y una hora concretas. Los errores en el código que gestiona estas fechas pueden tener repercusiones legales importantes, como por ejemplo las causadas por defectos en el procesamiento de la información del tacógrafo, el aparato que controla las franjas horarias de conducción de los transportistas.
Para procesar esa información horaria, los investigadores de este proyecto han desarrollado un gestor de tiempo basado en una nueva biblioteca informática de tiempo —un subtipo de programa informático usado para el desarrollo de software— que está verificada formalmente. Dicha biblioteca incorpora dos novedades que la transforman en un convertidor horario de alta precisión, excelente para los sectores industriales que necesitan estándares de seguridad y fiabilidad elevados. En primer lugar, se ha verificado formalmente que no contiene ningún error en el código, ya que la base de cualquier programa informático es la especificación, es decir, la descripción detallada de las acciones que queremos que haga el programa. En el nuevo sistema, se utiliza una innovadora técnica lógico-matemática para extraer un algoritmo que traduce esa especificación al lenguaje matemático. Posteriormente, para comprobar que no contiene errores, se verifica formalmente a través de un asistente de demostración llamado Coq, un programa informático que comprueba que es completamente fiable. «Este procedimiento no solo permite verificar que el código no contiene errores internos, sino que también demuestra matemáticamente que el código implementado corresponde a la perfección con las especificaciones que se han diseñado», explica Joost Joosten. «Si la ley envía a alguien a la cárcel basándose en la lectura electrónica de un tacógrafo, es mejor estar seguro de que lo que dice el programa es correcto. Por ello esta infalibilidad es tan importante», añade el investigador.
