Notícies
Inici  >  Notícies > Investigadors de la UB dissenyen un programari lliure d’errors

Investigadors de la UB dissenyen un programari lliure d’errors

 

 

22/10/2020

Recerca

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.

 

Comparteix-la a:
| Més |
  • Segueix-nos:
  • botó per accedir al facebook de la universitat de barcelona
  • botó per accedir al twitter de la universitat de barcelona
  • botó per accedir a l'instagram de la Universitat de Barcelona
  • botó per accedir al linkedin de la Universitat de Barcelona
  • botó per accedir al youtube de la universitat de barcelona
  • botó per accedir al google+ de la universitat de barcelona
  • ??? peu.flickr.alt ???
Membre de la Reconeixement internacional de l'excel·lència HR Excellence in Research logo del ∞ - League of European Research Universities logo del bkc - campus excel·lència logo del health universitat de barcelona campus

© Universitat de Barcelona