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

Nel mondo della robotica, costruire una singola macchina che si muove e pensa è già di per sé difficile. Costruire una squadra di esse che lavori insieme senza scontrarsi è una sfida di un tipo completamente diverso. Queste macchine, spesso chiamate robot mobili autonomi, sono progettate per navigare in ambienti reali, evitando muri, persone e l'una l'altra mentre cercano di raggiungere destinazioni specifiche. Il software che le pilota è incredibilmente complesso, basandosi su un flusso costante di dati provenienti da sensori come i laser per capire dove si trovano e cosa hanno intorno. Poiché questi robot operano in un mondo fisico continuo, i loro movimenti sono fluidi e regolari, cambiando per frazioni minuscole di secondo e millimetri di distanza. Tuttavia, i computer che li controllano pensano in passi discreti, elaborando informazioni in blocchi distinti di tempo. Questo divario tra la realtà fluida della fisica e la logica a tappe del codice crea un punto cieco pericoloso. Se il software non è perfettamente tarato, un robot potrebbe muoversi troppo velocemente perché i suoi sensori riescano a rilevare un ostacolo, oppure due robot potrebbero arrivare alla stessa intersezione esattamente nello stesso momento, portando a un vicolo cieco in cui nessuno dei due può muoversi.

Per risolvere questo problema, i ricercatori hanno bisogno di un modo per testare ogni possibile scenario che una squadra di robot potrebbe affrontare prima ancora di accendere le macchine reali. È qui che entra in gioco un campo chiamato verifica formale. Invece di eseguire una simulazione alcune volte sperando nel meglio, la verifica formale utilizza la logica matematica per controllare ogni singolo percorso che un sistema potrebbe intraprendere. Pone una domanda semplice ma potente: esiste una qualsiasi sequenza di eventi, per quanto improbabile, che causi il fallimento del sistema? Per una squadra di robot, questo significa dimostrare che non si scontreranno mai, non rimarranno mai bloccati per sempre e raggiungeranno sempre i loro obiettivi. La sfida è sempre stata che i robot reali si muovono in un mondo continuo, mentre queste prove matematiche richiedono che il mondo venga suddiviso in una griglia di passi fissi. Se i passi sono troppo grandi, la prova ignora piccoli ma critici incidenti. Se i passi sono troppo piccoli, il computer viene sopraffatto dall'enorme numero di possibilità e non riesce a completare il calcolo.

Per colmare questo divario, un gruppo di ricercatori della Mälardalen University e della KTH Royal Institute of Technology in Svezia ha sviluppato un nuovo metodo. Hanno creato un sistema che consente agli ingegneri di progettare una squadra di robot multi-robot utilizzando un linguaggio di modellazione specializzato chiamato Timed Rebeca, che tratta ogni robot come un attore indipendente che reagisce ai messaggi. Questo modello viene poi rigorosamente controllato da un computer per garantirne la sicurezza. Fondamentalmente, il team ha anche scritto il software effettivo per i robot utilizzando un sistema standard chiamato ROS2, assicurando che il modello matematico e il codice reale fossero perfettamente allineati. Non si sono limitati a simulare i robot; hanno costruito una versione del modello che fosse abbastanza astratta da essere controllata da un computer, ma abbastanza dettagliata da riflettere la fisica reale delle macchine. Facendo ciò, sono stati in grado di prevedere guasti rari e pericolosi che le simulazioni standard spesso perdono.

I ricercatori si sono concentrati su uno scenario che coinvolge cinque robot che si muovono attraverso una griglia di cinquanta per cinquanta, uno spazio approssimativamente delle dimensioni del pavimento di un grande magazzino. Hanno allestito un ambiente complesso in cui i robot dovevano navigare attorno agli ostacoli e incrociare i propri percorsi per raggiungere i propri obiettivi. Nel mondo reale, questi robot utilizzano scanner laser per rilevare oggetti, effettuando misurazioni centinaia di volte al secondo. Il team ha dovuto capire come tradurre questi raggi laser continui e questi movimenti fluidi nei passi discreti richiesti dal computer. Hanno scoperto che esiste una relazione stretta tra la velocità con cui un robot si muove e la frequenza con cui scansiona l'ambiente circostante. Se un robot si muove troppo velocemente, può percorrere l'intera distanza tra due scansioni senza che il sensore noti un ostacolo sul suo cammino. I ricercatori hanno dimostato che, affinché il loro modello fosse accurato, la velocità del robot doveva essere limitata in modo da non poter attraversare una cella della griglia più velocemente del tempo necessario affinché il sensore si aggiorni. Questa regola, derivata da un principio fondamentale dell'elaborazione dei segnali, ha garantito che il modello digitale non mancasse potenziali collisioni.

Per rendere fattibile il controllo del computer, il team ha dovuto semplificare il mondo senza perdere la verità del problema. Hanno rappresentato i robot non come forme fluide, ma come rettangoli che si muovono da una cella quadrata all'altra, ruotando con incrementi di quarantacinque gradi. Hanno calcolato il tempo necessario per spostarsi tra queste celle in base alla velocità del robot e alla dimensione della cella. Inoltre, hanno pre-calcolato complessi valori trigonometrici, come il seno e il coseno degli angoli, e li hanno memorizzati in tabelle di ricerca (lookup tables) in modo che il computer non dovesse calcolarli da zero ogni volta. Queste ottimizzazioni hanno permesso al model checker di esplorare milioni di stati possibili in pochi minuti. Quando hanno eseguito il controllo, il computer poteva dire loro con assoluta certezza se un determinato insieme di regole avrebbe portato a uno scontro o a un arrivo sicuro.

I risultati dei loro esperimenti sono stati sorprendenti. Nei casi in cui i robot erano programmati con velocità sicure e tempi di attesa variabili, il model checker ha confermato che tutti i cinque robot avrebbero raggiunto le loro destinazioni senza mai scontrarsi o rimanere bloccati. I ricercatori hanno poi eseguito il codice ROS2 effettivo in una simulazione, e i robot si sono comportati esattamente come previsto dal modello, navigando con successo nello spazio affollato. Tuttavia, quando hanno cambiato i parametri per creare una situazione pericolosa — come far muovere tutti i robot alla stessa velocità o impostare una frequenza di scansione troppo bassa rispetto alla velocità — il model checker ha immediatamente trovato un difetto. Ha identificato una specifica sequenza di eventi che avrebbe portato a una collisione. Quando hanno eseguito il codice reale con queste stesse impostazioni pericolose, la simulazione è andata in crash esattamente come previsto dal modello. In un test, il modello ha individuato una collisione dopo aver esplorato solo poche migliaia di stati, mentre la simulazione reale è fallita tre volte su cinque, confermando che il pericolo era reale e prevedibile.

Lo studio ha anche evidenziato l'importanza del tempismo. In uno scenario, i ricercatori hanno impostato i robot a una velocità che era appena troppo elevata per la frequenza di aggiornamento del sensore. Il model checker ha scoperto che questa piccola violazione della regola di sicurezza rendeva una collisione quasi inevitabile, indipendentemente da come i robot fossero programmati per evitare gli altri. Il computer ha mostrato che i robot sarebbero arrivati a un incrocio nello stesso momento e, poiché non potevano vedersi in tempo, si sarebbero scontrati. La simulazione reale ha confermato questo, con i robot che non riuscivano ad evitare l'altro in ogni singola esecuzione. Ciò ha dimostrato che il modello non era solo un esercizio teorico, ma uno strumento pratico in grado di cogliere errori sottili e pericolosi che gli ingegneri umani potrebbero trascurare.

I ricercatori hanno riconosciuto che il loro approccio ha dei limiti. L'attuale metodo richiede agli ingegneri di costruire manualmente sia il modello matematico che il codice reale, un processo che richiede molto tempo e che potrebbe introdurre errori umani. Hanno inoltre osservato che, sebbene il loro sistema potesse gestire cinque robot su una griglia di cinquanta per cinquanta, scalare il sistema a cento robot o a una mappa molto più grande avrebbe rapidamente sovraccaricato la memoria del computer. Il collo di bottiglia è l'enorme numero di percorsi possibili che i robot possono intraprendere; man mano che il numero di robot e la dimensione della mappa aumentano, il numero di combinazioni cresce così velocemente che il computer esaurisce lo spazio per memorizzarle. Nonostante queste limitazioni, il lavoro dimostra che è possibile creare un gemello digitale di un complesso sistema robotico che sia allo stesso tempo semplice da controllare e abbastanza accurato da essere affidabile.

Questa ricerca offre una nuova strada per lo sviluppo di sistemi autonomi sicuri. Trattando la progettazione del software robotico come un processo di costruzione e verifica di un modello matematico in primo luogo, gli ingegneri possono identificare difetti fatali prima che venga costruito o dispiegato un singolo robot. Il team ha dimostrato che, bilanciando attentamente il livello di dettaglio del modello con la necessità di efficienza computazionale, è possibile verificare che un sistema multi-robot si comporterà in modo sicuro nel mondo reale. Il loro lavoro suggerisce che il futuro della robotica non risiede solo nel costruire macchine più intelligenti, ma nel costruire modi migliori per dimostrare che quelle macchine non falliranno quando la situazione lo richiede.