Un equip de la Universitat de Barcelona, juntament amb les empreses Formal Vindications i Guretruck, ha desenvolupat un sistema per aconseguir programes informàtics lliures d’errors. Amb mètodes de la lògica matemàtica, aquesta revolucionària tecnologia permet un programari infal·lible, i aconsegueix l’exacta correspondència entre allò que el programari executa i les instruccions que li han estat donades. 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, uns instruments de vital importància per a la regulació legal de la indústria del transport. El treball està liderat per Joost Joosten, professor del Departament de Filosofia de la Universitat de Barcelona i investigador de l’Institut de Matemàtica de la UB (IMUB).
Els programes informàtics sovint necessiten una gestió molt precisa del temps per processar aspectes com l’hora de començament d’un esdeveniment, la data límit d’una gestió legal o el temps de conducció màxim permès als transportistes. En aquest procés, el programari depèn dels segellats de temps, el mecanisme digital que permet demostrar que unes dades electròniques s’han produït en una data i una hora concretes. Errors en el codi que gestiona aquestes dates poden tenir repercussions legals importants, com per exemple les causades per defectes en el processament de la informació del tacògraf, l’aparell que controla les franges horàries de conducció dels transportistes. Per processar aquesta informació horària, els investigadors d’aquest projecte han desenvolupat un gestor de temps basat en una nova biblioteca informàtica de temps —un subtipus de programa informàtic utilitzat en el desenvolupament de programari— que està verificada formalment. Aquesta biblioteca incorpora dues novetats que la transformen en un convertidor horari d’alta precisió, excel·lent per als sectors industrials que necessiten uns estàndards de seguretat i de fiabilitat elevats. En primer lloc, s’ha verificat 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, s’utilitza una innovadora tècnica logicomatemàtica per extreure un algoritme que tradueix aquesta especificació al llenguatge matemàtic. 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 no només que el codi 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.
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’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. «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.
