Atef Azaiez’ doktorgradsarbeid viser hvordan matematisk verifikasjon kan styre utformingen av landbruksroboter og holde dem trygge i felt, med en nødløsning klar for uventede situasjoner.
Roboter flytter ut av inngjerdede fabrikkhaller og inn på jorder og i frukthager, der de arbeider tett på mennesker og planter. I sin avhandling har Atef Azaiez undersøkt hvordan ingeniører kan vise at slike roboter er trygge ved hjelp av formelle metoder. Dette er matematiske teknikker som sjekker en modell av roboten mot alle situasjoner modellen tillater, ikke bare situasjonene et testteam har tenkt på å prøve.
En gjennomgang av 180 studier publisert mellom 2007 og 2024 viste at forskere stort sett bruker disse teknikkene på et design som allerede er fastlagt, eller til å overvåke en robot mens den er i drift. Landbruk utgjorde to prosent av anvendelsene. Få studier tok for seg robotkomponenter som lærer fra data, for eksempel kamerabasert gjenkjenning av planter.
Azaiez utviklet deretter to metoder for fasene som tidligere arbeid nesten ikke hadde berørt, og testet dem på en modell av en robot som arbeider blant jordbærplanter. Den første metoden lar ingeniører sammenligne designideer matematisk før noen bygger maskinvare, og forkaste ideene som ikke kan oppfylle sikkerhetskravene. Den andre kjører på roboten mens den arbeider. En planlegger justerer robotens oppførsel når forholdene endrer seg, mens en annen overvåker situasjonen og står klar med en nødbrems og bytter til den ved behov.
Hva er de viktigste funnene?
Hovedfunnet er at matematiske garantier for slike roboter ikke kan dekke alt. Noen læringsbaserte komponenter lar seg ikke beskrive presist nok til å sjekkes, og en hel robot er for stor til å analyseres fullt ut. Avhandlingen beskriver hva hver metode dekker og hva den utelater. Deretter bygger den sikkerhetsargumentet slik at det ikke avhenger av at de usjekkede delene oppfører seg riktig.
Hva var målet med doktorgradsarbeidet?
Arbeidet skulle finne ut i hvilke faser av en robots utvikling ingeniører kan etablere formelle sikkerhetsgarantier, og hva som kan støtte en sikkerhetspåstand i fasene der det ikke går.
Hvorfor er denne forskningen viktig?
En robot som arbeider uten gjerde, trenger en sikkerhetsmekanisme som overbeviser tilsynsmyndigheter, sertifiseringsorganer og bonden som bruker den. Testing dekker bare situasjonene noen har prøvd. En matematisk garanti dekker alle situasjoner i modellen, men slutter å gjelde, uten forvarsel, så snart de virkelige forholdene beveger seg utenfor modellen. Ute på jordet skjer det oftere enn i en fabrikk, fordi lys, vær og planter endrer seg fra dag til dag.
For forskningen på robotsikkerhet tar avhandlingen formelle metoder inn i to faser som det tidligere er forsket lite på: tidlig konseptdesign og drift i felt. Ingen av metodene avhenger av jordbærcaset, så ingeniører kan bruke dem på andre roboter i åpne omgivelser. Avhandlingen demonstrerer dem riktignok bare på én plattform. I en større sammenheng kan tilnærmingen hjelpe produsenter med å gi sertifiseringsorganer formelle bevis fra de tidligste designbeslutningene. Den kan også gi bønder roboter med sikkerhetspåstander som sier hva de dekker.
Arbeidet var en del av RoboFarmer-prosjektet, finansiert av Norges forskningsråd.
Atef Azaiez skal forsvare sin doktoravhandling, Verifisering av sikkerhet og pålitelighet av autonome robotsystemer: håndtereusikkerhet gjennom Model sjekking den 20. november 2026. Se disputasoppslaget her.