Kjøretidsverifisering av Autonome Robotsystemer i ROS 2
Abstract
Den økte bruken av autonome robotsystemer har nødvendiggjort fremskritt i sikkerhetstiltak på grunnav 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 automatisertsamfunn. Med økende kompleksitet har det blitt tydelig at grundig offline testing ikke kan ta høyde foralle 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 flereverktøy. Et slikt verktøy kalles Kjøretidsverifisering (Runtime Verification, RV). Kjøretidsverifisering, etbegrep som har blitt stadig mer populært, refererer til lette formelle metoder for å observere, analysereog noen ganger avbryte prosessene til systemprogramvare eller Cyber-Physical Systems (CPS). Et avde mest brukte språkene for CPS-robotikk er Robot Operating System (ROS). Selv om ROS har mangetilgjengelige kjøretidsverifiseringsverktøy, har den nylige utgivelsen av ROS 2 skapt et kunnskapsgapangående kompatible verktøy og deres bruk, spesielt med overgangen fra en sentralisert til en distribuertoppdagelsesinfrastruktur. Ved feil eller svikt i en sikkerhetskontroller spiller kjøretidsverifisering enavgjørende rolle i å oppdage hva som gikk galt, n˚ar og hvor det skjedde, og hvordan man kan administrereavbøtende tiltak. Hovedmålet med denne avhandlingen er å lage en pipeline for automatisk generering avRV-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 sikkerhetskravi 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 evalueresgjennom 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 ibruddrapportering.Viktige funn viser at RV-rammeverket effektivt forbedrer sikkerhet og pålitelighet, med overvåkerensom 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 verifiserteRV-overvåkere for ROS 2 er mulig med dagens programvare og er raskt å implementere eller endre, noesom gjør det mulig å teste flere spesifikasjonsmodeller på samme system uten å endre kildekoden.Fremtidig arbeid innebærer å forbedre det generative RV-rammeverket, forbedre maskinvareintegrasjonog 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 andredomener. 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.