@@ -4,11 +4,11 @@ Dann folgt eine Erläuterung der Funktionsweise des implementierten Adapters sow
\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.
Allerdings können komplexe Zusammenhänge, auch abhängig von der gewünschten Akkuratheit, bei einer Implementierung in Form von Plug-Ins den Entwicklungsaufwand stark erhöhen. Problematisch ist bei Gazebo die Performance bei vielen simulierten Robotern oder komplexen Umgebungen, sodass in diesen Fällen potentiell andere Simulatoren verwendet werden sollten \cite{Ivaldi2014}.
Auch sind 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.
Allerdings können komplexe Zusammenhänge, auch abhängig von der gewünschten Akkuratheit, bei einer Implementierung in Form von Plug-Ins den Entwicklungsaufwand stark erhöhen. Problematisch ist bei Gazebo die Performance bei vielen simulierten Robotern oder komplexen Umgebungen, sodass in diesen Fällen potenziell andere Simulatoren verwendet werden sollten \cite{Ivaldi2014}.
\section{Uppaal-Modellierung}
Vor dem Erstellen eines Modells müssen zunächst die gewünschten Anforderungen des Systems formal festgehalten werden. Diese formalen Anforderungen müssen dann quantisiert werden. Dazu bieten sich besonders für die nicht-funktionalen Eigenschaften Invarianten im Modell an.
Da für die Testgenerierung auch ein Modell für die Inputs des Systems nötig ist, können die Modelle auch innerhalb von Uppaal verifiziert werden. Ebenso können formale Eigenschaften mithilfe des integrierten Verifiers überprüft werden. Wie in \cref{grundlagen:testentwicklung:modell-basiert} erwähnt können, falls schon eine Implementierung vorhanden ist, auch Modelle die zur Entwicklung verwendet wurden zur Verifizierung beitragen.
Vor dem Erstellen eines Modells müssen zunächst die gewünschten Anforderungen des Systems formal festgehalten werden. Diese formalen Anforderungen sind dann zu quantisieren. Dabei bieten sich besonders für die nicht-funktionalen Eigenschaften Invarianten im Modell an.
Da für die Testgenerierung auch ein Modell für die Inputs des Systems nötig ist, können die Modelle auch innerhalb von Uppaal verifiziert werden. Ebenso lassen sich formale Eigenschaften mithilfe des integrierten Verifiers überprüfen. Wie in \cref{grundlagen:testentwicklung:modell-basiert} erwähnt können, falls schon eine Implementierung vorhanden ist, auch Modelle die zur Entwicklung verwendet wurden zur Verifizierung beitragen.
\section{TRON-Adapter}
Um den Adapter an da ROS-System anzuknüpfen, wurde ein ROS-Node geschrieben, welcher die Pakete des Adapters annimmt und intern über die ROS Topics an das System weitergibt. Diese Übersetzung ist generisch implementiert, sodass zukünftig für ROS-Projekte dieser Adapter bis auf die Konfiguration wiederverwendet werden kann. Um die Umgebung in der Simulation auch für TRON verfügbar zu machen, müssen die dafür vorhandenen Daten über ein ROS Topic im System veröffentlicht und dann durch den Adapter weitergereicht werden.
...
...
@@ -23,7 +23,7 @@ Im Leitfaden zu TRON~\cite{TronManual} sind die verwendeten Pakete beschrieben u
\subsection{Adapter-Phasen}
\subsubsection{Konfigurierungsphase}
Zunächst wird der SocketAdapter auf eine eingehende Verbindung warten. Folglich werden Konfigurationsdaten ausgetauscht. Strings sind dabei durch ein Byte mit der Länge des Strings gefolgt von dieser Anzahl an Bytes repräsentiert. Als erstes werden die verschiedenen Channel als Input beziehungsweise Output deklariert. Dazu wird ein Paket mit dem ersten Byte 1 beziehungsweise 2 und dem Namen des jeweiligen Channels im Uppaal Modell versendet. Als Antwort empfängt der Node einen 32-Bit Integer, der die ab diesem Zeitpunkt für diesen Channel genutzte ID widerspiegelt. Ist dieser kleiner oder gleich 0, so trat ein Fehler auf. Die Fehlermeldung kann dann mittels eines Pakets ermittelt werden (erstes Byte 127, dann Fehlercode). Nach erhalten der ChannelIDs werden diese genutzt um die Namen der Variablen im Uppaal Modell den Channels zuzuordnen. Als letzter Schritt der Konfigurierungsphase werden mittels der Codes 5 und 6 die Zeiteinheiten sowie der Timeout zum Beenden des Tests gesetzt. \cref{konzept:tron_konfigurierung} skizziert den fehlerfreien Ablauf dieser Phase. Für Output-Channel müssen die dargestellten Bytecodes 1 und 3 durch 2 und 4 ersetzt werden.
Zunächst wird der SocketAdapter auf eine eingehende Verbindung warten. Folglich werden Konfigurationsdaten ausgetauscht. Strings sind dabei durch ein Byte mit der Länge gefolgt von dieser Anzahl an Bytes repräsentiert. Als Erstes werden die verschiedenen Channel als Input beziehungsweise Output deklariert. Dazu wird ein Paket mit dem ersten Byte 1 beziehungsweise 2 und dem Namen des jeweiligen Channels im Uppaal Modell versendet. Als Antwort empfängt der Node einen 32-Bit Integer, der die ab diesem Zeitpunkt für diesen Channel genutzte ID widerspiegelt. Ist dieser kleiner oder gleich 0, so trat ein Fehler auf. Die Fehlermeldung kann dann mittels eines Pakets ermittelt werden (erstes Byte 127, dann Fehlercode). Nach Erhalten der Channel-IDs werden diese genutzt, um die Namen der Variablen im Uppaal Modell dem jeweiligen Channel zuzuordnen. Als letzter Schritt der Konfigurierungsphase werden mittels der Codes 5 und 6 die Zeiteinheiten sowie der Timeout zum Beenden des Tests gesetzt. \cref{konzept:tron_konfigurierung} skizziert den fehlerfreien Ablauf dieser Phase. Für Output-Channel müssen die dargestellten Bytecodes 1 und 3 durch 2 und 4 ersetzt werden.
@@ -31,16 +31,16 @@ Zunächst wird der SocketAdapter auf eine eingehende Verbindung warten. Folglich
\label{konzept:tron_konfigurierung}
\end{figure}
\subsubsection{Ausführungsphase}
Nach erfolgreicher Konfiguration sendet der Node ein Byte mit dem Wert 64 um den Start des Tests anzufragen, als Antwort erhält er ein Byte mit dem Wert 0. Folglich werden Inputs und Outputs ausgetauscht, dabei bestehen die ersten 4 Byte der Nachricht aus den ChannelIdentifiern, worauf 2 Byte mit der Anzahl an verknüpften Variablen und schließlich die Variablen (je 4 Byte) folgen. Diese müssen dann innerhalb der ROS-Topics verbreitet werden. Als Antwort wird von beiden Seiten eine Bestätigung zurückgesendet, Inputs und Outputs können jedoch asynchron übertragen werden.
Nach erfolgreicher Konfiguration sendet der Node ein Byte mit dem Wert 64, um den Start des Tests anzufragen, als Antwort erhält er ein Byte mit dem Wert 0. Folglich werden Inputs und Outputs ausgetauscht, dabei bestehen die ersten 4 Byte der Nachricht aus den Channel-Identifiern, worauf 2 Byte mit der Anzahl an verknüpften Variablen und schließlich die Variablen (je 4 Byte) folgen. Diese müssen dann innerhalb der ROS-Topics verbreitet werden. Als Antwort wird von beiden Seiten eine Bestätigung zurückgesendet, Inputs und Outputs können jedoch asynchron übertragen werden.
\subsection{Implementierung}
Der implementierte Adapter verwendet vom Betriebssystem bereitgestellte Sockets für die Kommunikation mit TRON und hält relevante Variablen, in welchen die Abbildungen von Channels auf Topics sowie die zugehörigen Variablen beschrieben werden, innerhalb einer Klasse. Die Verwendung dieser wird im nächsten Abschnitt dargestellt.
Der implementierte Adapter verwendet vom Betriebssystem bereitgestellte Sockets für die Kommunikation mit TRON und hält relevante Variablen, in welchen die Abbildungen von Channel auf Topics sowie die zugehörigen Variablen beschrieben werden, innerhalb einer Klasse. Die Verwendung dieser wird im nächsten Abschnitt dargestellt.
Bei der Implementierung des Adapters (siehe Header-Datei im Anhang) sind einige Unklarheiten im Handbuch zu TRON (\cite{TronManual}) aufgefallen. So werden die Bytecodes 64 (tatsächlich zum Starten verwendet) und 127 (verwendet zum Anfragen von Fehlermeldungen) vertauscht. Lokale Variablen sowie probabilistische Kanten wie in \cref{konzept:uppaal_tor} werden von TRON nicht unterstützt, im Handbuch allerdings auch nicht erwähnt. Außerdem ist bei der Übertragung der Zeit pro Zeiteinheit die Rede von zwei 32-Bit-Integer-Variablen, während TRON tatsächlich einen 64-Bit-Integer (ohne Vorzeichen) verwendet, um die Mikrosekunden einer Modell-Zeiteinheit festzulegen. Derartige Fehlinformationen sind vermutlich darauf zurückzuführen, dass Uppaal sowie TRON selbst Updates erhielten, ohne dass das Handbuch angepasst wurde.\\
Der Adapter wurde möglichst generisch gehalten und ist somit für sämtliche Nachrichten die innerhalb von ROS Topics ausgetauscht werden verwendbar. Einem Channel des Modells lassen sich beliebig viele Topics zuweisen und umgekehrt.
Templates ermöglichen generische Callbacks mit denen den TRON-Variablen Positionen innerhalb der ROS-Nachrichten zugewiesen werden, es sind jedoch auch eigene Implementierungen zum Beispiel für Felder mit variabler Länge möglich, welche in den meisten Fällen zu empfehlen sind.
Templates ermöglichen generische Callbacks, mit denen den Uppaal-Variablen Positionen innerhalb der ROS-Nachrichten zugewiesen werden, es sind jedoch auch eigene Implementierungen zum Beispiel für Felder mit variabler Länge möglich, welche in den meisten Fällen zu empfehlen sind.
\subsubsection{Verwendung}
Zur Verwendung des Adapters muss eine Instanz der Klasse \textit{TRON\_Adapter} erstellt werden. Ihr wird die ZielIP-Adresse sowie der Port übergeben, über den eine bereits laufende TRON Instanz erreichbar ist. Die Struktur \textit{Mapping} beschreibt das Verhältnis von einem Channel zu einem Topic und muss daher für jedes gewünschte Paar mittels der Funktion \textit{createMapping} initialisiert werden. Dabei ist (nach dem Namen des Topics und dem Namen des Channels) anzugeben, ob dieses Mapping als Eingabe oder Ausgabe dient. Soll ein Channel sowohl Eingabe als auch Ausgabe sein, oder sollen mehrere Topics einem Channel zugewiesen werden (oder umgekehrt), so müssen dafür zusätzliche Mappings erstellt werden.
\\ Nach der Initialisierung lassen sich Variablen hinzufügen. Dazu wird dem Adapter über \textit{add\_var\_to\_mapping} neben dem Mapping selbst der Name der Variablen in Uppaal übergeben. Optionale Parameter wie zum Beispiel der Offset können angegeben werden, wenn die Übersetzung mittels Byte-Positionen innerhalb der ROS-Nachricht stattfinden soll. Der Offset beginnt vom Ende des letzten Felder, sodass in diesem Fall die Variablen in der richtigen Reihenfolge angegeben werden müssen.
Zur Verwendung des Adapters muss eine Instanz der Klasse \textit{TRON\_Adapter} erstellt werden. Ihr wird die Ziel-IP-Adresse sowie der Port übergeben, über den eine bereits laufende TRON Instanz erreichbar ist. Die Struktur \textit{Mapping} beschreibt das Verhältnis von einem Channel zu einem Topic und muss daher für jedes gewünschte Paar mittels der Funktion \textit{createMapping} initialisiert werden. Dabei ist (nach dem Namen des Topics und dem Namen des Channels) anzugeben, ob dieses Mapping als Eingabe oder Ausgabe dient. Soll ein Channel sowohl Eingabe als auch Ausgabe sein, oder sollen mehrere Topics einem Channel zugewiesen werden (oder umgekehrt), so müssen dafür zusätzliche Mappings erstellt werden.
\\ Nach der Initialisierung lassen sich Variablen hinzufügen. Dazu wird dem Adapter über \textit{add\_var\_to\_mapping} neben dem Mapping selbst der Name der Variablen in Uppaal übergeben. Optionale Parameter wie zum Beispiel der Offset können angegeben werden, wenn die Übersetzung mittels Byte-Positionen innerhalb der ROS-Nachricht stattfinden soll. Der Offset beginnt vom Ende des letzten Feldes, sodass in diesem Fall die Variablen in der richtigen Reihenfolge angegeben werden müssen.
\\ Für Input-Channel ist zusätzlich ein Callback zu spezifizieren, welcher als Parameter eine Referenz zum entsprechenden Mapping und ein Array von 32-Bit-Integern, den von TRON übergebenen Variablen, bekommt. \textit{mapping\_callback\_to\_topic} kann dafür verwendet werden, und mit den festgelegten Byte-Positionen zu arbeiten. Output-Channel haben keinen separaten Callback, da dieser beim Abonnieren eines Topics durch die ROS API festgelegt wird. Wie bei den Input-Channel ist dafür eine generische Funktion vorhanden, \textit{mappings\_callback\_to\_TRON}, welche bei einfachen Nachrichten verwendet werden kann. Anzumerken ist hierbei, dass diese Methode alle Channel informiert, die als Output mit dem Topic angegeben sind, während bei den Inputs jeweils eine Funktion im Mapping hinterlegt ist.
\\ Schließlich muss das Mapping der Liste \textit{mappings} hinzugefügt werden. Zu beachten ist, dass für jedes Topic, welches im Rahmen von Input-Mappings verwendet wird ein entsprechender \textit{ros::Publisher} in der Liste \textit{input\_publishers} vorhanden sein muss. Analog dazu müssen \textit{ros::Subscriber} zu \textit{output\_subscriber} hinzugefügt werden.
\\ Neben den Mappings muss auch die Zeiteinheit sowie der Zeitraum für den getestet werden soll festgelegt werden, dies geschieht über einen Funktionsaufruf an \textit{set\_time\_unit\_and\_timeout}.
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.
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.
Ein besonderes Augenmerk liegt auf dem Callback des ros::Subscriber. Dieser benötigt nach dem boost::bind der Adapter-Instanz an die Funktion einen expliziten Cast zu einer boost::function des entsprechenden Typs, da der Compiler diesen nicht zuverlässig selbstständig ableiten kann und dennoch keinen Fehler ausgibt. Dies ist auf der zum Thema passenden Übersichtsseite von ROS\footnote{\url{http://wiki.ros.org/roscpp/Overview/Publishers\%20and\%20Subscribers}} in einer Notiz unter 2.3.3 angemerkt.
\\
In den meisten praktischen Fällen ist das verwenden eigens für bestimmte Nachrichten implementierter Callbacks sinnvoller, da ROS-Nachrichten sehr komplex sein können und viele Felder variabler Größe verwendet werden, wofür Konvertierungsfunktionen nötig wären. Außerdem wird dadurch die Lesbarkeit des Codes erhöht und folglich die Wartung erleichtert. Benutzerdefinierte Callbacks können \textit{report\_now} und \textit{publish\_to\_topic} nutzen um Nachrichten zu TRON beziehungsweise zu den Topics zu senden.
@@ -3,10 +3,10 @@ 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. 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.\\
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 \textit{Guards} (boolesche Ausdrücke) 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 \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
...
...
@@ -15,7 +15,7 @@ Invarianten können global oder nur in bestimmten Zuständen angegeben werden. A
\label{konzept:uppaal_tor}
\end{figure}
\subsection{TRON Adapter}
Channels, welche sowohl im modellierten Input als auch im System vorkommen stellen die Schnittstellen für den Adapter dar. Wird im Inputmodell ein Channel verwendet, so wird dieser sowohl im modellierten als auch im echten (oder simulierten) System über den Adapter ausgelöst. Asynchron dazu gibt das System den Output zurück an den Adapter, welcher dann mit den Gegebenheiten des Modells verglichen wird. Als built-in Adapter sind der sogenannte TraceAdapter, welcher über stdin/stdout (Standard-Pipes von Linux) kommuniziert, und der SocketAdapter, welcher zur Kommunikation eine TCP/IP-Verbindung aufbaut, verfügbar. Auch eigene Implementationen werden als dynamische C-Bibliothek ermöglicht. Für ROS bietet sich der SocketAdapter an, da die ROS-interne Kommunikation selbst auf TCP aufsetzt und so auch Übertragbarkeit gewährleistet wird.
Channels, welche sowohl im modellierten Input als auch im System vorkommen, stellen die Schnittstellen für den Adapter dar. Wird im Input-Modell ein Channel verwendet, so wird dieser sowohl im modellierten als auch im echten (oder simulierten) System über den Adapter ausgelöst. Asynchron dazu gibt das System den Output zurück an den Adapter, welcher dann mit den Gegebenheiten des Modells verglichen wird. Als built-in Adapter sind der sogenannte TraceAdapter, welcher über \textit{stdin/stdout} (Standard-Pipes von Linux) kommuniziert, und der SocketAdapter, welcher zur Kommunikation eine TCP/IP-Verbindung aufbaut, verfügbar. Auch eigene Implementationen werden als dynamische C-Bibliothek ermöglicht. Für ROS bietet sich der SocketAdapter an, da die ROS-interne Kommunikation selbst auf TCP aufsetzt und so auch Übertragbarkeit gewährleistet wird.
\section{GraphWalker}
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. In \cref{konzept:graphwalker:bild} ist das schon bei Uppaal verwendete Beispiel ähnlich modelliert zu sehen. Guards sowie Variablenzuweisungen sind im Editor nicht zu sehen. Eine Synchronisation mit anderen Modellen wie dem Schlüssel könnte über globale Variablen realisiert sein, da keine Channels im Sinne von Uppaal vorhanden sind.
