Un equip de la Universitat de Barcelona, juntament amb les empreses Formal Vindications SL i Guretruck SL, ha desenvolupat un sistema per aconseguir programes informàtics lliures d’errors que aconsegueix l’exacta correspondència entre allò que el software executa i les instruccions que li han estat donades. L’objectiu de la solució és evitar riscos per problemes en la programació i que poden arribar a causar pèrdues econòmiques milionàries com les produïdes per l’estavellament de prototips Boeing 737 MAX.

El primer resultat d’aquest projecte és una biblioteca informàtica de temps formalment verificada que permet realitzar conversions horàries d’alta precisió i que es preveu aplicar en els tacògrafs, un instrument vital per a la regulació legal de la indústria del transport.

El treball està liderat pel Dr. Joost J. Joosten, professor del Departament de Filosofia de la UB i investigador de l’Institut de Matemàtica de la UB, i ha rebut un ajut de la convocatòria Retos Colaboración del Ministeri de Ciència i Innovació, l’objectiu del qual és finançar projectes en cooperació amb empreses i organismes de recerca.

Un codi sense errors verificat matemàticament

En aquest projecte els investigadors han desenvolupat un gestor de temps per processar aquesta informació horària que es basa en una nova biblioteca informàtica de temps –un subtipus de programari utilitzat per al desenvolupament de software– que està verificada formalment. Aquesta biblioteca incorpora dues novetats que la fan treballar com un convertidor horari d’alta precisió per als sectors industrials que necessiten uns estàndards de seguretat i de fiabilitat elevats.

En primer lloc, s’ha verificat formalment que no conté cap error en el codi, ja que la base de qualsevol programa informàtic és l’especificació, és a dir, la descripció detallada de les accions que volem que faci el programa. En el nou sistema, a partir d’aquesta especificació s’utilitza una innovadora tècnica lògico-matemàtica per extraure un algoritme que tradueix aquesta especificació al llenguatge matemàtic.

La solució demostra matemàticament que el codi implementat correspon a la perfecció amb les especificacions que s’han dissenyat

Posteriorment, per comprovar que no conté errors es verifica formalment a través d’un assistent de demostració anomenat Coq, un programa informàtic que comprova que és completament fiable. “Aquest procediment permet verificar que el codi no només no conté errors interns, sinó que també demostra matemàticament que el codi implementat correspon a la perfecció amb les especificacions que s’han dissenyat”, explica Joost Joosten. “Si la llei envia algú a la presó basant-se en una lectura electrònica d’un tacògraf, és millor estar segur que el que diu el programa és correcte. Per això aquesta infal·libilitat és tan important”, afegeix l’investigador.

Un programari que incorpora els segons intercalars

La segona característica rellevant de la nova tecnologia és que els càlculs de la biblioteca informàtica verificada formalment inclouen segons intercalars. Aquests segons són petites discrepàncies entre el temps atòmic i el temps mesurat en la rotació real de la Terra que formen part de l’anomenat estàndard UTC (temps universal coordinat o temps civil), que s’utilitza en la majoria de les lleis que tracten temps i durades. No obstant això, els segons intercalars no se solen tenir en compte a les biblioteques d’ús general, amb els potencials errors i repercussions legals que això comporta.

La biblioteca redueix la bretxa entre prescripció legal i enginyeria pràctica

“En una publicació recent hem demostrat matemàticament que es pot ‘enganyar’ els registres del tacògraf ignorant els segons intercalars i conduir des de Barcelona fins a Amsterdam sense parar, una situació totalment il·legal. Al món real –prossegueix l’investigador– aquest comportament no se sol produir, però les desviacions dels registres de conducció reals arriben al voltant del 8%, de manera que amb la nostra biblioteca reduïm la bretxa entre prescripció legal i enginyeria pràctica”.

A més del sector del transport, el nou sistema de gestió temporal està preparat per ser utilitzat en qualsevol altre àmbit que requereixi conversions temporals, especialment en aquells sectors en què sigui més necessari un sistema lliure d’errors, com ara l’aviació, el comerç en línia o la indústria.