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.

(Foto: Pixabay)

La segunda característica relevante de la nueva tecnología es que los cálculos de la biblioteca informática verificada formalmente incluyen segundos intercalares. Estos segundos son pequeñas discrepancias entre el tiempo atómico y el tiempo medido en la rotación de la Tierra que forman parte del estándar UTC (tiempo universal coordinado o tiempo civil), utilizado en la mayoría de las leyes que tratan tiempo y duraciones. Sin embargo, los segundos intercalares no se suelen tener en cuenta en las bibliotecas de uso general, con los potenciales errores y repercusiones legales que ello comporta. «En una publicación reciente, hemos demostrado matemáticamente que se puede engañar a los registros del tacógrafo ignorando los segundos intercalares, y conducir desde Barcelona a Ámsterdam sin parar, una situación totalmente ilegal. En el mundo real —prosigue el investigador—, este comportamiento no suele producirse, pero las desviaciones de los registros de conducción reales llegan a alrededor del 8 %, por lo que con nuestra biblioteca reducimos la brecha entre prescripción legal e ingeniería práctica».

Además del sector del transporte, el nuevo sistema de gestión temporal está preparado para utilizarse en cualquier otro ámbito que requiera conversiones temporales, especialmente en aquellos sectores en los que sea más necesario un sistema libre de errores, como la aviación, el comercio en línea o la industria.

Este proyecto dispone de un presupuesto total que supera los 2.200.000 euros, y se ha gestionado a través de la Fundación Bosch i Gimpera, la oficina de transferencia de resultados de la investigación de la UB.