diff --git a/sections/evaluation.tex b/sections/evaluation.tex
index 910a6319d6fecbde12b88685438bcd54256f87f8..cdea9231a76a02d34bb9e098482ed1e24c7565c9 100644
--- a/sections/evaluation.tex
+++ b/sections/evaluation.tex
@@ -3,20 +3,20 @@ Nach der Anwendung von Uppaal mit TRON lässt sich das verwendete Konzept evalui
 
 \section{Anforderungen}
 \subsection{Abdeckung und Vollständigkeit}
-Die Abdeckung der Testmethodik ist unter anderem durch das verwendetet Modell festgelegt. Da dieses relativ abstrakt gehalten wird, muss auch der Adapter zur Abdeckung beitragen. Gazebo ist als Simulation zwar äußerst hilfreich, bietet aber nur begrenzt Möglichkeiten zum Modellieren nicht-funktionaler Eigenschaften, die im Fallbeispiel dieser Arbeit jedoch nicht benötigt wurden. Funktionale Anforderungen sowie Interaktionen und die Umwelt lassen sich jedoch erfassen, sofern entsprechende Modelle für eine Simulation vorliegen.
+Die Abdeckung der Testmethodik ist unter anderem durch das verwendete Modell festgelegt. Da dieses relativ abstrakt gehalten wird, muss auch der Adapter zur Abdeckung beitragen. Gazebo ist als Simulation zwar äußerst hilfreich, bietet aber nur begrenzt Möglichkeiten zum Modellieren nicht-funktionaler Eigenschaften, die im Fallbeispiel dieser Arbeit jedoch nicht benötigt wurden. Funktionale Anforderungen sowie Interaktionen und die Umwelt lassen sich jedoch erfassen, sofern entsprechende Modelle für eine Simulation vorliegen.
 \subsection{Reproduzierbarkeit}
 Ein wiederholtes Ausführen der Tests hat im Fallbeispiel funktioniert. Das Modell beschreibt aufgrund seiner Abstraktheit die Testfälle eindeutig, wobei im Adapter darauf geachtet werden muss, dass die Übersetzung ebenso eindeutig stattfindet, damit der Testfall wiederholt werden kann. Damit sind durch Modell und Adapter alle Testfälle dokumentiert.
-Auch hier ist die Simulation und die damit einhergehende korrekte Modellierung als wichtigster Faktor anzusehen. Da wie in jeder Simulation auch Gazebo bei jeder Ausführung minimale Abweichungen aufweist, kann keine absolute Eindeutigkeit gewährleistet werden. Im Fallbeispiel wurde gezeigt, dass selbst kleine Abweichungen größere Veränderungen bewirken können, in diesem Fall ob etwa die Flasche herunterfällt oder nicht. 
+Auch hier ist die Simulation und die damit einhergehende korrekte Modellierung als wichtigster Faktor anzusehen. Da wie in jeder Simulation auch Gazebo bei jeder Ausführung minimale Abweichungen aufweist, kann keine absolute Eindeutigkeit gewährleistet werden. Im Fallbeispiel wurde gezeigt, dass selbst kleine Abweichungen größere Veränderungen bewirken können, in diesem Fall, ob etwa die Flasche herunterfällt oder nicht. 
 \subsection{Skalierbarkeit}
 Diese Form der Testausführung ist ohne Probleme skalierbar, es kann eine beliebige Anzahl an Tests ausgeführt werden, wobei die Tests jedoch je nach System viel Zeit in Anspruch nehmen können. Dies war im Fallbeispiel primär den Berechnungen von ROS/MoveIt und der Geschwindigkeit der Simulation zuzuschreiben. Diese konnte nur mit einem Tempo von 20 Prozent der Echtzeit ausgeführt werden, da sonst praktisch jede Ausführung fehlschlug, da die Greifoperation des Roboters nicht darauf ausgelegt ist.
 \subsection{Aufwand}
-Wie erwartet ist ein erhöhter Aufwand bei der initialen Implementierung von modell-basiertem Testen nötig. Obwohl der Code für den Cobot nur etwa 500 Zeilen umfasst, beinhaltet das Modell über 30 Zustände und dementsprechend viele Übergänge. Die Entwicklung des formalen Modells erwies sich dabei als relativ einfach, während die Konfiguration des Adapters sowie die Anpassung des Modells an die Topics von ROS deutlich schwieriger war. Dies ist zum einen darauf zurückzuführen, dass Uppaal ursprünglich für die Verifikation von Modellen und nicht zum modell-basierten Testen entwickelt wurde, zum anderen wird Uppaal und TRON nicht mehr aktiv weiterentwickelt und ist relativ alt. Einen weiteren erschwerenden Faktor stellt die schlechte Dokumentation der Tools dar. Weiterhin werden komplexe Berechnungen innerhalb von Uppaal aufgrund der begrenzten Syntax nicht möglich sein, und TRON unterstützt lediglich 32-Bit-Integer-Variablen, was offensichtlich einen Nachteil darstellt und dazu führt das Logik in den Adapter ausgelagert werden muss.
+Wie erwartet ist ein erhöhter Aufwand bei der initialen Implementierung von modell-basiertem Testen nötig. Obwohl der Code für den Cobot nur etwa 500 Zeilen umfasst, beinhaltet das Modell über 30 Zustände und dementsprechend viele Übergänge. Die Entwicklung des formalen Modells erwies sich dabei als relativ einfach, während die Konfiguration des Adapters sowie die Anpassung des Modells an die Topics von ROS deutlich schwieriger war. Dies ist zum einen darauf zurückzuführen, dass Uppaal ursprünglich für die Verifikation von Modellen und nicht zum modell-basierten Testen entwickelt wurde, zum anderen wird Uppaal und TRON nicht mehr aktiv weiterentwickelt und ist relativ alt. Einen weiteren erschwerenden Faktor stellt die schlechte Dokumentation der Tools dar. Weiterhin werden komplexe Berechnungen innerhalb von Uppaal aufgrund der begrenzten Syntax nicht möglich sein, und TRON unterstützt lediglich 32-Bit-Integer-Variablen, was offensichtlich einen Nachteil darstellt und dazu führt, dass Logik in den Adapter ausgelagert werden muss.
 Außerdem müssen die neben dem System laufenden ROS-Topics analysiert und die gewünschten Informationen innerhalb dieser gefunden werden, um sie im Adapter hinzuzufügen. Daher kann diese Testmethode auch nicht ohne Weiteres auf beispielsweise HIL-Simulationen übertragen werden, wenn Informationen der Umwelt benötigt werden. Positiv anzumerken ist jedoch, dass neu implementierte Änderungen des Systems einfach zu testen sind, wenn dafür gewünschte Informationen bereits durch den Adapter übertragen werden.\\
 Bezüglich der Ausführbarkeit ist festzuhalten, dass eine einfache Automatisierbarkeit gegeben ist. roslaunch-Dateien sowie TRON können einfach aus einem Skript gestartet werden und die Ausführung ohne GUI ist mit Gazebo problemlos umsetzbar. Die Parallelisierbarkeit ist jedoch durch ROS selbst stark eingeschränkt, da es nicht möglich ist mehrere Nodes mit gleichem Namen parallel laufen zu lassen. Dafür wären mehrere Systeme nötig oder es könnte auf virtuellen Maschinen gearbeitet werden. 
 \subsection{Analysierbarkeit}
 Uppaal und TRON selbst bieten praktisch keine Möglichkeit zur automatisierten Analyse von ausgeführten Testfällen. Dennoch ist eine gute Analysierbarkeit gegeben, wenn alle dafür nötigen Variablen im Uppaal-Modell vorhanden sind. Die von TRON erstellten Log-Dateien können in ihrer Ausführlichkeit angepasst werden und dann durch einfache Batch-Skripts durchsucht und wichtige Informationen zusammengetragen werden. Dies ermöglichte im Fallbeispiel das Finden möglicher Gründe in jedem Fehlerfall, sorgte aber auch für einen relativ hohen Speicherbedarf, da die Log-Datei beinahe jeder Testausführung über 20MB in Anspruch nahm.
 \subsection{Akkuratheit}
-Die Akkuratheit ist wieder zu einem Großteil durch die Simulation bestimmt. Gazebo ist dabei wie in \cref{konzept:simulation} beschrieben verglichen mit anderen Simulationen als gut einzustufen. Probleme mit zum Beispiel weichen Materialien oder Flüssigkeiten sind jedoch vorhanden, sodass in diesen Fällen eventuell eine andere Simulation in Betracht gezogen werden sollte.\\
+Die Akkuratheit ist wieder zu einem Großteil durch die Simulation bestimmt. Gazebo ist dabei wie in \cref{konzept:simulation} beschrieben, verglichen mit anderen Simulationen, als gut einzustufen. Probleme mit zum Beispiel weichen Materialien oder Flüssigkeiten sind jedoch vorhanden, sodass in diesen Fällen eventuell eine andere Simulation in Betracht gezogen werden sollte.\\
 Das echte Einsatzumfeld des Cobots ist mir nicht bekannt, daher kann ich dazu wenige Aussagen treffen. Offensichtlich ist jedoch, dass die Objekte in der verwendeten Simulation Quader waren, was echte Gläser und Flaschen jedoch selten sind. Neben der Simulation lässt sich also nur erneut darauf hinweisen, dass Modelle möglichst präzise den Gegebenheiten der echten Welt folgen sollten.
 \subsection{Sicherheit}
 Die Sicherheit ist durch die Simulation vollkommen gewährleistet. Eine Überwachbarkeit des Testablaufs ist somit nicht nötig und würde lediglich die Automatisierbarkeit der Testausführung einschränken. Wegen der in \cref{grundlagen:simulationen:hil} aufgezählten Gründe sind HIL-Simulationen im Fallbeispiel nicht sinnvoll gewesen und ließe sich mit der vorgestellten Methode wie bereits erwähnt auch nur schwer implementieren. 
\ No newline at end of file
diff --git a/sections/fallbeispiel.tex b/sections/fallbeispiel.tex
index 33d50ed4053ee592990ed2fb501521b71876be3e..5f3cd816d0af7f7755fff25df3de04410f047501 100644
--- a/sections/fallbeispiel.tex
+++ b/sections/fallbeispiel.tex
@@ -21,7 +21,7 @@ Das entsprechend erstellte Uppaal-Modell ist in \cref{integration:uppaal} zu seh
 	\caption{Testmodell des Action-Servers}
 	\label{integration:uppaal}
 \end{figure}
-Der Einsatz des Adapters erfolgt unter Verwendung von eigens für die Nachrichtentypen implementierten Callbacks statt der Zuweisung von Bytes. Dadurch können andere Bestandteile des Action-Protokolls wie die Header vernachlässigt werden. Weiterhin ist zu beachten, dass im Adapter die Nachrichten verwendet werden, die \textbf{Action} im Namen tragen (z.B. TriggerActionGoal, nicht TriggerGoal). Diese Nachrichten beinhalten neben den Daten auch Header- und Statusinformationen und müssen verwendet werden, wenn der Adapter selbst weder Client noch Server des Systems ist, sondern ersteren nur emuliert oder die Kommunikation beider Parteien abhört. Eine Implementierung des Adapters, welcher selbst einen Client darstellt wäre allerdings auch möglich. Die Namen der Topics sind aus dem Namen des Servers (wird bei Konstruktion übergeben) und dem Inhalt der Nachricht zusammengesetzt und können daher ohne Probleme verwendet werden. Die (nicht vollständige) Konfigurationsphase für den Adapter des in \cref{integration:uppaal} gezeigten Modells sieht wie folgt aus:
+Der Einsatz des Adapters erfolgt unter Verwendung von eigens für die Nachrichtentypen implementierten Callbacks statt der Zuweisung von Bytes. Dadurch können andere Bestandteile des Action-Protokolls wie die Header vernachlässigt werden. Weiterhin ist zu beachten, dass im Adapter die Nachrichten verwendet werden, die \textbf{Action} im Namen tragen (z.B. TriggerActionGoal, nicht TriggerGoal). Diese Nachrichten beinhalten neben den Daten auch Header- und Statusinformationen und müssen verwendet werden, wenn der Adapter selbst weder Client noch Server des Systems ist, sondern ersteren nur emuliert oder die Kommunikation beider Parteien abhört. Eine Implementierung des Adapters, welcher selbst einen Client darstellt, wäre allerdings auch möglich. Die Namen der Topics sind aus dem Namen des Servers (wird bei Konstruktion übergeben) und dem Inhalt der Nachricht zusammengesetzt und können daher ohne Probleme verwendet werden. Die (nicht vollständige) Konfigurationsphase für den Adapter des in \cref{integration:uppaal} gezeigten Modells sieht wie folgt aus:
 \begin{lstlisting}[tabsize=1]
 	// oeffnen und schliessen stellt jeweils ein Ziel dar
 	Mapping map = adapter.createMapping("/garage_server/goal", "oeffnen", true);
@@ -58,7 +58,7 @@ 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}\label{cobot:formales_modell}
-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.
+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_bild} dargestellt.\\
 \begin{figure}[h]
@@ -67,9 +67,9 @@ Das aus diesen Angaben erstellte Modell ist in \cref{cobot:formales_modell_bild}
 	\caption{Formales Modell des Cobots}
 	\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. 
+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.
+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}
 	\item A[] (deadlock imply (Cobot.finished\_success or Cobot.shut\_down))
@@ -79,10 +79,10 @@ Der Uppaal Verifier kann mit der Anfrage \textit{A<> deadlock} (jeder Pfad führ
 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 verglichen und die Ergebnisse als Differenz an TRON weitergegeben werden können. Anzumerken ist, dass für jede Differenz ein eigener Channel in Uppaal existiert. Dies ist nötig da eine einzelne Kante, welche alle Werte aktualisiert, dazu führen würde, dass Uppaal alle Kombinationen dieser als mögliche Outputs berechnet, was zu exponentiell erhöhter Rechenzeit führt (\textit{State Explosion}). Die Simulationssoftware beginnt vor dem Initialisieren der Objekte bereits mit dem Veröffentlichen von Nachrichten, sodass vom Adapter mit dem Weitergeben an TRON gewartet wird, bis die Objekte initialisiert wurden. Außerdem wird beim Berechnen der Orientierungsabweichung eine Drehung um die Z-Achse (senkrecht zur Szene) ignoriert, da diese für ein Aufrechtstehen nicht relevant ist.
+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 verglichen und die Ergebnisse als Differenz an TRON weitergegeben werden können. Anzumerken ist, dass für jede Differenz ein eigener Channel in Uppaal existiert. Dies ist nötig da eine einzelne Kante, welche alle Werte aktualisiert, dazu führen würde, dass Uppaal alle Kombinationen dieser als mögliche Outputs berechnet, was zu exponentiell erhöhter Rechenzeit führt (\textit{State Explosion}). Die Simulationssoftware beginnt vor dem Initialisieren der Objekte bereits mit dem Veröffentlichen von Nachrichten, sodass vom Adapter mit dem Weitergeben an TRON gewartet wird, bis die Objekte initialisiert wurden. Außerdem wird beim Berechnen der Orientierungsabweichung eine Drehung um die z-Achse (senkrecht zur Szene) ignoriert, da diese für ein Aufrechtstehen nicht relevant ist.
 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.
-Um die Positionen der Objekte im Uppaal-System festzuhalten wurde je ein separates Modell, zu sehen in \cref{cobot:positionen_modell_bild} (analog für Flasche) hinzugefügt, welches durch das Topic \textit{/gazebo/link\_states} aktualisiert wird und globale Variablen setzt, die das Modell des Cobots verwendet, um festzustellen ob sich das Objekt an der richtigen Position befindet. Dabei musste auch darauf geachtet werden, dass fehlgeschlagene Versuche passend dargestellt sind, es existiert also für jede Zustand eine Kante zu seinem Vorgänger. Zum Startzustand kann allerdings nur zurückgegangen werden, wenn das Objekt nicht gleichzeitig im Endzustand ist, um ein fälschliches Zurückgehen zu verhindern. Es existiert keine Kante direkt vom Start- zum Endzustand, sodass das Objekt mindestens einmal seine Position verlassen muss.\\
+Um die Positionen der Objekte im Uppaal-System festzuhalten wurde je ein separates Modell, zu sehen in \cref{cobot:positionen_modell_bild} (analog für Flasche) hinzugefügt, welches durch das Topic \textit{/gazebo/link\_states} aktualisiert wird und globale Variablen setzt, die das Modell des Cobots verwendet, um festzustellen, ob sich das Objekt an der richtigen Position befindet. Dabei musste auch darauf geachtet werden, dass fehlgeschlagene Versuche passend dargestellt sind, es existiert also für jeden Zustand eine Kante zu seinem Vorgänger. Zum Startzustand kann allerdings nur zurückgegangen werden, wenn das Objekt nicht gleichzeitig im Endzustand ist, um ein fälschliches Zurückgehen zu verhindern. Es existiert keine Kante direkt vom Start- zum Endzustand, sodass das Objekt mindestens einmal seine Position verlassen muss.\\
 \begin{figure}[h]
 	\centering
 	\includegraphics[scale=.22]{./cobot1_positionen_modell.png}
@@ -90,10 +90,10 @@ Um die Positionen der Objekte im Uppaal-System festzuhalten wurde je ein separat
 	\label{cobot:positionen_modell_bild}
 \end{figure}
 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. Außerdem ist eine Bewegung nach dem Fehlschlagen des Platzierens vom Glas eingefügt worden, da diese hier hinzugefügt wurde, um Abstand zu gewinnen, bevor ein weiterer Versuch ausgeführt wird.
-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.
+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. Außerdem ist eine Bewegung nach dem Fehlschlagen des Platzierens vom Glas eingefügt worden, da diese hier hinzugefügt wurde, um Abstand zu gewinnen, bevor ein weiterer Versuch ausgeführt wird.
+Die restlichen Bewegungen (bis auf die zur Startposition des Roboters) sind als Teilvorgänge des Platzierens und Aufhebens anzusehen, da sie an sich keine essenzielle 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. Dies ist nötig, da TRON sonst einen Fehler aufgrund von nicht erwartetem Output ausgibt. 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 und eine Deklarierung von allen Channels als \textit{urgent} realisiert sein, wird jedoch hier nicht vorgenommen, um das Modell übersichtlicher zu halten.\\
-Für die Orientierungsbeschränkung beim Bewegen kommen nur Topics die ein Ziel festlegen (\textit{/move\_group/goal}, \textit{/pickup/goal}, \textit{/place/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.\\
+Für die Orientierungsbeschränkung beim Bewegen kommen nur Topics, die ein Ziel festlegen (\textit{/move\_group/goal}, \textit{/pickup/goal}, \textit{/place/goal}) infrage, 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{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 ebenfalls auf andere Channel angewandt, welche zu jedem Zeitpunkt aktiviert werden können.\\
 Das endgültige Testmodell für den Cobot (ohne die zusätzlich verwendeten Modelle, siehe Anhang) ist in \cref{cobot:modell_bild} abgebildet.
 \begin{figure}[h]
@@ -104,20 +104,21 @@ Das endgültige Testmodell für den Cobot (ohne die zusätzlich verwendeten Mode
 \end{figure}
 
 \subsection{Testausführung}\label{cobot:testausfuehrung}
-Zur Ausführung wurde ein simples Bash-Script geschrieben, welches zuerst einen build für das Projekt ausführt und dann eine beliebige Anzahl an Tests startet. Dabei werden die Tests sequentiell ausgeführt, indem zunächst TRON und schließlich eine roslaunch-Datei gestartet wird. In dieser Datei ist das Starten der Simulation und nötigen ros-Nodes, inklusive des Test-Adapters, geregelt. Mittels dem Argument \textit{gui} (und dem Wert \textit{false}) wird Gazebo \textit{headless} gestartet, sodass die Tests problemlos im Hintergrund ablaufen können. TRON ermöglicht das festhalten der Ergebnisse in Textdateien (siehe \cite{TronManual}). Das Tool eine Testausführung ab, wenn ein Fehler auftritt oder der im Adapter festgelegte Timeout abläuft. Da das System nicht unendlich läuft und ein Erfolg mittels der Zustände \textit{finished\_success} und \textit{shut\_down} kodiert ist, kann ein erfolgreicher Test vor dem Timeout beendet werden. Dazu wurde ein weiterer Channel \textit{test\_done} deklariert, welcher beim Übergang in diese Zustände auslöst und als Input dient, auf welchen der Adapter mit einer von TRON nicht erwarteten Ausgabe reagiert (Channel \textit{intentional\_fail}). Dadurch können bei gleichbleibender Zeit deutlich mehr Tests durchgeführt werden, wenn in Kauf genommen wird, dass nach dem im Modell spezifizierten Verhalten keine weitere Überprüfung stattfindet.
+Zur Ausführung wurde ein simples Bash-Script geschrieben, welches zuerst einen build für das Projekt ausführt und dann eine beliebige Anzahl an Tests startet. Dabei werden die Tests sequentiell ausgeführt, indem zunächst TRON und schließlich eine roslaunch-Datei gestartet wird. In dieser Datei ist das Starten der Simulation und nötigen ros-Nodes, inklusive des Test-Adapters, geregelt. Mittels dem Argument \textit{gui} (und dem Wert \textit{false}) wird Gazebo \textit{headless} gestartet, sodass die Tests problemlos im Hintergrund ablaufen können. TRON ermöglicht das Festhalten der Ergebnisse in Textdateien (siehe \cite{TronManual}). Das Tool eine Testausführung ab, wenn ein Fehler auftritt oder der im Adapter festgelegte Timeout abläuft. Da das System nicht unendlich läuft und ein Erfolg mittels der Zustände \textit{finished\_success} und \textit{shut\_down} kodiert ist, kann ein erfolgreicher Test vor dem Timeout beendet werden. Dazu wurde ein weiterer Channel \textit{test\_done} deklariert, welcher beim Übergang in diese Zustände auslöst und als Input dient, auf welchen der Adapter mit einer von TRON nicht erwarteten Ausgabe reagiert (Channel \textit{intentional\_fail}). Dadurch können bei gleichbleibender Zeit deutlich mehr Tests durchgeführt werden, wenn in Kauf genommen wird, dass nach dem im Modell spezifizierten Verhalten keine weitere Überprüfung stattfindet.
 
 \subsection{Testergebnisse}
-Die in \cref{cobot:testausfuehrung} beschriebene Methode wurde angewandt um das Modell 100 mal auszuführen und Log-Dateien anzulegen. Folglich konnte erneut ein Bash-Skript genutzt werden, um die Testergebnisse zu analysieren. Da lediglich ein Zustand erreicht werden muss, um den Test erfolgreich abzuschließen, reicht es in diesem Fall nach einem entsprechenden Zustand im Log zu suchen. Wird kein Endzustand erreicht, so kann der Testfall als fehlgeschlagen eingestuft und weiter untersucht werden.\\
+Die in \cref{cobot:testausfuehrung} beschriebene Methode wurde angewandt, um das Modell 100 mal auszuführen und Log-Dateien anzulegen. Folglich konnte erneut ein Bash-Skript genutzt werden, um die Testergebnisse zu analysieren. Da lediglich ein Zustand erreicht werden muss, um den Test erfolgreich abzuschließen, reicht es in diesem Fall nach einem entsprechenden Zustand im Log zu suchen. Wird kein Endzustand erreicht, so kann der Testfall als fehlgeschlagen eingestuft und weiter untersucht werden.\\
 In 46 der 100 Fälle wurde die Sequenz erfolgreich ausgeführt und die Flasche sowie das Glas waren in der richtigen Position. Dabei wurde eine Toleranz von 5cm verwendet. Nur 3 Fälle führten zum Herunterfahren des Systems, was ebenfalls als erfolgreicher Abschluss gezählt werden kann. Die restlichen 51 Ausführungen führten zu keinem Erfolg und wurden im Folgenden manuell analysiert.\\
 Die größte Fehlerquelle stellte das Neigen der Flasche beim Befüllen des Glases dar. Es kam dabei 42 mal zum Umfallen mindestens eines Objektes.
 \cref{fallbeispiel:testergebnisse:log} zeigt das Ende des Logs eines fehlgeschlagenen Tests. Der Channel \textit{place\_success} wurde aktiviert während sich das Modell des Cobots im Zustand \textit{placing\_bottle} befindet, obwohl die Flasche 17cm von seiner Zielposition entfernt war und 90 Grad von der aufrechten Position abwich, sie lag also auf dem Boden.
-Mithilfe der protokollierten Abstände von Positionen und Orientierungen sowie der Zustände in denen diese auftraten lässt sich grob feststellen, wann ein solches Ereignis auftrat. 
+Mithilfe der protokollierten Abstände von Positionen und Orientierungen sowie der Zustände, in denen diese auftraten, lässt sich grob feststellen, wann ein solches Ereignis auftrat. 
 In 27 Fällen war die Flasche zu mindestens einem Zeitpunkt mehr als 110 Grad geneigt, sodass wahrscheinlich kurz vor oder bei der vollen Neigung der Flasche diese verloren ging. Davon wurde in 3 Fällen auch das Glas umgeworfen. Die restlichen 15 mal fiel die Flasche vermutlich eher, da hier keine 110 Grad bei der Orientierungsdifferenz erreicht wurde. Einmal war die Flasche dabei mehr als 2 Meter von seiner Startposition entfernt, was bei dem Tempo der Bewegungen des Roboters äußerst unwahrscheinlich wirkt und vielleicht durch einen Bug (in der Simulation) verursacht wurde. \\
 Nach dem erfolgreichen Befüllen kam es in zwei Fällen zum Umwerfen des Glases beim Aufheben dieses. Weitere zwei Fälle wurde es kurz angehoben und fiel scheinbar zurück in seine Startposition.\\
 Die übrig gebliebenen Testfälle lassen sich unter anderem auf die Planung von Bewegungen zurückführen. So hielt das System je einmal im Zustand \textit{stepping\_back} und \textit{goto\_last\_state\_before\_shutdown}, welche beide auf das Fehlschlagen vom Platzieren des Glases folgen, um den nächsten Platzierungsversuch von einer (leicht) anderen Position auszuführen. Bei genauerer Inspektion des Codes fiel auf, dass an dieser Stelle ein Fehlschlagen der Bewegungsplanung nicht verarbeitet wird, was die Fehlerquelle darstellen könnte.\\
-Die letzten 3 Testausführungen sind (vermutlich) vom eigentlichen System unabhängig aufgetretene Fehler. Zwei mal wurde im Zustand \textit{in\_start\_pos} ein Update von Positionen der Simulation empfangen, was für TRON zu spät war, da als nächstes der Übergang zu \textit{finished\_success} aufgrund des urgent Channels \textit{asap} hätte stattfinden sollen. Da an diesem Punkt aber bereits die Ausführung des Systems beendet war und sich sowohl die Flasche als auch das Glas an den richtigen Positionen befanden, sind diese Fälle als erfolgreiche Systemausführung zu werten und es sollte eine Korrektur auf diese fehlerhafte Modellierung folgen. Beispielsweise könnten die Channels, welche Positionsupdates empfangen, ebenfalls als urgent gekennzeichnet werden.\\
+Die letzten 3 Testausführungen sind (vermutlich) vom eigentlichen System unabhängig aufgetretene Fehler. Zwei mal wurde im Zustand \textit{in\_start\_pos} ein Update von Positionen der Simulation empfangen, was für TRON zu spät war, da als Nächstes der Übergang zu \textit{finished\_success} aufgrund des urgent Channels \textit{asap} hätte stattfinden sollen. Da an diesem Punkt aber bereits die Ausführung des Systems beendet war und sich sowohl die Flasche als auch das Glas an den richtigen Positionen befanden, sind diese Fälle als erfolgreiche Systemausführung zu werten und es sollte eine Korrektur auf diese fehlerhafte Modellierung folgen. Beispielsweise könnten die Channels, welche Positionsupdates empfangen, ebenfalls als urgent gekennzeichnet werden.\\
 Der letzte Fehler konnte in der Konfiguration des Adapters identifiziert werden. Im Zustand \textit{move\_to\_glass} wurde eine Nachricht ohne Orientierungsbeschränkung empfangen, was nur auftreten konnte, da für den Channel \textit{goal}, welcher diese Beschränkung übermittelt, mehrere Topics zuständig sind, sodass in der Queue des Subscribers für eines dieser Topics noch eine Nachricht vorhanden war, in der keine Beschränkung besteht, während eine andere mit dieser (von einem anderen Topic)  bereits verarbeitet war. Das Auftreten eines solchen Fehlers ist als sehr selten einzustufen und könnte verhindert werden, indem etwa nur die letzte Nachricht der drei Topics an TRON weitergegeben wird.\\
-Insgesamt ist festzustellen, dass eine Verbesserung des Befüllvorgangs mit Abstand am relevantesten zur Fehlerreduzierung ist. Außerdem sollte das Fehlschlagen von Planungen der Bewegungen immer beachtet und entsprechend damit umgegangen werden. Schließlich könnte das Aufheben und Platzieren von Objekten zuverlässiger gestaltet werden. Unabhängig vom zu testenden System sind auch Fehler im Modell und Adapter aufgefallen, welche jedoch relativ simpel entfernt werden können. Eine kompakte Auflistung aller Testergebnisse ist in \cref{cobot:testergebnisse:tabelle} zu sehen.
+Insgesamt ist festzustellen, dass eine Verbesserung des Befüllvorgangs mit Abstand am relevantesten zur Fehlerreduzierung ist. Aufgrund der hohen Anzahl dieser Fehler ist zu vermuten, dass es Probleme bei der Simulation des Festhaltens gibt.
+Außerdem sollte das Fehlschlagen von Planungen der Bewegungen immer beachtet und entsprechend damit umgegangen werden. Schließlich könnte das Aufheben und Platzieren von Objekten zuverlässiger gestaltet werden. Unabhängig vom zu testenden System sind auch Fehler im Modell und Adapter aufgefallen, welche jedoch relativ simpel entfernt werden können. Eine kompakte Auflistung aller Testergebnisse ist in \cref{cobot:testergebnisse:tabelle} zu sehen.
 
 \lstset{
 	escapeinside={*}{*}
diff --git a/sections/fazit.tex b/sections/fazit.tex
index ce9134aae179f7475b11e0f6a91753f0bc7f197b..a5b62769bb7d958ea631b0500a19fc022399d8b9 100644
--- a/sections/fazit.tex
+++ b/sections/fazit.tex
@@ -3,6 +3,6 @@ In dieser Arbeit wurde eine Testmethode zum systematischen modell-basierten Test
 \\
 Zusammengefasst lässt sich sagen, dass die in dieser Arbeit verwendete Testmethode erfolgreich zum Finden von unerwünschtem Verhalten und Fehlern verwendet werden kann. Allerdings ist die Implementierung ein aufwändiger Prozess, der sich in einigen Fällen wahrscheinlich nicht lohnt. Bei Systemen, die sich in der Entwicklung befinden oder die aus sonstigen Gründen häufige Änderungen erfahren, kann jedoch ein solcher Testprozess angewandt werden, da bei Vorhandensein des Adapters Änderungen schnell testbar sind, indem das Modell entsprechend verändert wird.
 \\
-Beschränkende Faktoren für die Testentwicklung von Robotersystemen sind vor allem Simulationen, welche jedoch bereits viele Aspekte des Testens stark verbessern. Daher ist die Forschung auf dem Gebiet der Simulationen äußerst wichtig für die Robotik. Aber auch in der Robotik selbst muss weiterhin Forschung betrieben werden, gerade spezielle Tools zum Testen dieser Systeme für akademische Zwecke (oder open source) sind bisher kaum vorhanden, während für modell-basiertes Testen an sich bereits schon viele Lösungen existieren.
+Beschränkende Faktoren für die Testentwicklung von Robotersystemen sind vor allem Simulationen, welche jedoch bereits viele Aspekte des Testens stark verbessern. Daher ist die Forschung auf dem Gebiet der Simulationen äußerst wichtig für die Robotik. Aber auch in der Robotik selbst muss weiterhin Forschung betrieben werden, gerade spezielle Tools zum Testen dieser Systeme für akademische Zwecke (oder open source) sind bisher kaum vorhanden, während für modell-basiertes Testen an sich bereits viele Lösungen existieren.
 \\
 Uppaal selbst ist eine hilfreiche Anwendung und wurde mit TRON um ein sehr sinnvolles Feature erweitert. Allerdings sind die Tools relativ umständlich zu nutzen und es fehlt Unterstützung für heutzutage wichtige Funktionen wie komplexe Variablentypen. Daher wäre eine neue Version des Programms oder eine bessere Alternative ein wichtiger Schritt um modell-basiertes Testen für Robotiksysteme voranzubringen.
\ No newline at end of file