Kurzfassung

Die Erstellung von Software für kooperierende Teams mobiler Roboter stellt hohe Anforderungen. Zum einen ist eine Reaktion in Echtzeit zu garantieren zum anderen erhöht die Kooperation von Agenten die Komplexität. Formale Methoden zu Entwurf und Verifikation von Multiagenten-Systemen existieren bisher kaum. Im Rahmen unseres Projekts entwickeln wir daher ein Verfahren zum formalen Software-Entwurf solcher Systeme. Diese Entwürfe sind in unserem Ansatz direkt ausführbare Spezifikationen....Die Erstellung von Software für kooperierende Teams mobiler Roboter stellt hohe Anforderungen. Zum einen ist eine Reaktion in Echtzeit zu garantieren zum anderen erhöht die Kooperation von Agenten die Komplexität. Formale Methoden zu Entwurf und Verifikation von Multiagenten-Systemen existieren bisher kaum. Im Rahmen unseres Projekts entwickeln wir daher ein Verfahren zum formalen Software-Entwurf solcher Systeme. Diese Entwürfe sind in unserem Ansatz direkt ausführbare Spezifikationen. Hierzu werden Mittel aus der Deduktion und Logikprogrammierung (Prolog) und der Unified Modeling Language (UML), speziell Statecharts, eingesetzt. Damit ist nun in einem weiteren Schritt die Analyse und Verifikation von Multiagenten-Systemen durchführbar, indem Temporal- bzw. dynamische Logiken und Methoden aus dem Model Checking für den hier vorgesehenen Zweck (weiter)entwickelt werden. Insgesamt ist so ein Systementwurf möglich, der in Systeme mobiler Roboter integriert werden kann. Dies wird konkret für die RoboCup-Simulation sowie für echte Roboter vom Typ Sony Aibo durchgeführt.» weiterlesen» einklappen