Investigadores de la UB diseñan un software libre de errores
Los programas informáticos tienen cada vez una mayor relevancia en el funcionamiento de la sociedad. Esta dependencia implica también la exposición a los riesgos de los inevitables errores de programación, que pueden llegar a causar pérdidas económicas millonarias, como las producidas por el estrellamiento de prototipos Boeing 737 MAX. Un equipo de la Universidad de Barcelona, junto con las empresas Formal Vindications S.L. y Guretruck S.L, ha desarrollado un sistema para conseguir programas informáticos libres de errores. Con métodos de la lógica matemática, esta revolucionaria tecnología permite un software infalible, consiguiendo la exacta correspondencia entre lo que el software ejecuta y las instrucciones que le han sido dadas. 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, un instrumento vital para la regulación legal de la industria del transporte.
El trabajo está liderado por el Dr. Joost J. Joosten, profesor del Departamento de Filosofía de la UB e investigador del Instituto de Matemática de la UB, y ha contado con una ayuda de la convocatoria Retos Colaboración del Ministerio de Ciencia e Innovación, cuyo objetivo es financiar proyectos en cooperación con empresas y organismos de investigación.
Un código sin errores verificado matemáticamente
Los programas informáticos a menudo necesitan una gestión muy precisa del tiempo para procesar aspectos como, por ejemplo, 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 de los transportistas. En este 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. 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.
En este proyecto los investigadores han desarrollado un gestor de tiempo para procesar esta información horaria que se basa en una nueva biblioteca informática de tiempo –un subtipo de programa informático utilizado para el desarrollo de software– que está verificada formalmente. Esta biblioteca incorpora dos novedades que la convierten en un convertidor horario de alta precisión, excelente para los sectores industriales que necesitan unos 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, a partir de esta especificación se utiliza una innovadora técnica lógico-matemática para extraer un algoritmo que traduce esta 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 permite verificar que el código no sólo 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 una 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.
Un programa que incorpora los segundos intercalares
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 real de la Tierra que forman parte del llamado estándar UTC (tiempo universal coordinado o tiempo civil), que se utiliza 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 Amsterdam 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 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 ser utilizado 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 cuenta con un presupuesto total que supera los 2.200.000 euros, y ha sido gestionado a través de la Fundación Bosch i Gimpera, la oficina de transferencia de resultados de la investigación de la UB.
El 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.
