Dieses Vorhaben befasst sich mit der Entwicklung und
Erprobung neuer Ansätze zur Spezifikation und Verifikation
sicheren kooperativen Verhaltens autonomer Agenten,
etwa Roboter oder autonom fahrender Autos. Nachdem in
früheren Vorhaben allgemeine Fragestellungen untersucht
wurden, nämlich• Überdeckungskriterien für das gesamte kooperative
Verhalten und zugehörige Testfallgenerierung zur Erzielung
dieser Kriterien (s. R3-COP) sowie
• Bewertung der Zuverlässigkeit kooperativen Verhaltens und
zugehörige Testfallgenerierung zur Durchführung
statistischen Testens (s. R5-COP)
wendet sich dieses weitere Vorhaben an die Untersuchung
besonderer Ausprägungen des potentiellen kooperativen
Verhaltens, etwa um
• das Auftreten vorgegebener sicherheitskritischer
Szenarien nach Möglichkeit von vornherein auszuschließen,
• die Möglichkeit eines solchen Auftretens durch dedizierte
Testfälle vor dem Betrieb aufzuspüren und durch angemessene
Korrektur künftig zu eliminieren,
• die rechtzeitige Erkennung potentiell kritischer Zustände
im Betrieb zu unterstützen und passende Reaktionen auf
vordefinierten Rückfallebenen automatisch einzuleiten.
Teilprojekt 1: Verifikation bzw. Falsifikation
sicherheitsrelevanter Eigenschaften kooperativen
Verhaltens
In diesem Teilprojekt werden modellbasierte Ansätze zur
Erkennung von Verletzungen von Kooperations- bzw.
Koexistenzeigenschaften untersucht. Hierzu wurde folgendes
beispielhafte Agentensystem betrachtet, das aus 2 Robotern
besteht, die Transportmissionen autonom übernehmen; hierbei
ist jede Transportmission definiert durch
• eine zu transportierende Menge nicht weiter
spezifizierten Materials und
• eine Missionspriorität.
Die Transportmission gilt genau dann als erfolgreich
abgeschlossen, wenn das zu transportierende Material an der
einzig vorhandenen Entladestation entladen wurde.
Selbstverständlich dürfen Entladevorgänge nicht zur
Überladung der Entladestation führen. Zur Gewährleistung
dieser sicherheitsrelevanten Eigenschaft hat jeder Roboter
vor Auslösung der Entladung zu überprüfen,
• ob die eigene Entladung zu einer Überladung der Station
führen kann und
• ob ein auf einem angrenzenden Parksegment stehender
Roboter mit einer höher priorisierten Mission ebenfalls die
Möglichkeit der Entladung überprüft.
Dann und nur dann, wenn beide Bedingungen nicht erfüllt
werden, wird die Entladung initiiert.
Um obige Kriterien zu evaluieren erfährt jeder Roboter
• über entsprechende Sensoren die aktuelle Kapazität der
Entladestation und
• über ein Display die Priorität der Mission eines
benachbarten Roboters.
Die auf die Kooperation der beiden Roboter begrenzte
Anwendung soll anschließend auf die Koexistenz von 3
Robotern erweitert werden. Es war deshalb zu analysieren,
inwieweit bei unveränderter Verhaltensspezifikation diese
Erweiterung zu einer Verletzung der betrachteten
Sicherheitseigenschaft führen kann.
Hierzu wurde der im abgeschlossenen Projekt „Modellbasierte
Verifikation relevanter Eigenschaften komplexer
Softwaresysteme mittels heuristischer Testverfahren“
entwickelte Ansatz zur Falsifikation universeller
temporallogischer CTL-Formeln eingesetzt. Dieser Ansatz
erforderte zunächst die Modellierung des Gesamtverhaltens
durch eine erweiterte endliche Zustandsmaschine, die als
Kreuzprodukt von 4 einzelnen erweiterten Zustandsmaschinen
(jeweils eine für jeden der 3 Roboter sowie eine vierte für
die Entladestation) konstruiert wurde. Auf dieser Basis
konnte der entwickelte Ansatz Eingangsdaten finden, die zu
einem betrieblichen Szenario führen, in dem die
Sicherheitseigenschaft verletzt wird. Somit konnte
nachgewiesen werden, dass die Erweiterung des
Agentensystems eine Anpassung der ursprünglichen
Verhaltensspezifikation erforderlich macht.
Teilprojekt 2: Selbstreflektierende Anpassung der
Autonomiegrade kooperierender Agenten
Im Vergleich zu traditionellen zentralisierten Systemen
stellen kooperierende autonome Agenten-Systeme bekanntlich
zusätzliche Herausforderungen: zum einen können sich
Aktionen eines Agenten auf Nachfolgeentscheidungen weiterer
Agenten auswirken; zum anderen sind die Agenten meist nicht
in der Lage, die Aktionen der anderen Agenten
vorauszusagen. Eine systematische, optimale und
sicherheitsgerichtete Entscheidungsfindung mag daher u. U.
(etwa infolge nur unvollständig verfügbarer Informationen)
nicht möglich sein, wodurch das Auftreten kritischer
Situationen nicht im Voraus ausgeschlossen werden kann.
Im Rahmen dieses Forschungsprojektes wird untersucht,
inwieweit kritische Situationen sich dadurch vermeiden bzw.
reduzieren lassen, dass die einzelnen Agenten zeitweise
einen Teil ihrer Autonomie an eine zentrale Instanz
abgeben. Diese zentrale Instanz überwacht die Aktionen der
einzelnen Agenten; darauf basierend, muss sie in der Lage
sein, das potentielle Auftreten einer kritischen Situation
zu erkennen und als Gegenmaßnahme in die Autonomie der
Agenten einzugreifen, indem sie diesen die als nächstes
auszuführende Aktion vorgibt (um somit die kritische
Situation zu vermeiden).
In einem ersten Schritt wurde untersucht, wie die internen
Zustände des Agentensystems in Abhängigkeit vom Bedarf
einer angemessenen Intervention seitens der zentralen
Instanz, sowie von der Art der geforderten Intervention
klassifiziert werden können.