Noticias
Inicio  >  Noticias > Investigadores de la UB diseñan un software libre de errores

Investigadores de la UB diseñan un software libre de errores

 

 

19/10/2020

Recerca

Los programas informáticos tienen cada vez mayor relevancia en el funcionamiento de la sociedad. Esta dependencia implica también la exposición al riesgo de los inevitables errores de programación, que pueden que pueden llegar a tener graves consecuencias en vidas humanas y causar pérdidas económicas millonarias, como las producidas al estrellarse prototipos Boeing 737 MAX.

Un equipo de la Universidad de Barcelona, 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.

Un código sin errores verificado matemáticamente

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.

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 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.

 

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. Asimismo, ha tenido 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.


 

Compártelo en:
| Más |
  • Síguenos:
  • botón para acceder al facebook de la universitat de barcelona
  • botón para acceder al twitter de la universitat de barcelona
  • Botón para acceder al Instagram de la Universitat de Barcelona
  • Botón para acceder al Linkedin de la Universitat de Barcelona
  • botón para acceder al youtube de la universitat de barcelona
  • Botón para acceder al Google+ de la Universitat de Barcelona
  • ??? peu.flickr.alt ???
Miembro de la Reconocimiento internacional de la excelencia HR Excellence in Research logo del leru - League of European Research Universities logo del bkc - campus excel·lència logo del health universitat de barcelona campus

© Universitat de Barcelona