diff --git a/images/anforderungen.pdf b/images/anforderungen.pdf
index 7a7e1d3b64df1942f096dadd0caa1ad5cb30cef2..f071f3df0e5649fd69089c43cb801e1ddedc5c88 100644
Binary files a/images/anforderungen.pdf and b/images/anforderungen.pdf differ
diff --git a/images/konzept.drawio b/images/konzept.drawio
new file mode 100644
index 0000000000000000000000000000000000000000..8de7210c7fa862cbb8963170201e4657441d543b
--- /dev/null
+++ b/images/konzept.drawio
@@ -0,0 +1 @@
+<mxfile host="app.diagrams.net" modified="2021-06-26T11:58:34.441Z" agent="5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/91.0.4472.114 Safari/537.36" etag="Oy6-UVjRcIf5FK2X_SB3" version="14.8.0" type="device"><diagram id="BvBVtmby5S5bfYz1Z3JI" name="Page-1">7VhNc5swEP01PtaDBNhwTJ3U7SFxJk5T+6gBxWhGIEaWA+6vrzDiQwg7boIzk05PYZ+0y+7bfRLOyJ7F+ZyjNLplIaYjaIX5yL4eQQgs25Z/CmRfIg6wSmDDSag2NcCS/MaVp0J3JMRbbaNgjAqS6mDAkgQHQsMQ5yzTtz0zqr81RRtsAMsAURP9RUIRlagHpw3+HZNNVL0ZTPxyJUbVZlXJNkIhy1qQfTOyZ5wxUT7F+QzTgryKl9Lv25HVOjGOE3GOw9PcnwVTtrq/vZuvf0SPi6fn2RcV5QXRnSr48WFxpxIW+4qFbUZiihJpfVUOmAucH80E1PXJwcAsxoLv5Rbl4ClG1EhMlJk1/EJHYVGbW1+BSPV0U0duypYPqvK/YAEaLPxMU4QKv8NEU4MQznZJiIuYQHKSRUTgZYqCYjWTQpBYJGKqls+i7Hh7jvIIXY1Hx+QRuH08Vn6D8zg1eDSIw0l4VchSWgFF2y0JdK5wTsRKPltjmWVprgtTPV/nbWNfGYnMftU21q0Qhd34HazKsUwPh8YZ0BllWQLb8QCfqN1RhxPiG3yqpV5/S1tN6+tZhXFMkSAverp9fVRvuGdEFlJPjO3r0qtnpgpRlqm82odJJ5DT0TCwO7mUPBiBDmNVl/32SfOMSXtYLD9ApacF6QBHZ8UCY9szVQl7VQnHFxOmP4Awa42Np64ms1c0Viu6LWcV46iiBxSmd6YwnX9DmE5HmN1L88LCdIxJuwpRKjB/nzg5E5JelkjTt4YRa/3dUR9hcOz2aHViNn1yqQ8Rd1CdQk2n4EydAk2n8MN0Cj+DTqHrdobG+Zw6nQw4aUC7DlrXw2s3QnMLrFuDd/FJO/dTDf6/EU5OmjSbn6/l9uafAPbNHw==</diagram></mxfile>
\ No newline at end of file
diff --git a/images/konzept.pdf b/images/konzept.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..89de22fc40ab064c122e22dcd3d13577613dda24
Binary files /dev/null and b/images/konzept.pdf differ
diff --git a/images/konzept.svg b/images/konzept.svg
new file mode 100644
index 0000000000000000000000000000000000000000..26bb8fda42f4e1e78bc613b0935aa435bc3cbd2c
--- /dev/null
+++ b/images/konzept.svg
@@ -0,0 +1,3 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" version="1.1" width="641px" height="181px" viewBox="-0.5 -0.5 641 181" content="<mxfile host="app.diagrams.net" modified="2021-06-26T12:12:43.262Z" agent="5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/91.0.4472.114 Safari/537.36" etag="ku7JttpDox93Vf9c3W14" version="14.8.0" type="device"><diagram id="BvBVtmby5S5bfYz1Z3JI" name="Page-1">7VjbcpswEP0aP9aDxMXwmDip25nmMnGaxo8qKIaOjBghxzhfXxHERQgcmuB00umT2UW7ls6eo5WYmPNNtmAoCS9ogMkEGkE2Mc8mEALDNMVP7tkXHgsYhWPNokAOqh3L6AmXkdK7jQKcKgM5pYRHier0aRxjnys+xBjdqcMeKFH/NUFrrDmWPiK690cU8LDwunBW+7/gaB2W/wwcr3izQeVguZI0RAHdNVzm+cScM0p58bTJ5pjk4JW4FHGfe95WE2M45kMC7hbe3J/R++uLy8Xqa3h7dfcw/ySzPCKylQu+vbm6lBPm+xKFdBdtCIqFdSoDMOM4650JqNYniIHpBnO2F0NkgCsRkZRwpLmr8YWW9IVNbMs4JGu6rjLXyxYPcuV/gALUUPieJAjlcc+MJhogjG7jAOc5gcBkF0YcLxPk5293QgjCF/INka8HQdZfnl4coa3gaOk4ArsLxzJudBxnGo4acDgOTnJZCssnKE0jX8UKZxG/F8/GVMyyMFe5KZ/PsqaxL41YzP6+aawaKXK7jnu2ysBiejjQ9oAWlcUS6Jb5+MDaLbk5IbbGh0rqdpe0UbSumpU+hgni0aM63a46yn+4ppFYSMUY01OlV3GmTFEsU0Y1N5NWIqulYWC25lLgoCV6plW17NczzdWYdnO1fAeVHhakBSwFFc+dWjNdlLBTlO7UcI6kS28EXVYSm85sRWUvSKwSdFPNMkevoEfUpTtQl9a/oUurpUuvlejIurQ0pp0EKOGYvU2bjHIBL42F6RnjaLU6dlQ7GJzaHVp19KI7xzqH2KPqFCo6BQN1ChSdwnfTKfwIOoW23SKN9TF16ozINKC0g0Z7eKkj1F1g1SDe0Zk29KQG/3eEEZhWXuSbzBJVXEqTMh7SNY0ROa+9p3VzyGtfj/lGaSKp8gtzvpffC9CW075rxF+h2NBDR89lYDB33tRtgH75X6An/JO+rVeP0JsdMKg3gw75Ha03A/0jgYZTGqIkf3wgOJN752nnNpoKZvBB92C1HR/uxn3X4He8BQ8lPughQLO8Rtc1yRhpe22d/jTeDN5e28fIdqJXb6/CrD8OFsPrT6zm+W8=</diagram></mxfile>"><defs/><g><path d="M 0 23 L 0 0 L 240 0 L 240 23" fill="#ffffff" stroke="#000000" stroke-miterlimit="10" pointer-events="all"/><path d="M 0 23 L 0 180 L 240 180 L 240 23" fill="none" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><path d="M 0 23 L 240 23" fill="none" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><g fill="#000000" font-family="Helvetica" font-weight="bold" pointer-events="none" text-anchor="middle" font-size="12px"><text x="119.5" y="16">TRON</text></g><rect x="25" y="40" width="150" height="125" rx="18.75" ry="18.75" fill="#ffffff" stroke="#000000" pointer-events="none"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 148px; height: 1px; padding-top: 103px; margin-left: 26px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 12px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: none; white-space: normal; word-wrap: normal; ">Uppaal Modell</div></div></div></foreignObject><text x="100" y="106" fill="#000000" font-family="Helvetica" font-size="12px" text-anchor="middle">Uppaal Modell</text></switch></g><path d="M 273 71 L 327.63 70.54" fill="none" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><path d="M 332.88 70.49 L 325.91 74.05 L 327.63 70.54 L 325.85 67.05 Z" fill="#000000" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><rect x="334" y="38.47" width="120" height="128.06" rx="18" ry="18" fill="#ffffff" stroke="#000000" pointer-events="none"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 118px; height: 1px; padding-top: 103px; margin-left: 335px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 12px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: none; white-space: normal; word-wrap: normal; ">ROS</div></div></div></foreignObject><text x="394" y="106" fill="#000000" font-family="Helvetica" font-size="12px" text-anchor="middle">ROS</text></switch></g><path d="M 334 134.51 L 279.37 134.05" fill="none" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><path d="M 274.12 134.01 L 281.15 130.57 L 279.37 134.05 L 281.09 137.57 Z" fill="#000000" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><rect x="180" y="72.5" width="126" height="60" rx="9" ry="9" fill="#ffffff" stroke="#000000" transform="rotate(90,243,102.5)" pointer-events="none"/><g transform="translate(-0.5 -0.5)rotate(90 243 102.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 124px; height: 1px; padding-top: 103px; margin-left: 181px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 12px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: none; white-space: normal; word-wrap: normal; ">Adapter</div></div></div></foreignObject><text x="243" y="106" fill="#000000" font-family="Helvetica" font-size="12px" text-anchor="middle">Adapter</text></switch></g><path d="M 175 71.25 L 206.63 71.04" fill="none" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><path d="M 211.88 71.01 L 204.91 74.55 L 206.63 71.04 L 204.86 67.55 Z" fill="#000000" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><path d="M 213 134 L 181.37 133.79" fill="none" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><path d="M 176.12 133.76 L 183.14 130.3 L 181.37 133.79 L 183.09 137.3 Z" fill="#000000" stroke="#000000" stroke-miterlimit="10" pointer-events="none"/><rect x="530" y="72.5" width="110" height="60" rx="9" ry="9" fill="#ffffff" stroke="#000000" pointer-events="none"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 108px; height: 1px; padding-top: 103px; margin-left: 531px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 12px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: none; white-space: normal; word-wrap: normal; ">Gazebo</div></div></div></foreignObject><text x="585" y="106" fill="#000000" font-family="Helvetica" font-size="12px" text-anchor="middle">Gazebo</text></switch></g><path d="M 473.5 107.5 L 473.5 118 L 454.5 102.5 L 473.5 87 L 473.5 97.5 L 510.5 97.5 L 510.5 87 L 529.5 102.5 L 510.5 118 L 510.5 107.5 Z" fill="none" stroke="#000000" stroke-linejoin="round" stroke-miterlimit="10" pointer-events="none"/></g><switch><g requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"/><a transform="translate(0,-5)" xlink:href="https://www.diagrams.net/doc/faq/svg-export-text-problems" target="_blank"><text text-anchor="middle" font-size="10px" x="50%" y="100%">Viewer does not support full SVG 1.1</text></a></switch></svg>
\ No newline at end of file
diff --git a/images/uppaal_tor.png b/images/uppaal_tor.png
new file mode 100644
index 0000000000000000000000000000000000000000..052f56b3cc10c0877153d765e665af8c624466bd
Binary files /dev/null and b/images/uppaal_tor.png differ
diff --git a/literatur.bib b/literatur.bib
index fb26b59b21f5b7dbced6c3b0b818c5a6b648dc27..9f0b09ab836f9db914b9da5a2b31c6c9fea0f3ed 100644
--- a/literatur.bib
+++ b/literatur.bib
@@ -139,7 +139,7 @@
publisher = {{IEEE}},
doi = {10.1109/ecmr.2015.7324210},
file = {:07324210.pdf:PDF},
- ranking = {rank1},
+ ranking = {rank5},
readstatus = {read},
}
@@ -358,4 +358,14 @@
file = {:2005_Book_Model-BasedTestingOfReactiveSy.pdf:PDF},
}
+@MastersThesis{Gummel2018,
+ author = {Artur Gummel},
+ school = {Tallinn University of Technology},
+ title = {Model-based testing with TestIt: The Robot Operating System Case-Study},
+ year = {2018},
+ file = {:f1d9d4bc9d2143e48f4640b0b2309bf3.pdf:PDF},
+ ranking = {rank5},
+ readstatus = {read},
+}
+
@Comment{jabref-meta: databaseType:bibtex;}
diff --git a/sections/grundlagen.tex b/sections/grundlagen.tex
index 971f16fdc68cdd73b978dae3c5c6ad15fac78395..bd407eaa63905213dd82be96ac539e1c7d5cf96c 100644
--- a/sections/grundlagen.tex
+++ b/sections/grundlagen.tex
@@ -101,7 +101,7 @@ Die Tests ermöglichen ebenfalls eine einfachere Zusammenarbeit der Entwickler,
Die Dokumentation zu ROS erwähnt als Nachteile die Entwicklungs- und Instandhaltungskosten der Teststruktur. Außerdem kann bei Robotersystemen nur eine sehr beschränkte Teilmenge aller Input-Output-Paare getestet werden und der Entwickler muss für jeden Test Kriterien angeben, um festzulegen, wann ein Test als erfolgreich oder fehlgeschlagen gilt. Die Komplexität sorgt auch dafür, dass Abhängigkeiten verschiedener Inputs voneinander nur schwer überprüft werden können.\cite{Pueschel2018}
Als weiterer Nachteil kann gesehen werden, dass bei dieser Vorgehensweise nur die Nodes getestet werden und nicht der gesamte Roboter, wie in \cite{Bihlmaier2014} vorgeschlagen.
-\subsection{Modell-basiertes Testen}
+\subsection{Modell-basiertes Testen}\label{grundlagen:testentwicklung:modell-basiert}
Das Modell-basierte Testen wie in \cite{Pueschel2018} beschreibt einen Ansatz zum automatischen Generieren von Tests, welcher auf allen Ebenen des hierarchischen Testmodells angewandt werden kann. Dabei wird ein abstraktes Modell des Testobjektes erstellt, von dem die Tests abgeleitet werden können. Wichtig hierbei ist, dass das Modell eine gewisse Unabhängigkeit von Modellen besitzt, die zur Entwicklung genutzt wurden, da sich ansonsten Fehler aus dem Entwicklungsmodell in die Testfälle übertragen könnten. Es bietet sich daher an, das Modell direkt aus den Anforderungen des Systems zu entwickeln; das Entwicklungsmodell kann als Basis verwendet werden, oder um das Testmodell zusätzlich zu validieren.\cite{Utting2011}
Da das Modell von Implementierungsdetails unabhängig ist, eignet sich Modell-basiertes Testen nicht für white box Tests. Der in \cite{Pueschel2018} dargestellte Testprozess besteht aus 5 Schritten:
\begin{enumerate}
@@ -111,8 +111,8 @@ Da das Modell von Implementierungsdetails unabhängig ist, eignet sich Modell-ba
\item Folglich werden die Tests ausgeführt.
\item Die Ergebnisse werden analysiert, Fehler gefunden und behoben.
\end{enumerate}
-Diese Methode der Testentwicklung ermöglicht erhebliche Einsparungen beim Entwicklungsaufwand, besonders bei Änderungen im Modell können ohne viel Aufwand neue Testfälle generiert werden. Die Anzahl an Testfällen lässt sich einfach anpassen, wodurch mehr Fehler gefunden werden können.\cite{Pretschner2005}
+Diese Methode der Testentwicklung ermöglicht erhebliche Einsparungen beim Entwicklungsaufwand, besonders bei Änderungen im Modell können ohne viel Aufwand neue Testfälle generiert werden. Die Anzahl an Testfällen lässt sich einfach anpassen, wodurch mehr Fehler gefunden werden können und eine bessere Abdeckung gegeben ist.\cite{Pretschner2005}
Als weiterer Vorteil ist bei dieser Methode anzugeben, dass das zu erstellende Modell (neben der Generierung der Testfälle) einen Überblick über die Funktionsweise basierend auf den Anforderungen des Systems gibt, sodass (neue) Entwickler dieses potentiell besser verstehen und daran arbeiten können. Nachteilig lässt sich anmerken, dass sich eine gewisse Redundanz zwischen dem zum Testen genutzten Modell und den Modellen zur Entwicklung nicht vermeiden lässt.\cite{Pueschel2018}
-In \cite{Utting2011} wird eine Klassifizierung von möglichen Modellen für Modell-basiertes Testen vorgenommen, unter anderem lassen sich Markov-Ketten, endliche Automaten oder Petri-Netze zur Modellierung nutzen. Da Modelle, deren Umfang sich nur auf Inputs bezieht, kaum funktionales Verhalten verifizieren können sollten für cyber-physische Systeme Input-Output-Modelle verwendet werden. Die Echtzeitanforderungen eines Systems müssen im Modell widergespiegelt werden und spielen folglich auch bei der Testgenerierung und Ausführung eine Rolle.\cite[S. 358f]{Broy2005} Robotiksysteme sollten sich meist deterministisch verhalten, aufgrund des in \cref{grundlagen:simulationen} beschriebenen Nichtdeterminismus der Simulation oder uneindeutiger Inputs kann aber auch ein nichtdeterministisches Modell verwendet werden; sollen auch nichtdeterministische Systemfunktionalitäten überprüft werden, so ist ein deterministisches Modell offensichtlich nicht sinnvoll. Die Dynamik des Modells muss abhängig von den zu testenden Anforderungen sein, meist sind Robotiksystemen als kontinuierlich oder hybrid (Mix aus kontinuierlichen und diskreten Eigenschaften) einzustufen. Das Paradigma des Modells sowie das Testauswahlkriterium müssen bei der Entwicklung ausgewählt werden, da sie stark von den zu testenden Anforderungen abhängen. Allerdings werden häufig verschiedene dieser Paradigmen verwendet, da sich verschiedene vereinigen lassen. Bezüglich des Testauswahlkriteriums und der Testgenerierungstechnik können ebenfalls mehrere verwendet werden.\cite{Utting2011}
+In \cite{Utting2011} wird eine Klassifizierung von möglichen Modellen für Modell-basiertes Testen vorgenommen, unter anderem lassen sich Markov-Ketten, endliche Automaten oder Petri-Netze zur Modellierung nutzen. Da Modelle, deren Umfang sich nur auf Inputs bezieht, kaum funktionales Verhalten verifizieren können sollten für cyber-physische Systeme Input-Output-Modelle verwendet werden. Die Echtzeitanforderungen eines Systems müssen im Modell widergespiegelt werden und spielen folglich auch bei der Testgenerierung und Ausführung eine Rolle.\cite[S. 358f]{Broy2005} Robotiksysteme sollten sich meist deterministisch verhalten, aufgrund des in \cref{grundlagen:simulationen} beschriebenen Nichtdeterminismus der Simulation oder uneindeutiger Inputs kann aber auch ein nichtdeterministisches Modell verwendet werden; sollen auch nichtdeterministische Systemfunktionalitäten überprüft werden, so ist ein deterministisches Modell offensichtlich nicht sinnvoll. Die Dynamik des Modells muss abhängig von den zu testenden Anforderungen sein, meist sind Robotiksystemen als kontinuierlich oder hybrid (Mix aus kontinuierlichen und diskreten Eigenschaften) einzustufen. Das Paradigma des Modells sowie das Testauswahlkriterium müssen bei der Entwicklung ausgewählt werden, da sie stark von den zu testenden Anforderungen abhängen. Allerdings werden häufig verschiedene dieser Paradigmen verwendet, da sich verschiedene vereinigen lassen. Bezüglich des Testauswahlkriteriums und der Technik zum Generieren der Tests können ebenfalls mehrere verwendet werden.\cite{Utting2011}
diff --git a/sections/konzept.tex b/sections/konzept.tex
index b9170020bc721188829da696ed5619b7a1e2dfa2..8a9a38aea869a0ea654f1345d0c2e8a682b0ca47 100644
--- a/sections/konzept.tex
+++ b/sections/konzept.tex
@@ -1 +1,28 @@
\chapter{Konzept}
+Aufgrund der genannten Vorteile von Modell-basiertem Testen wird dieses im folgenden umgesetzt. Zur Modellierung wird Uppaal\footnote{\url{https://uppaal.org/}} genutzt, eine Erweiterung namens TRON\footnote{\url{https://people.cs.aau.dk/~marius/tron/}} (Testing Realtime Systems Online) ermöglicht die Testgenerierung und direkte Ausführung aus dem erstellten Modell, indem ein Adapter erstellt wird. Als Vorbild dienen \cite{Ernits2015, Gummel2018}.
+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}
+\cref{konzept:bild} zeigt den schematischen Aufbau der Implementierung.
+
+\begin{figure}[h]
+ \centering
+ \includegraphics[scale=.8]{./konzept.pdf}
+ \caption{Aufbau der Testmethode}
+ \label{konzept:bild}
+\end{figure}
+
+\section{Modell in Uppaal}
+Ein System in Uppaal besteht aus einem oder mehreren Automaten. Sogenannte Channel und global deklarierte Variablen sorgen für eine Synchronisation dieser. Die Automaten selbst sind als erweiterte endliche nicht-deterministische Automaten einzuordnen. 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. Invarianten können global oder nur in bestimmten Zuständen angegeben werden. \cref{konzept:uppaal_tor} zeigt beispielhaft ein modelliertes System.
+\begin{figure}[h]
+ \centering
+ \includegraphics[scale=.4]{./uppaal_tor.png}
+ \caption{zeigt ein Modell 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 "auslösen" informiert, wechselt in den Zustand "oeffnend" und setzt die Variable "zeit" auf 0. Nach 10000 vergangenen Zeiteinheiten wechselt das Tor dann in den Zustand "offen". Das Schließen läuft analog dazu ab.}
+ \label{konzept:uppaal_tor}
+\end{figure}
+
+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 an.
+Folglich kann das Systemverhalten modelliert werden.
+Zur Verifizierung des Modells können die Inputs in das System ebenfalls modelliert werden und so innerhalb von Uppaal eine Simulation stattfinden. 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 werden zur Verifizierung beitragen.
+
+\section{Testgenerierung mit TRON}