No commit message

No commit message

images/graphwalker_example.json

+{"models":[{"edges":[{"id":"efe24be0-fc3a-11eb-ae6c-913f42b658d7","name":"ausloesen","sourceVertexId":"cb995b20-fc3a-11eb-ae6c-913f42b658d7","targetVertexId":"ca73c6e0-fc3a-11eb-ae6c-913f42b658d7","actions":["zeit = Date.now()"]},{"id":"f0f14ae0-fc3a-11eb-ae6c-913f42b658d7","name":"fertig","sourceVertexId":"cb6a5be0-fc3a-11eb-ae6c-913f42b658d7","targetVertexId":"cb995b20-fc3a-11eb-ae6c-913f42b658d7","guard":"Date.now() - zeit > 10000"},{"id":"ba79b320-fc3b-11eb-ae6c-913f42b658d7","name":"fertig","sourceVertexId":"ca73c6e0-fc3a-11eb-ae6c-913f42b658d7","targetVertexId":"a9921d00-fc3a-11eb-ae6c-913f42b658d7","guard":"Date.now() - zeit > 10000"},{"id":"3756eba0-fc3d-11eb-ae6c-913f42b658d7","name":"ausloesen","sourceVertexId":"a9921d00-fc3a-11eb-ae6c-913f42b658d7","targetVertexId":"cb6a5be0-fc3a-11eb-ae6c-913f42b658d7","actions":["zeit = Date.now();"]},{"id":"777e1b90-fc3d-11eb-ae6c-913f42b658d7","sourceVertexId":"ca73c6e0-fc3a-11eb-ae6c-913f42b658d7","targetVertexId":"ca73c6e0-fc3a-11eb-ae6c-913f42b658d7"},{"id":"a9b0e840-fc3d-11eb-ae6c-913f42b658d7","sourceVertexId":"cb6a5be0-fc3a-11eb-ae6c-913f42b658d7","targetVertexId":"cb6a5be0-fc3a-11eb-ae6c-913f42b658d7"}],"generator":"random(edge_coverage(100))","id":"a4bffb80-fc3a-11eb-ae6c-913f42b658d7","name":"garage","startElementId":"a9921d00-fc3a-11eb-ae6c-913f42b658d7","vertices":[{"id":"a9921d00-fc3a-11eb-ae6c-913f42b658d7","name":"geschlossen","properties":{"x":249,"y":265}},{"id":"ca73c6e0-fc3a-11eb-ae6c-913f42b658d7","name":"schliessend","properties":{"x":399,"y":380}},{"id":"cb6a5be0-fc3a-11eb-ae6c-913f42b658d7","name":"oeffnend","properties":{"x":402,"y":137}},{"id":"cb995b20-fc3a-11eb-ae6c-913f42b658d7","name":"offen","properties":{"x":585,"y":261}}],"editor":{"elements":{"edges":[{"data":{"id":"ba79b320-fc3b-11eb-ae6c-913f42b658d7","name":"fertig","source":"ca73c6e0-fc3a-11eb-ae6c-913f42b658d7","target":"a9921d00-fc3a-11eb-ae6c-913f42b658d7","color":"LightGreen"},"position":{"x":0,"y":0},"group":"edges","removed":false,"selected":false,"selectable":true,"locked":false,"grabbable":true,"pannable":true,"classes":""},{"data":{"id":"efe24be0-fc3a-11eb-ae6c-913f42b658d7","name":"ausloesen","source":"cb995b20-fc3a-11eb-ae6c-913f42b658d7","target":"ca73c6e0-fc3a-11eb-ae6c-913f42b658d7","color":"LightGreen"},"position":{"x":0,"y":0},"group":"edges","removed":false,"selected":false,"selectable":true,"locked":false,"grabbable":true,"pannable":true,"classes":""},{"data":{"id":"f0f14ae0-fc3a-11eb-ae6c-913f42b658d7","name":"fertig","source":"cb6a5be0-fc3a-11eb-ae6c-913f42b658d7","target":"cb995b20-fc3a-11eb-ae6c-913f42b658d7","color":"LightGreen"},"position":{"x":0,"y":0},"group":"edges","removed":false,"selected":false,"selectable":true,"locked":false,"grabbable":true,"pannable":true,"classes":""}],"nodes":[{"data":{"id":"cb995b20-fc3a-11eb-ae6c-913f42b658d7","name":"offen","color":"LightGreen"},"position":{"x":585,"y":261},"group":"nodes","removed":false,"selected":false,"selectable":true,"locked":false,"grabbable":true,"pannable":false,"classes":""},{"data":{"id":"a9921d00-fc3a-11eb-ae6c-913f42b658d7","name":"geschlossen","color":"LightGreen"},"position":{"x":249,"y":265},"group":"nodes","removed":false,"selected":false,"selectable":true,"locked":false,"grabbable":true,"pannable":false,"classes":""},{"data":{"id":"ca73c6e0-fc3a-11eb-ae6c-913f42b658d7","name":"schliessend","color":"LightGreen"},"position":{"x":399,"y":380},"group":"nodes","removed":false,"selected":false,"selectable":true,"locked":false,"grabbable":true,"pannable":false,"classes":""},{"data":{"id":"cb6a5be0-fc3a-11eb-ae6c-913f42b658d7","name":"oeffnend","color":"LightGreen"},"position":{"x":402,"y":137},"group":"nodes","removed":false,"selected":false,"selectable":true,"locked":false,"grabbable":true,"pannable":false,"classes":""}]},"style":[{"selector":"core","style":{"active-bg-size":"0px"}},{"selector":"node","style":{"label":"data(name)","text-wrap":"wrap","text-valign":"center","text-halign":"center","shape":"roundrectangle","width":"label","height":"label","color":"rgb(0,0,0)","background-color":"data(color)","line-color":"data(color)","padding":"10px"}},{"selector":"edge","style":{"label":"data(name)","text-wrap":"wrap","curve-style":"bezier","text-rotation":"autorotate","target-arrow-shape":"triangle","width":"4px","line-color":"data(color)","target-arrow-color":"data(color)","background-color":"data(color)"}},{"selector":":loop","style":{"curve-style":"unbundled-bezier","control-point-step-size":"60px"}},{"selector":":selected","style":{"border-width":"4px","border-color":"rgb(0,0,0)","line-color":"rgb(0,0,0)","target-arrow-color":"rgb(0,0,0)"}}],"data":{},"zoomingEnabled":true,"userZoomingEnabled":true,"zoom":1,"minZoom":1e-50,"maxZoom":1e+50,"panningEnabled":true,"userPanningEnabled":true,"pan":{"x":0,"y":0},"boxSelectionEnabled":true,"renderer":{"name":"canvas"}},"actions":[""]}],"selectedModelIndex":0,"selectedElementId":null}
\ No newline at end of file

sections/stateoftheart.tex

@@ -18,10 +18,22 @@ Invarianten können global oder nur in bestimmten Zuständen angegeben werden. A
 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.
 
 \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.
+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.
+\begin{figure}[h]
+	\centering
+	\includegraphics[scale=.3]{./graphwalker_example.png}
+	\caption{Beispiel-Modell in GraphWalker}
+	\label{konzept:graphwalker:bild}
+\end{figure}
 
 \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, wie in \cref{konzept:mate:bild} zu sehen. 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.
+\begin{figure}[h]
+	\centering
+	\includegraphics[scale=.6]{./MATE.png}
+	\caption{GUI von MATE (zu finden auf der Webseite)}
+	\label{konzept:mate:bild}
+\end{figure}
 
 \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