No commit message

No commit message

sections/evaluation.tex

@@ -10,7 +10,7 @@ Auch hier ist die Simulation und die damit einhergehende korrekte Modellierung a
 \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 der Aufwand bei der Implementierung von modell-basiertem Testen eher als hoch anzusehen. 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 das 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}
@@ -19,9 +19,4 @@ Uppaal und TRON selbst bieten praktisch keine Möglichkeit zur automatisierten A
 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. 
-
+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
-\section{Fazit}
-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.\\
-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

sections/fallbeispiel.tex

-\chapter{Fallbeispiel}
+\chapter{Fallbeispiel}\label{fallbeispiel}
+In diesem Kapitel wird zunächst die Möglichkeit der Integration des Testadapters in ein System, welches die actionlib verwendet, beispielhaft überprüft.
+Die actionlib \cite{Actionlib} baut ein Protokoll auf den Nachrichten von ROS auf und ermöglicht Kommunikation von Nodes für das Ausführen einer bestimmten Aufgabe mithilfe einer Client-Server-Architektur. Diese unterscheidet sich von den \textit{ROS Services}\footnote{\url{http://wiki.ros.org/Services}} insbesondere durch die ermöglichte Asynchronität, welche für konstante Rückmeldung des Servers sowie weitere Anfragen des Clients (wie etwa nach der Präemptierung einer Aktion) genutzt wird. 
+Dazu wurde von der Bibliothek die Implementierung eines endlichen Automaten realisiert, was sich neben den verwendeten ROS-Nachrichten für das Testen mittels TRON aufgrund der einfachen Modellierung in Uppaal anbietet. \\
+Wenn die Integration möglich ist, wird folgend das am Lehrstuhl verwendete Cobot-Projekt\footnote{\url{https://git-st.inf.tu-dresden.de/ceti/ros/chemistry-lab-demo/}} (verwendete Version \href{https://git-st.inf.tu-dresden.de/ceti/ros-internal/chemistry-lab-demo/cobot_1/-/tree/0ab6cd6d48613f4cb913e433832ccd741682bcde}{0ab6cd6d}) benutzt, um den Testvorgang mittels des vorgestellten Konzeptes zu evaluieren. Der Roboter (Franka Panda\footnote{\url{https://www.franka.de/robot-system}}) soll eine Flasche aufheben, um damit ein Glas zu befüllen. Folglich wird die Flasche wieder an ihre Anfangsposition gebracht und das nun befüllte Glas auf die andere Seite des Roboters transportiert.
+
 \section{Integration mit actionlib}\label{actionlib:integration}
 Hier wird überprüft, ob der Testadapter bei Systemen, welche auf der actioblib basieren, verwendbar ist.
 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.\\
@@ -104,27 +109,23 @@ Die letzten 3 Testausführungen sind (vermutlich) vom eigentlichen System unabh
 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.
 
-\begin{table}[h]
+\begin{table}
 	\caption{Testergebnisse}
 	\label{cobot:testergebnisse:tabelle}
-\begin{tabularx}{\textwidth}{c|c|X}
-	
+	{\small
+\begin{tabularx}{\textwidth}{rlX}
+	\toprule[.3mm]
 	\textbf{Anzahl} & \textbf{Ergebnis} & \textbf{(potentieller) Fehler} \\
-	\hline
+	\midrule[.3mm]
 	46 & erfolgreiche Ausführung & - \\
-	\hline
 	3 & System heruntergefahren (Erfolg) & - \\
-	\hline
 	42 & Flasche (und Glas) gefallen & Probleme beim Aufheben oder Festhalten \\
-	\hline
 	4 & Glas gefallen & Probleme beim Aufheben oder Festhalten \\
-	\hline
 	2 & System angehalten & fehlgeschlagene Bewegungsplanung \\
-	\hline
 	2 & Zu spätes Positionsupdate & Modellfehler \\
-	\hline
 	1 & Nicht mehr aktuelle Nachricht & Fehler im Adapter \\
 \end{tabularx}
+}
 \end{table}
 
 

sections/fazit.tex

+\chapter{Fazit}
+In dieser Arbeit wurde eine Testmethode zum systematischen modell-basierten Testen von Robotiksystemen unter ROS vorgestellt. Zur Modellierung wurde Uppaal benutzt, während dessen Erweiterung TRON online-Testing der exemplarisch überprüften Implementierung des Cobots ermöglichte. Am Ende fand eine Bewertung des Konzepts mittels eingangs aus aktueller Literatur ermittelter spezieller Anforderungen für Robotiksysteme statt.
+\\
+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.
+\\
+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

sections/konzept.tex

 \chapter{Konzept}
+Dieses Kapitel beschreibt welche Simulation verwendet wird und erklärt den Prozess der Modellentwicklung in Uppaal.
+Dann folgt eine Erläuterung der Funktionsweise des implementierten Adapters sowie der Verwendung dessen.
+
 \section{Simulation}\label{konzept:simulation}
 Als Simulator bietet sich Gazebo an, da es sich einfach in ROS integrieren lässt und eine relativ hohe physikalische Korrektheit bietet. Verschiedene Physik-Engines können innerhalb von Gazebo verwendet werden.
 Auch werden Plug-Ins unterstützt, sodass sich auch nicht nativ implementiere Sachverhalte wie etwa die Umgebungstemperatur darstellen lassen \cite{Harris2011}. Gazebo ist daher und aufgrund seiner Stabilität in der Robotik und insbesondere in der Forschung die momentan am meisten verwendete Simulationssoftware.
@@ -63,11 +66,4 @@ Zur Verwendung des Adapters müssen primär Veränderungen in der Funktion \text
 \end{lstlisting}
 Der Channel \textit{position} sowie die Variable \textit{pos} sind in \cref{konzept:uppaal_tor} nicht dargestellt, werden hier aber verwendet um einen Output-Channel sowie das Übertragen einer Variable zu demonstrieren.\\
 Wenn das Bestimmen der Positionen von Variablen innerhalb einer Nachricht schwierig ist, da diese beispielsweise aus vielen Feldern variabler Größen bestehen, so ist es sinnvoller eigene Callbacks zu implementieren, welche die von ROS erstellten Header-Dateien der Nachrichten zu nutzen, was gleichzeitig zu einer besseren Lesbarkeit des Codes beiträgt und damit die Wartung erleichtert. Dabei können diese Callbacks die Methode \textit{report\_now} verwenden, um TRON das Auslösen eines Channels zu signalisieren und Variablen zu übergeben. Auch hier ist zu erwähnen, dass die Übersetzung von einem Topic zu mehreren Channels in lediglich einer Methode stattfinden muss, die dem ROS-Subscriber als Parameter übergeben wird.
-Diese Variante wird auch bei einer später im Text folgenden beispielhaften Anwendung des Adapters für die sogenannte \textit{actionlib} (siehe \cref{konzept:actionlib}) verwendet.
-
-\section{actionlib}\label{konzept:actionlib}
-Die actionlib \cite{Actionlib} baut ein Protokoll auf den Nachrichten von ROS auf und ermöglicht Kommunikation von Nodes für das Ausführen einer bestimmten Aufgabe mithilfe einer Client-Server-Architektur. Diese unterscheidet sich von den \textit{ROS Services}\footnote{\url{http://wiki.ros.org/Services}} insbesondere durch die ermöglichte Asynchronität, welche für konstante Rückmeldung des Servers sowie weitere Anfragen des Clients (wie etwa nach der Präemptierung einer Aktion) genutzt wird. 
-Dazu wurde die Implementierung eines endlichen Automaten realisiert, was sich neben den verwendeten ROS-Nachrichten für das Testen mittels TRON anbietet. Daher wird die Möglichkeit einer Integration des Testadapters in ein System, welches die actionlib verwendet, beispielhaft überprüft.
-
-\section{Cobot}
-Das am Lehrstuhl verwendete Cobot-Projekt\footnote{\url{https://git-st.inf.tu-dresden.de/ceti/ros-internal/chemistry-lab-demo/cobot_1/-/tree/feature/cobot-homestate-version}} wird benutzt, um den Testvorgang mittels des hier vorgestellten Konzeptes zu evaluieren. Der Roboter (Franka Panda\footnote{\url{https://www.franka.de/robot-system}}) soll eine Flasche aufheben, um damit ein Glas zu befüllen. Folglich wird die Flasche wieder an ihre Anfangsposition gebracht und das nun befüllte Glas auf die andere Seite des Roboters transportiert.
+Diese Variante wird auch bei einer später im Text folgenden beispielhaften Anwendung des Adapters für die sogenannte \textit{actionlib} (siehe \cref{fallbeispiel}) verwendet.
\ No newline at end of file

sections/stateoftheart.tex

@@ -3,12 +3,11 @@ Neben der bereits erwähnten Integration von Unit-Tests in ROS und rostests, wel
 \section{Spec Explorer (2010)}
 Der Spec Explorer von Microsoft\footnote{\url{https://marketplace.visualstudio.com/items?itemName=SpecExplorerTeam.SpecExplorer2010VisualStudioPowerTool-5089}} ist ein Tool für Modell-basiertes Testen und als kostenlose Erweiterung für Visual Studio vorhanden. Da jedoch eine kostenpflichtige Visual Studio Version notwendig ist, ist dieses Tool als kommerziell einzustufen und kann im Rahmen dieser Arbeit nicht verwendet werden. Es ist jedoch aufgrund seiner Verbreitung hier zu erwähnen und wurde bereits häufig im akademischen Rahmen verwendet \cite{Silva2008, Campbell2005, Campbell2005a, Naujoks2011, Botincan2007}. Ein abstraktes Modell des zu testenden Systems wird dabei in C\# implementiert, es sind jedoch auch andere Sprachen möglich. Das Tool ist umfangreich und bietet sowohl online- als auch offline-Testing an, wobei sich durch Adapter sämtliche Programmiersprachen verwenden lassen. Ebenso wird eine Validierung des Modells selbst unterstützt und es können verschiedene Testauswahlkriterien angewandt werden.
 \section{Uppaal TRON}
-Uppaal\footnote{\url{https://uppaal.org/}} ist ein für akademische Zwecke frei verfügbares Tool zum Validieren von Modellen und wurde bereits in \cite{Ernits2015, Gummel2018} im Zusammenhang mit ROS verwendet. Dabei wird eine Erweiterung namens TRON\footnote{\url{https://people.cs.aau.dk/~marius/tron/}} (Testing Realtime Systems Online) benutzt, welche das Modell im Rahmen eines online-Tests durchläuft, was sich wie in \cref{grundlagen:testentwicklung:modell-basiert} dargestellt für Robotiksysteme anbietet. Außerdem kann Uppaal ein erstelltes Modell mithilfe von formalen Anfragen einer eigenen Syntax validieren, was gerade in den Anfangsphasen eines Projektes hilfreich sein kann.
-Aus diesen Gründen und da auch am Lehrstuhl bereits mit Uppaal gearbeitet wurde, wird das Tool in dieser Arbeit exemplarisch angewandt. Die Erweiterung von TRON namens DTRON (Distributed TRON) für verteilte Systeme sowie das verwendete Adapter-Template von \cite{Ernits2015, Gummel2018} steht zum momentanen Zeitpunkt nicht zur Verfügung und kann daher nicht verwendet werden. Im folgenden wird sowohl das Modell unter Uppaal sowie die Funktionsweise des TRON-Adapters erläutert.
+Uppaal\footnote{\url{https://uppaal.org/}} ist ein für akademische Zwecke frei verfügbares Tool zum Validieren von Modellen und wurde bereits in \cite{Ernits2015, Gummel2018} im Zusammenhang mit ROS verwendet. Dabei wird eine Erweiterung namens TRON\footnote{\url{https://people.cs.aau.dk/~marius/tron/}} (Testing Realtime Systems Online) benutzt, welche das Modell im Rahmen eines online-Tests durchläuft, was sich wie in \cref{grundlagen:testentwicklung:modell-basiert} dargestellt für Robotiksysteme anbietet. Außerdem kann Uppaal ein erstelltes Modell mithilfe von formalen Anfragen einer eigenen Syntax validieren, was gerade in den Anfangsphasen eines Projektes hilfreich sein kann. Im folgenden wird sowohl das Modell unter Uppaal sowie die Funktionsweise des TRON-Adapters erläutert.
 \subsection{Modell in Uppaal}
 Ein System in Uppaal besteht aus einem oder mehreren Automaten. Sogenannte \textit{Channel} und global deklarierte Variablen sorgen für eine Synchronisation dieser. Die Automaten selbst sind als erweiterte endliche nicht-deterministische Automaten einzuordnen, die auch Zeitangaben unterstützen. Durch Guards kann festgelegt werden, wann eine Kante verfügbar ist. Beim Entlanggehen einer Kante, welches auch durch die erwähnten Channel ausgelöst werden kann, können Variablen (global oder lokal) angepasst werden. Channel bieten sich als Modellierung der ROS Topics an.
 Invarianten können global oder nur in bestimmten Zuständen angegeben werden. Außerdem lassen sich Channel sowie Zustände mit verschiedenen Eigenschaften versehen, welche die Ausführung des Modells beeinflussen. Ein als \textit{urgent} bezeichneter Channel sorgt beispielsweise dafür, dass Kanten die mit ihm markiert sind so schnell wie möglich abgelaufen werden. Zustände die als \textit{commited} (im Editor markiert mit einem C) oder als \textit{urgent} (im Editor markiert mit einem U) verbieten, dass in ihnen Zeit abläuft und ermöglichen so das Modellieren von unmittelbar aufeinander folgenden Ereignissen, wobei \textit{commited} noch restriktiver ist, da ein solcher Zustand im nächsten Übergang verlassen werden muss.\\
-\cref{konzept:uppaal_tor} zeigt beispielhaft ein modelliertes System eines automatischen Tores mit einem dazugehörigen Schlüssel. Beim probabilistischen Auslösen dieses Schlüssels (mit einer Wahrscheinlichkeit von 1:101) wird das Tor über den Channel \textit{auslösen} informiert, wechselt in den Zustand \textit{öffnend} und setzt die Variable "zeit" auf 0. Nach 10000 vergangenen Zeiteinheiten wechselt das Tor dann in den Zustand \textit{offen}. Das Schließen läuft analog dazu ab.
+\cref{konzept:uppaal_tor} zeigt beispielhaft ein modelliertes System eines automatischen Tores mit einem dazugehörigen Schlüssel. Beim probabilistischen Auslösen dieses Schlüssels (mit einer Wahrscheinlichkeit von 1:101) wird das Tor über den Channel \textit{auslösen} informiert, wechselt in den Zustand \textit{öffnend} und setzt die Variable \textit{zeit} auf 0. Nach 10000 vergangenen Zeiteinheiten wechselt das Tor dann in den Zustand \textit{offen}. Das Schließen läuft analog dazu ab.
 \begin{figure}[h]
 	\centering
 	\includegraphics[scale=.4]{./uppaal_tor.png}
@@ -22,4 +21,7 @@ Channels, welche sowohl im modellierten Input als auch im System vorkommen stell
 GraphWalker \footnote{\url{http://graphwalker.github.io/}} ist ein neueres Tool, welches auf eine möglichst einfache Bedienung ausgelegt ist. Zum Erstellen von Modellen gibt daher es einen grafischen Editor, welcher über einen Browser geöffnet werden kann. Die Modellierungsmöglichkeiten ähneln denen von Uppaal, wobei weniger Kontrolle über die Ausführung gegeben ist, da Kanten sofort abgelaufen werden, wenn sie verfügbar sind. Dafür können sowohl bei Übergängen als auch in Knoten Aktionen ausgeführt werden, welche durch JavaScript beschrieben sind. Dadurch können im Gegensatz zu Uppaal komplexere Zusammenhänge besser dargestellt werden. Online- und offline-Testen wird unterstützt, wofür eine REST- sowie Websocket-API zur Verfügung steht. Informationen werden dabei durch JSON übermittelt, was auch das Übertragen von komplexen Variablen ermöglicht. Eine Verifizierung eines erstellten Modells kann jedoch nur durch das Ablaufen dieses erfolgen, eine Möglichkeit zur formalen Validierung von Systemeigenschaften existiert nicht.
 
 \section{MATE}
-Das Model-based Adaptivity Test Environment\footnote{\url{http://81.88.24.184/qmate/}} (MATE) wurde unter anderem in \cite{Pueschel2018} vorgestellt und unterstützt verschiedene Arten von Modellen, sodass sich Systeme möglichst optimal darstellen lassen. Abhängig vom genutzten Modell sind Editoren vorhanden, die das Erstellen vereinfachen. Auch hier kann vor dem Testen eine Verifizierung der erarbeiteten Darstellung stattfinden. Es wird online und offline-Testing ermöglicht, statistische Analysen der Testergebnisse werden automatisch (bei offline-Tests) durchgeführt. Zur Ausführung der Tests lassen sich benutzerdefinierte Adapter einrichten, sodass MATE unabhängig von der vom System verwendeten Technologie angewandt werden kann. Außerdem ist das Tool auf Erweiterbarkeit ausgelegt, das heißt es existiert beispielsweise ein Framework, mit welchem eigene Modelltypen implementiert werden können (solange diese einem Metamodell-Interface folgen). Insgesamt ist MATE ein mächtiges und breit einsetzbares Tool für Modell-basiertes Testen, es ist jedoch momentan nicht verfügbar und kann daher im Rahmen dieser Arbeit nicht verwendet werden.
+Das Model-based Adaptivity Test Environment\footnote{\url{http://81.88.24.184/qmate/}} (MATE) wurde unter anderem in \cite{Pueschel2018} vorgestellt und unterstützt verschiedene Arten von Modellen, sodass sich Systeme möglichst optimal darstellen lassen. Abhängig vom genutzten Modell sind Editoren vorhanden, die das Erstellen vereinfachen. Auch hier kann vor dem Testen eine Verifizierung der erarbeiteten Darstellung stattfinden. Es wird online und offline-Testing ermöglicht, statistische Analysen der Testergebnisse werden automatisch (bei offline-Tests) durchgeführt. Zur Ausführung der Tests lassen sich benutzerdefinierte Adapter einrichten, sodass MATE unabhängig von der vom System verwendeten Technologie angewandt werden kann. Außerdem ist das Tool auf Erweiterbarkeit ausgelegt, das heißt es existiert beispielsweise ein Framework, mit welchem eigene Modelltypen implementiert werden können (solange diese einem Metamodell-Interface folgen). Insgesamt ist MATE ein mächtiges und breit einsetzbares Tool für Modell-basiertes Testen, es ist jedoch momentan nicht verfügbar und kann daher im Rahmen dieser Arbeit nicht verwendet werden.
\ No newline at end of file
+
+\section{Tool-Auswahl}
+Uppaal und TRON werden im weiteren Verlauf dieser Arbeit exemplarisch angewandt. Zum einen kann das Verhalten der Modelle durch die verschiedenen Typen von Knoten und Kanten genau bestimmt werden, zum anderen ist die Verifizierung ein hilfreiches Feature. Außerdem wurde vom Lehrstuhl bereits mit dem Tool, jedoch ohne TRON, gearbeitet. Aus diesen Gründen und da auch am Lehrstuhl bereits mit Uppaal gearbeitet wurde, wird das Tool in dieser Arbeit exemplarisch angewandt. Die Erweiterung von TRON namens DTRON (Distributed TRON) für verteilte Systeme sowie das verwendete Adapter-Template von \cite{Ernits2015, Gummel2018} steht momentan nicht zur Verfügung und kann daher nicht verwendet werden.
\ No newline at end of file

thesis.tex

@@ -126,6 +126,7 @@
 \input{sections/konzept.tex}
 \input{sections/fallbeispiel.tex}
 \input{sections/evaluation.tex}
+\input{sections/fazit.tex}
 
 \printbibliography[heading=bibintoc]\label{sec:bibliography}%