Investigadors de la UB dissenyen un programari lliure d’errors
Els programes informàtics tenen cada vegada una major rellevància en el funcionament de la societat. Aquesta dependència implica també l’exposició als riscos dels inevitables errors de programació, que poden arribar a causar pèrdues econòmiques milionàries, com les produïdes per l’estavellament de prototips Boeing 737 MAX. 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. 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 software 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, 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
Els programes informàtics sovint necessiten una gestió molt precisa del temps per processar aspectes com, per exemple, 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 dels 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.
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 converteixen 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 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. 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. “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 practica”.
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.
Aquest projecte disposa d’un pressupost total que supera els 2.200.000 euros, i ha estat gestionat a través de la Fundació Bosch i Gimpera, l’oficina de transferència de resultats de la investigació de la UB.
El projecte, amb el número d’expedient RTC-2017-6740-7, està cofinançat pel Fons Europeu de Desenvolupament Regional (FEDER) de la Unió Europea.
