Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

In de wereld van de robotica is het al moeilijk genoeg om een enkele machine te bouwen die beweegt en denkt. Het bouwen van een team van dergelijke machines dat samenwerkt zonder op elkaar te botsen, is een heel andere uitdaging. Deze machines, vaak autonome mobiele robots genoemd, zijn ontworpen om door echte omgevingen te navigeren, waarbij ze muren, mensen en elkaar ontwijken terwijl ze proberen specifieke bestemmingen te bereiken. De software die ze aanstuurt is ongelooflijk complex en vertrouwt op een constante stroom gegevens van sensoren zoals lasers om te begrijpen waar ze zich bevinden en wat er om hen heen is. Omdat deze robots in een continue fysieke wereld opereren, zijn hun bewegingen vloeiend en soepel, veranderend met minuscule fracties van een seconde en millimeters afstand. De computers die hen aansturen denken echter in discrete stappen, waarbij informatie in afzonderlijke blokken tijd wordt verwerkt. Deze kloof tussen de vloeiende realiteit van de fysica en de stap-voor-stap logica van code creëert een gevaarlijke blinde vlek. Als de software niet perfect is afgestemd, kan een robot te snel bewegen voor zijn sensoren om een obstakel op te merken, of kunnen twee robots precies op hetzelfde moment een kruispunt bereiken, wat leidt tot een deadlock waarbij niemand meer kan bewegen.

Om dit op te lossen, hebben onderzoekers een manier nodig om elk mogelijk scenario te testen waar een robotteam mee te maken zou kunnen krijgen voordat ze de echte machines überhaupt aanzetten. Hier komt een vakgebied genaamd formele verificatie in beeld. In plaats van een simulatie een paar keer te draaien en te hopen op het beste, gebruikt formele verificatie wiskundige logica om elke mogelijke route te controleren die een systeem kan nemen. Het stelt een eenvoudige maar krachtige vraag: is er een mogelijke reeks gebeurtenissen, hoe onwaarschijnlijk ook, die het systeem doet falen? Voor een team van robots betekent dit bewijzen dat ze nooit zullen botsen, nooit voor eeuwig vast komen te zitten en altijd hun doelen zullen bereiken. De uitdaging is altijd geweest dat echte robots in een continue wereld bewegen, terwijl deze wiskundige bewijzen vereisen dat de wereld wordt onderverdeeld in een raster van vaste stappen. Als de stappen te groot zijn, mist het bewijs kleine maar kritieke ongelukken. Als de stappen te klein zijn, raakt de computer overbelast door de enorme hoeveelheid mogelijkheden en kan hij de berekening niet voltooien.

Om dit op te lossen, hebben onderzoekers van de Mälardalens University en de KTH Royal Institute of Technology in Zweden een nieuwe manier ontwikkeld om deze kloof te overbruggen. Ze hebben een systeem gecreëerd waarmee ingenieurs een team van meerdere robots kunnen ontwerpen met behulp van een gespecialiseerde modellerings taal genaamd Timed Rebeca, die elke robot behandelt als een onafhankelijke actor die reageert op berichten. Dit model wordt vervolgens rigoureus gecontroleerd door een computer om de veiligheid te garanderen. Cruciaal is dat het team ook de eigenlijke software voor de robots heeft geschreven met behulp van een standaard systeem genaamd ROS2, waardoor het wiskundige model en de echte code perfect op elkaar waren afgestemd. Ze hebben de robots niet alleen gesimuleerd; ze hebben een versie van het model gebouwd die abstract genoeg was om door een computer gecontroleerd te worden, maar gedetailleerd genoeg om de echte fysica van de machines te weerspiegelen. Door dit te doen, konden ze zeldzame en gevaarlijke fouten voorspellen die standaard simulaties vaak missen.

De onderzoekers concentreerden zich op een scenario waarbij vijf robots over een rooster van vijftig bij vijftig bewegen, een ruimte die ongeveer de grootte heeft van een grote magazijnvloer. Ze zetten een complexe omgeving op waarin de robots obstakels moesten omzeilen en elkaars pad moesten kruisen om hun doelen te bereiken. In de echte wereld gebruiken deze robots laserscanners om objecten te detecten, waarbij ze honderden keren per seconde metingen verrichten. Het team moest uitzoeken hoe ze deze continue laserstralen en vloeiende bewegingen konden vertalen naar de discrete stappen die nodig zijn voor de computer om de logica te controleren. Ze ontdekten dat er een strikte relatie bestaat tussen hoe snel een robot beweegt en hoe vaak hij zijn omgeving scant. Als een robot te snel beweegt, kan hij de volledige afstand tussen twee scans afleggen zonder dat de sensor een obstakel in zijn pad opmerkt. De onderzoekers bewezen dat voor hun model accuraat te zijn, de snelheid van de robot beperkt moest worden, zodat deze niet sneller een roostercel kon doorkruisen dan de tijd die nodig is voor de sensorupdate. Deze regel, afgeleid van een fundamenteel principe van signaalverwerking, zorgde ervoor dat het digitale model geen potentiële botsingen zou missen.

Om de computercontrole haalbaar te maken, moest het team de wereld vereenvoudigen zonder de essentie van het probleem te verliezen. Ze stelden de robots niet voor als vloeiende vormen, maar als rechthoeken die van de ene vierkante cel naar de andere bewegen, draaiend in stappen van veertig graden. Ze berekenden de tijd die nodig was om tussen deze cellen te bewegen op basis van de snelheid van de robot en de grootte van de cel. Ze berekenden ook complexe trigonometrische waarden, zoals de sinus en cosinus van hoeken, vooraf en sloegen deze op in lookup-tabellen, zodat de computer ze niet telkens opnieuw hoefde te berekenen. Deze optimalisaties stelden de modelchecker in staat om miljoenen mogelijke toestanden binnen enkele minuten te verkennen. Wanneer ze de controle uitvoerden, kon de computer met absolute zekerheid aangeven of een specifieke set regels zou leiden tot een botsing of een veilige aankomst.

De resultaten van hun experimenten waren opmerkelijk. In gevallen waarin de robots geprogrammeerd waren met veilige snelheden en variërende wachttijden, bevestigde de modelchecker dat alle vijf de robots hun bestemmingen zouden bereiken zonder ooit te botsen of vast te komen zitten. De onderzoekers draaiden vervolgens de eigenlijke ROS2-code in een simulatie, en de robots gedroegen zich precies zoals het model had voorspeld, waarbij ze de drukke ruimte succesvol navigeerden. Echter, toen ze de parameters wijzigden om een gevaarlijke situatie te creëren — zoals het laten bewegen van alle robots met exact dezelfde snelheid of het instellen van een te lage scansnelheid voor de snelheid — vond de modelchecker onmiddellijk een fout. Het identificeerde een specifieke reeks gebeurtenissen die tot een botsing zou leiden. Wanneer ze de echte code met deze zelfde gevaarlijke instellingen draaiden, crashte de simulatie op exact dezelfde manier als het model had voorspeld. In één test vond het model een botsing na het verkennen van slechts enkele duizend toestanden, terwijl de echte simulatie drie van de vijf keer faalde, wat bevestigde dat het gevaar echt en voorspelbaar was.

De studie benadrukte ook het belang van timing. In één scenario stelden de onderzoekers de robots in op een snelheid die net iets te snel was voor de sensorupdatefrequentie. De modelchecker vond dat deze kleine overtreding van de veiligheidsregel een botsing bijna onvermijdelijk maakte, ongeacht hoe de robots geprogrammeerd waren om elkaar te ontwijken. De computer toonde aan dat de robots een kruispunt op hetzelfde moment zouden bereiken en omdat ze elkaar niet op tijd konden zien, zouden ze botsen. De echte simulatie bevestigde dit, waarbij de robots in elke uitvoering faalden om elkaar te ontwijken. Dit toonde aan dat het model niet slechts een theoretische oefening was, maar een praktisch hulpmiddel dat subtiele, gevaarlijke fouten kon vangen die menselijke ingenieurs over het hoofd zouden kunnen zien.

De onderzoekers erkenden dat hun aanpak beperkingen heeft. De huidige methode vereist dat ingenieurs handmatig zowel het wiskundige model als de echte code bouwen, wat een tijdrovend proces is dat menselijke fouten kan introduceren. Ze merkten ook op dat hoewel hun systeem vijf robots op een rooster van vijftig bij vijftig kon aan, het opschalen naar honderd robots of een veel grotere kaart de computer snel zou overbelasten. De bottleneck is het enorme aantal mogelijke paden die de robots kunnen nemen; naarmate het aantal robots en de grootte van de kaart toenemen, groeit het aantal combinaties zo snel dat de computer geen ruimte meer heeft om ze op te slaan. Ondanks deze beperkingen bewijst hun werk dat het mogelijk is om een digitale tweeling van een complex robotisch systeem te maken die zowel eenvoudig genoeg is om te controleren als nauwkeurig genoeg om te vertrouwen.

Dit onderzoek biedt een nieuwe weg voor de ontwikkeling van veilige autonome systemen. Door het ontwerp van robotsoftware te behandelen als een proces waarbij eerst een wiskundig model wordt gebouwd en geverifieerd, kunnen ingenieurs fatale fouten identificeren voordat er ook maar één robot wordt gebouwd of ingezet. Het team heeft aangetoond dat het, door zorgvuldig de balans te vinden tussen het detailniveau van het model en de noodzaak van computationele efficiëntie, mogelijk is om te verifiëren dat een multi-robot systeem veilig zal functioneren in de echte wereld. Hun werk suggereert dat de toekomst van de robotica niet alleen ligt in het bouwen van intelligentere machines, maar in het bouwen van betere manieren om te bewijzen dat die machines niet zullen falen op de momenten dat het er echt toe doet.