diff --git a/images/MATE.png b/images/MATE.png new file mode 100644 index 0000000000000000000000000000000000000000..fef60af215d26c0487df81594a2c49f243a79b30 Binary files /dev/null and b/images/MATE.png differ diff --git a/images/graphwalker_example.json b/images/graphwalker_example.json new file mode 100644 index 0000000000000000000000000000000000000000..ee15ec52cf298c4410ecfcdeb563a5d580afa235 --- /dev/null +++ b/images/graphwalker_example.json @@ -0,0 +1 @@ +{"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 diff --git a/images/graphwalker_example.png b/images/graphwalker_example.png new file mode 100644 index 0000000000000000000000000000000000000000..673967b6b5d4fa68aaf476f07660d43cae984e82 Binary files /dev/null and b/images/graphwalker_example.png differ diff --git a/sections/stateoftheart.tex b/sections/stateoftheart.tex index 931e0b2b6f4451b54c8ad20d162b17d2a4328145..05a6dbd5da2474654a4ce49e280b9cfbbcb3045a 100644 --- a/sections/stateoftheart.tex +++ b/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