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

In der Welt der Robotik ist es schon schwierig genug, eine einzige Maschine zu bauen, die sich bewegt und denkt. Ein Team von ihnen zu bauen, das zusammenarbeitet, ohne gegeneinander zu krachen, ist eine ganz andere Art von Herausforderung. Diese Maschinen, oft autonome mobile Roboter genannt, sind darauf ausgelegt, in realen Umgebungen zu navigieren und dabei Wände, Menschen und einander zu umgehen, während sie versuchen, bestimmte Ziele zu erreichen. Die Software, die sie steuert, ist unglaublich komplex und stützt sich auf einen ständigen Datenstrom von Sensoren wie Lasern, um zu verstehen, wo sie sich befinden und was um sie herum ist. Da diese Roboter in einer kontinuierlichen physischen Welt agieren, sind ihre Bewegungen glatt und flüssig und ändern sich um winzige Bruchteile von Sekunden und Millimetern der Distanz. Die Computer, die sie steuern, denken jedoch in diskreten Schritten und verarbeiten Informationen in abgegrenzten Zeitpaketen. Diese Lücke zwischen der glatten Realität der Physik und der schrittweisen Logik des Codes schafft einen gefährlichen blinden Fleck. Wenn die Software nicht perfekt abgestimmt ist, könnte ein Roboter zu schnell fahren, als dass seine Sensoren ein Hindernis erfassen könnten, oder zwei Roboter könnten genau im selben Moment an derselben Kreuzung eintreffen, was zu einem Totpunkt führt, bei dem keiner mehr weiterfahren kann.

Um dies zu lösen, müssen Forscher in der Lage sein, jedes mögliche Szenario, dem ein Roboterteam begegnen könnte, zu testen, bevor sie die echten Maschinen überhaupt einschalten. Hier kommt ein Feld namens formale Verifikation ins Spiel. Anstatt eine Simulation ein paar Mal durchzuführen und auf das Beste zu hoffen, nutzt die formale Verifikation mathematische Logik, um jeden einzelnen Pfad zu prüfen, den ein System nehmen könnte. Sie stellt eine einfache, aber kraftvolle Frage: Gibt es irgendeine mögliche Sequenz von Ereignissen, egal wie unwahrscheinlich, die dazu führt, dass das System versagt? Für ein Roboterteam bedeutet dies zu beweisen, dass sie niemals kollidieren, niemals auf ewig feststecken und immer ihre Ziele erreichen werden. Die Herausforderung bestand bisher immer darin, dass echte Roboter sich in einer kontinuierlichen Welt bewegen, während diese mathematischen Beweise erfordern, dass die Welt in ein Gitter fester Schritte unterteilt wird. Wenn die Schritte zu groß sind, übersieht der Beweis kleine, aber kritische Unfälle. Wenn die Schritte zu klein sind, wird der Computer von der schieren Anzahl der Möglichkeiten überwältigt und kann die Berechnung nicht abschließen.

Ein Forschungsteam der Mälardalen Universität und der KTH Royal Institute of Technology in Schweden hat einen neuen Weg entwickelt, um diese Lücke zu schließen. Sie entwickelten ein System, mit dem Ingenieure ein Multi-Roboter-Team unter Verwendung einer spezialisierten Modellierungssprache namens Timed Rebeca entwerfen können, die jeden Roboter als unabhängigen Akteur behandelt, der auf Nachrichten reagiert. Dieses Modell wird dann von einem Computer streng geprüft, um die Sicherheit zu gewährleisten. Entscheidend ist, dass das Team auch die eigentliche Software für die Roboter mit einem Standard-System namens ROS2 schrieb, um sicherzustellen, dass das mathematische Modell und der reale Code perfekt aufeinander abgestimmt waren. Sie haben die Roboter nicht nur simuliert; sie bauten eine Version des Modells, die abstrakt genug war, um von einem Computer geprüft zu werden, aber detailliert genug, um die reale Physik der Maschinen widerzuspiegeln. Durch dies konnten sie seltene und gefährliche Fehler vorhersagen, die Standard-Simulationen oft übersehen.

Die Forscher konzentrierten sich auf ein Szenario, bei dem fünf Roboter sich über ein Fünfzig-mal-Fünfzig-Gitter bewegen, einen Raum, der etwa der Größe eines großen Lagerhausbodens entspricht. Sie richteten eine komplexe Umgebung ein, in der die Roboter Hindernissen ausweichen und sich gegenseitig kreuzen mussten, um ihre Ziele zu erreichen. In der realen Welt nutzen diese Roboter Laserscanner, um Objekte zu erkennen, wobei sie hunderte Male pro Sekunde Messungen vornehmen. Das Team musste herausfinden, wie sie diese kontinuierlichen Laserstrahlen und glatten Bewegungen in die diskreten Schritte übersetzen, die der Computer zur Überprüfung der Logik benötigt. Sie entdeckten, dass es eine strikte Beziehung zwischen der Geschwindigkeit eines Roboters und der Häufigkeit, mit der er seine Umgebung scannt, gibt. Wenn ein Roboter zu schnell fährt, kann er die gesamte Distanz zwischen zwei Scans zurücklegen, ohne dass der Sensor ein Hindernis in seinem Pfad bemerkt. Die Forscher bewiesen, dass für die Genauigkeit ihres Modells die Geschwindigkeit des Roboters begrenzt sein musste, damit er eine Gitterselle nicht schneller überqueren konnte, als die Zeit für die Aktualisierung des Sensors dauerte. Diese Regel, die aus einem fundamentalen Prinzip der Signalverarbeitung abgeleitet wurde, stellte sicher, dass das digitale Modell keine potenziellen Kollisionen übersah.

Um die Überprüfung durch den Computer machbar zu machen, musste das Team die Welt vereinfachen, ohne die Wahrheit des Problems zu verlieren. Sie stellten die Roboter nicht als glatte Formen dar, sondern als Rechtecke, die sich von einer quadratischen Zelle zur nächsten bewegen und in 45-Grad-Schritten drehen. Sie berechneten die Zeit, die für die Bewegung zwischen diesen Zellen basierend auf der Geschwindigkeit des Roboters und der Größe der Zelle benötigt wurde. Sie berechneten zudem komplexe trigonometrische Werte, wie den Sinus und Kosinus von Winkeln, vorab und speicherten sie in Nachschlagetabellen (Lookup-Tables), damit der Computer sie nicht jedes Mal neu berechnen musste. Diese Optimierungen ermöglichten es dem Model Checker, Millionen von möglichen Zuständen in wenigen Minuten zu explorieren. Als sie die Prüfung durchführten, konnte der Computer mit absoluter Gewissheit sagen, ob ein bestimmter Satz von Regeln zu einem Crash oder einer sicheren Ankunft führen würde.

Die Ergebnisse ihrer Experimente waren bemerkenswert. In Fällen, in denen die Roboter mit sicheren Geschwindigkeiten und variierenden Wartezeiten programmiert wurden, bestätigte der Model Checker, dass alle fünf Roboter ihr Ziel erreichen würden, ohne jemals zu kollidieren oder steckenzubleiben. Die Forscher ließen dann den tatsächlichen ROS2-Code in einer Simulation laufen, und die Roboter verhielten sich exakt so, wie das Modell es vorhersagte, indem sie den überfüllten Raum erfolgreich navigierten. Wenn sie jedoch die Parameter änderten, um eine gefährliche Situation zu erzeugen – etwa indem sie alle Roboter mit der exakt gleichen Geschwindigkeit bewegen ließen oder die Scanrate für die Geschwindigkeit zu niedrig ansetzten –, fand der Model Checker sofort einen Fehler. Er identifizierte eine spezifische Sequenz von Ereignissen, die zu einer Kollision führen würde. Als sie den echten Code mit denselben gefährlichen Einstellungen ausführten, stürzte die Simulation auf die exakt gleiche Weise ab, wie das Modell es vorhergesagt hatte. In einem Test fand das Modell eine Kollision nach der Untersuchung von nur wenigen tausend Zuständen, während die reale Simulation in drei von fünf Fällen fehlschlug, was bestätigte, dass die Gefahr real und vorhersehbar war.

Die Studie hob auch die Bedeutung des Timings hervor. In einem Szenario setzten die Forscher die Roboter auf eine Geschwindigkeit, die nur knapp zu schnell für die Sensor-Aktualisierungsrate war. Der Model Checker fand, dass diese kleine Verletzung der Sicherheitsregel eine Kollision fast unvermeidlich machte, ungeachtet dessen, wie die Roboter programmiert waren, um einander auszuweichen. Der Computer zeigte, dass die Roboter zur gleichen Zeit an einem Kreuzungspunkt ankommen würden und, da sie einander nicht rechtzeitig sehen konnten, zusammenstoßen würden. Die reale Simulation bestätigte dies, wobei die Roboter in jedem einzelnen Durchlauf scheiterten, einander auszuweichen. Dies demonstrierte, dass das Modell nicht nur eine theoretische Übung war, sondern ein praktisches Werkzeug, das subtile, gefährliche Fehler erkennen konnte, die menschliche Ingenieure leicht übersehen könnten.

Die Forscher räumten ein, dass ihr Ansatz Grenzen hat. Die aktuelle Methode erfordert von den Ingenieuren, sowohl das mathematische Modell als auch den realen Code manuell zu erstellen, was ein zeitaufwendiger Prozess ist, der menschliche Fehler einführen kann. Sie merkten auch an, dass ihr System zwar fünf Roboter auf einem 50x50-Gitter handhaben konnte, es aber das Computergedächtnis schnell überfordern würde, wenn man es auf hundert Roboter oder eine viel größere Karte skalieren würde. Der Engpass ist die schiere Anzahl der möglichen Pfade, die die Roboter nehmen können; wenn die Anzahl der Roboter und die Größe der Karte zunehmen, wächst die Anzahl der Kombinationen so schnell an, dass der Computer keinen Platz mehr hat, um sie zu speichern. Trotz dieser Einschränkungen beweist die Arbeit, dass es möglich ist, einen digitalen Zwilling eines komplexen Robotersystems zu erstellen, der sowohl einfach genug ist, um geprüft zu werden, als auch genau genug, um vertrauenswürdig zu sein.

Diese Forschung bietet einen neuen Weg für die Entwicklung sicherer autonomer Systeme. Indem sie den Entwurf der Robotersoftware als einen Prozess behandeln, bei dem zuerst ein mathematisches Modell gebaut und verifiziert wird, können Ingenieure fatale Fehler identifizieren, bevor ein einziger Roboter gebaut oder eingesetzt wird. Das Team zeigte, dass es möglich ist, durch eine sorgfältige Abwägung zwischen dem Detailgrad des Modells und der Notwendigkeit der Recheneffizienz zu verifizieren, dass ein Multi-Roboter-System in der realen Welt sicher agieren wird. Ihre Arbeit legt nahe, dass die Zukunft der Robotik nicht nur darin liegt, intelligentere Maschinen zu bauen, sondern bessere Wege zu finden, um zu beweisen, dass diese Maschinen nicht versagen, wenn es darauf ankommt.