| dc.description.abstract | Den økte bruken av autonome robotsystemer har nødvendiggjort fremskritt i sikkerhetstiltak på grunn
av de potensielle farene disse systemene kan utgjøre. Dette økte fokuset på automatisering og robotsys-
temer stiller spørsmål om hvordan sikkerhet og samsvar vil opprettholdes i et stadig mer automatisert
samfunn. Med økende kompleksitet har det blitt tydelig at grundig offline testing ikke kan ta høyde for
alle farer forbundet med uendelige tilstandssystemer, da sikkerheten er begrenset av de definerte testtil-
fellene. For å opprettholde sikkerhet og pålitelighet under drift, er det ofte nødvendig å sette inn flere
verktøy. Et slikt verktøy kalles Kjøretidsverifisering (Runtime Verification, RV). Kjøretidsverifisering, et
begrep som har blitt stadig mer populært, refererer til lette formelle metoder for å observere, analysere
og noen ganger avbryte prosessene til systemprogramvare eller Cyber-Physical Systems (CPS). Et av
de mest brukte språkene for CPS-robotikk er Robot Operating System (ROS). Selv om ROS har mange
tilgjengelige kjøretidsverifiseringsverktøy, har den nylige utgivelsen av ROS 2 skapt et kunnskapsgap
angående kompatible verktøy og deres bruk, spesielt med overgangen fra en sentralisert til en distribuert
oppdagelsesinfrastruktur. Ved feil eller svikt i en sikkerhetskontroller spiller kjøretidsverifisering en
avgjørende rolle i å oppdage hva som gikk galt, n˚ar og hvor det skjedde, og hvordan man kan administrere
avbøtende tiltak. Hovedmålet med denne avhandlingen er å lage en pipeline for automatisk generering av
RV-overvåkere for ROS 2 fra krav i naturlig språk til formelt verifiserte temporale logiske ligninger. For å
oppnå dette, benytter pipelinen NASAs Copilot, OGMA og FRET-verktøy for å konvertere sikkerhetskrav
i naturlig språk til formelt verifiserte temporale logiske overvåkere.
Denne studien tar også for seg gapet i RV-verktøy for ROS 2, og gir en omfattende oversikt over eksis-
terende verktøy, implementeringsstrategier og fordelene med RV i CPS. Rammeverkets ytelse evalueres
gjennom simulering og felttesting ved bruk av landbruksroboten Thorvald-005 og D435 RealSense-
kameraet, med fokus på systembelastning, hendelse-til-strøm-basert kommunikasjon og effektivitet i
bruddrapportering.
Viktige funn viser at RV-rammeverket effektivt forbedrer sikkerhet og pålitelighet, med overvåkeren
som opprettholder akseptabel systemytelse selv under høye meldingshastigheter. Forskningen under-
streker også viktigheten av å erkjenne maskinvarebegrensninger og forbedre prediktive evner for yt-
terligere å øke systemets robusthet. Funnene beviser at automatisk generering av formelt verifiserte
RV-overvåkere for ROS 2 er mulig med dagens programvare og er raskt å implementere eller endre, noe
som gjør det mulig å teste flere spesifikasjonsmodeller på samme system uten å endre kildekoden.
Fremtidig arbeid innebærer å forbedre det generative RV-rammeverket, forbedre maskinvareintegrasjon
og utvide kompatibilitet til andre ROS-distribusjoner. Resultatene har bidratt til den pågående utviklin-
gen av NASAs RV-verktøy, og fremmer sikrere utplassering av autonome systemer i landbruk og andre
domener. Denne avhandlingen er i seg selv et bidrag til metodikken og kunnskapen som er oppnådd for å
riktig forstå og bruke Linear Temporal Logic (LTL)-overvåkere. | |
