Investigadors de la UB dissenyen un programari lliure dʼerrors

 
 
Recerca
(22/10/2020)

Els programes informàtics tenen cada vegada més 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 tenir greus conseqüències en vides humanes i causar pèrdues econòmiques milionàries, com les produïdes en estavellar-se els prototips Boeing 737 MAX.

 
 
Recerca
22/10/2020

Els programes informàtics tenen cada vegada més 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 tenir greus conseqüències en vides humanes i causar pèrdues econòmiques milionàries, com les produïdes en estavellar-se els prototips Boeing 737 MAX.

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

 

Un codi sense errors verificat matemàticament

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

 

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

Aquest projecte disposa dʼun pressupost total que supera els 2,2 milions dʼeuros, i ha estat gestionat a través de la Fundació Bosch i Gimpera, lʼoficina de transferència de resultats de la recerca de la Universitat de Barcelona.

 

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. Així mateix, ha rebut un ajut de la convocatòria Reptes de Col·laboració del Ministeri de Ciència i Innovació, que té com a objectiu finançar projectes en cooperació amb empreses i organismes de recerca.