\section{Integration mit actionlib}\label{actionlib:integration}
Das hier verwendete Szenario entspricht einer etwas erweiterten Version des in \cref{konzept:uppaal_tor} verwendeten Beispiels, einem Garagen-Tor, welches präemptiert werden kann. Der implementierte Action-Server nimmt einen Boolean entgegen, der festlegt, ob das Tor geöffnet oder geschlossen werden soll, und gibt dann zufällig Feedback in Form eines Integers zurück, welcher die aktuelle Position des Tores repräsentiert. Dabei steht der Wert 0 für ein geschlossenes sowie 1000 für ein offenes Tor. Nach Abschluss des aktuellen Vorgangs wird der Status zurück zum Client übertragen. Dieser kann jedoch auch während der Ausführung das Wechseln des Ziels anfragen, woraufhin der Server das alte Ziel verwirft.\\
Das entsprechend erstellte Uppaal-Modell ist in \cref{integration:uppaal} zu sehen. Auffällig dabei sind Kanten denen die Channel \textit{fertig} und \textit{position} zugewiesen sind. Bei diesen wird vom System die aktuelle Position übermittelt. Dazu wird eine zufällige Zahl zwischen 0 und 1000 ausgewählt und zur Position addiert beziehungsweise subtrahiert. Außerdem wird garantiert, dass die Grenzen des Wertebereiches nicht überschritten werden.
\begin{figure}[h]
...
...
@@ -44,17 +44,18 @@ Die vollständige Implementierung des actionlib-Servers und -Clients sowie des v
\section{Cobot}
Mit der Möglichkeit zur Verwendung der actionlib kann nun ein tatsächliches Testszenario angegangen werden. Dazu wird zunächst die Aufgabe des Systems überprüft und formale Bedingungen zur Ausführung festgehalten. Dabei wurde der Cobot mehrfach simuliert sowie der Code der Implementierung überflogen, um einen Eindruck vom Systemverhalten zu bekommen.
\subsection{Formales Modell}
Als erstes lässt sich feststellen, dass der Cobot wartet bis er ein Signal von einem Drucksensor erhält woraufhin er zu arbeiten beginnt. Nach diesem Signal bewirken weitere Eingaben nichts, wodurch das System als Sequenz modelliert werden kann.
Als erstes lässt sich feststellen, dass der Cobot, nachdem er seine Startposition angenommen hat, wartet bis er ein Signal von einem Drucksensor erhält woraufhin er zu arbeiten beginnt. Nach diesem Signal bewirken weitere Eingaben nichts, wodurch das System als Sequenz modelliert werden kann.
Am Anfang wird eine Anzahl an Versuchen festgelegt, die der Roboter beim Aufheben und Hinstellen von Objekten durchführt, bevor die Ausführung als fehlgeschlagen gilt und das System herunterfährt. Dann bewegt sich der Roboter zur Flasche (wie das Glas in der Simulation als Block dargestellt) und hebt diese auf. Dabei ist wichtig, dass nach dem Aufnehmen die Flasche in einem aufrechten Zustand gehalten wird, um ein Verschütten der (in Simulation nicht vorhandenen) Flüssigkeit zu verhindern. Dann bewegt der Roboter die Flasche neben das Glas und beginnt sie in Richtung des Glases zu kippen. Dabei wird die Beschränkung der Orientierung temporär aufgehoben, bis das Wiederaufrichten durchgeführt wurde und die Flasche wieder an ihre ursprüngliche Position gebracht werden kann. Nach dem Abstellen der Flasche wird das Glas angehoben. Der Weg zum Glas unterliegt wieder keinerlei Beschränkungen, während bei angehobenem Glas dieses aufrecht gehalten werden muss, bis es auf der anderen Seite abgestellt wurde, woraufhin sich der Roboterarm wieder in seine Startposition begibt. Beim Abstellen ist ein zusätzlicher Fallback integriert, der dafür sorgt, dass beim Fehlschlagen des Platzierens am Ziel das Glas wieder an seine Ursprungsposition gebracht und neu aufgehoben wird. Dies geschieht wie die einzelnen Versuche auch so oft wie am Anfang festgelegt. Dabei wird im Modell keine Aktualisierung der Orientierungsbeschränkung vorgenommen, da diese nach dem Abstellen zwar entfernt, aber durch das sofortige Wiederaufheben unmittelbar wieder hinzugefügt wird.
Das aus diesen Angaben erstellte Modell ist in \cref{cobot:formales_modell} dargestellt.\\
Das aus diesen Angaben erstellte Modell ist in \cref{cobot:formales_modell_bild} dargestellt.\\
\begin{figure}[h]
\centering
\includegraphics[scale=.2]{./cobot1_v1.png}
\caption{Formales Modell des Cobots}
\label{cobot:formales_modell}
\label{cobot:formales_modell_bild}
\end{figure}
Zu Überprüfen ist neben der Reihenfolge der Ausführung auch die Qualität dieser. Zum einen sind die tatsächlichen Positionen von Glas und Flasche relevant, zum anderen müssen die Beschränkungen beim Bewegen der gefüllten Behältnisse abgeglichen werden. Die am Anfang der Systemausführung übergebene Anzahl an Versuchen zum Platzieren oder Aufheben ist in diesem Modell zwischen (einschließlich) 5 und 10 festgelegt, kann aber beliebig angepasst werden.
Zu Überprüfen ist neben der Reihenfolge der Ausführung auch die Qualität dieser. Zum einen sind die tatsächlichen Positionen von Glas und Flasche relevant, zum anderen müssen die Beschränkungen beim Bewegen der gefüllten Behältnisse abgeglichen werden.
Die am Anfang der Systemausführung übergebene Anzahl an Versuchen zum Platzieren oder Aufheben ist in diesem Modell zwischen (einschließlich) 5 und 10 festgelegt, kann aber beliebig angepasst werden.
Zeitliche Anforderungen an das System sind nicht gegeben, es ist jedoch wichtig dass das System terminiert, auch wenn die Ausführung nicht erfolgreich stattfindet und daher Heruntergefahren wird. Aus diesem Grund kann bereits jetzt eine Verifizierung dieses Modells stattfinden.
Der Uppaal Verifier kann mit der Anfrage \textit{A<> deadlock} (jeder Pfad führt zu einem Deadlock (= terminiert)) nicht umgehen. Daher werden 3 Anfragen verwendet, die diesem Zusammenhang entsprechen:
\begin{enumerate}
...
...
@@ -62,4 +63,12 @@ Der Uppaal Verifier kann mit der Anfrage \textit{A<> deadlock} (jeder Pfad führ
\item A[] ((Cobot.finished\_success or Cobot.shut\_down) imply deadlock)
\item A<> (Cobot.finished\_success or Cobot.shut\_down)
\end{enumerate}
1. bedeutet dass wenn ein Deadlock auftritt sich der Cobot immer im Zustand \textit{finished\_success} oder \textit{shut\_down} befindet. 2. kehrt diese Aussage um und sorgt so zusammen mit 1. für einen genau-dann-wenn Zusammenhang zwischen einem Deadlock und den besagten Zuständen. Schließlich wird mit 3. abgefragt, ob jeder Pfad (nach endlicher Zeit) zu \textit{finished\_success} oder \textit{shut\_down} führt. Diese Anfragen werden alle als wahr ausgewertet, wodurch klar ist, dass das Modell immer terminiert.
\ No newline at end of file
1. bedeutet dass wenn ein Deadlock auftritt sich der Cobot immer im Zustand \textit{finished\_success} oder \textit{shut\_down} befindet. 2. kehrt diese Aussage um und sorgt so zusammen mit 1. für einen genau-dann-wenn Zusammenhang zwischen einem Deadlock und den besagten Zuständen. Schließlich wird mit 3. abgefragt, ob jeder Pfad (nach endlicher Zeit) zu \textit{finished\_success} oder \textit{shut\_down} führt. Diese Anfragen werden alle zu wahr evaluiert, wodurch klar ist, dass das Modell immer terminiert. Hier ist darauf hinzuweisen, dass für die Validierung ein weiteres Modell im System von Uppaal hinzugefügt werden muss, welches lediglich aus einem Knoten besteht, der sämtliche Channel aktiviert.
\subsection{Topics, Adapter und Modellanpassungen}
Als nächstes müssen ROS-Topics identifiziert werden, die die benötigten Informationen transportieren. Dazu eignet sich das Tool \textit{rostopic}\footnote{\url{http://wiki.ros.org/rostopic}}, mit welchem sich alle aktiven Topics auflisten und deren Nachrichten abhören lassen.\\
Für den initialen Impuls des Drucksensors ist bereits ein Topic vorhanden und wird vom Cobot verwendet, kann also auch als Output vom Adapter benutzt werden. Dabei lässt sich direkt die Anzahl an erneuten Versuchen vor einem Abbruch übertragen, da diese in einer Konfigurationsdatei des Systems festgelegt wird und daher in der Konfigurationsphase des Adapters ausgelesen werden kann. In dieser Konfigurationsdatei sind auch die Startposition der Flasche sowie die Start- und Zielposition des Glases hinterlegt, sodass auch diese im Adapter gehalten werden können. Das Speichern sowie Vergleichen der Positionen von Flasche und Glas muss im Adapter erfolgen, da Uppaal TRON keine Gleitkommazahlen beim Testen unterstützt. Gazebo veröffentlicht regelmäßig über \textit{/gazebo/link\_states} und \textit{/gazebo/model\_states} die aktuellen Positionen in der Simulationsmodelle, welche folglich mit den Gewünschten im Adapter verglichen und das Ergebnis als Boolean an Uppaal weitergegeben werden kann. Für die Verwendung mit TRON müssen auch diese Booleans in Uppaal als Integer deklariert werden, was allerdings kein Problem darstellt, da innerhalb der Modelle Vergleiche mit \textit{true} oder \textit{false} möglich sind und vom Adapter einfach 0 oder 1 übertragen werden kann. Diese Aspekte schränken zwar das Modell ein und machen eine Auslagerung von Logik in den Adapter notwendig, sorgen aber gleichzeitig dafür, dass das Modell abstrakt bleibt und nicht zu detailliert wird.\\
Für das Platzieren und Aufheben von Objekten sowie die Bewegungsplanung wird von ROS beziehungsweise MoveIt\footnote{\url{https://moveit.ros.org/}} (Framework unter anderem zur Bewegungsplanung) die actionlib verwendet, sodass sich die dort verwendeten Topics \textit{/pickup/result} und \textit{/place/result} zum Testen eignen. Die dort benutzten Nachrichten besitzen einen eigenen Typ von Fehlercode, durch welchen an TRON der Erfolg oder das Fehlschlagen einer Aktion gemeldet werden kann. Um das Modell eindeutiger zu gestalten, wurde die Variable \textit{success} durch je einen weiteren Channel für einen Fehlschlag ersetzt.\\
Für das Verfolgen von Bewegungen, welche bei der Bewegung zur Flasche, zum Glas und beim Einfüllen relevant sind wird das Topic \textit{/follow\_joint\_trajectory/result} des \textit{position\_joint\_trajectory\_controller} genutzt. Die restlichen Bewegungen (bis auf die zur Startposition des Roboters) sind als Teilvorgänge des Platzierens und Aufhebens anzusehen, da sie an sich keine essentielle Funktion des Cobots darstellen und sind daher nicht explizit im Modell angegeben.\\
Da logischerweise auch das Platzieren und Aufheben von Objekten Bewegungen des Arms beinhaltet, müssen bei entsprechenden Knoten im Modell zusätzliche Kanten eingefügt werden, die zum Knoten selbst zurückführen und dabei eine (nicht-) erfolgreiche Ausführung durch einen Channel abfragen. Diese Kanten sorgen dafür, dass die in \cref{cobot:formales_modell} beschriebene Validierung nicht ohne Weiteres so verwendet werden kann, da nun Endlosschleifen möglich sind. Dies könnte beispielsweise durch einen Zähler mit einer (unrealistisch hohen) maximalen Anzahl an Bewegungen realisiert sein. Für die Orientierungsbeschränkung beim Bewegen kommt nur das Topic \textit{/move\_group/goal} in Frage, da nur in diesen Nachrichten eine solche Beschränkung übergeben wird und eine Überprüfung von bereits berechneten Bewegungsbahnen aufwendig wäre. Anzumerken ist hier, dass das Einhalten einer gegebenen Beschränkung genauso wie das Aufheben oder die Bewegungen selbst nicht Teil des Tests darstellen, sondern auf den niedrigeren Testebenen (Unit-Tests oder Integrations-Tests) getestet werden müssen. Daher wird hier nur überprüft, ob eine Orientierungsbeschränkung festgelegt ist. Auch hier wäre ein Abgleich mit einer gewünschten Orientierung innerhalb des Adapters möglich, diese ist jedoch hier nicht zwingend nötig, da eine falsche Orientierung bei einer Simulation extrem auffällig wäre und daher hier ausgeschlossen werden kann. Bei genauerer Analyse des Cobots sind weitere Bewegungsbeschränkungen wie etwa bei der Beschleunigung aufgefallen, diese würden dem gleichen Schema folgen.\\
Da innerhalb von jedem Modell-Zustand Nachrichten an \textit{/move\_group/goal} gesendet werden, für das Testen allerdings nur eine Änderung bei der Orientierungsbeschränkung relevant ist, wird in das Uppaal-System ein weiteres Modell integriert, welches Outputs an den entsprechenden Channel entgegennimmt, wenn keine Änderung erfolgte. Das gleiche Prinzip wird auf den Channel angewandt, welcher den Drucksensor repräsentiert.
