@@ -23,6 +23,7 @@ Ein System in Uppaal besteht aus einem oder mehreren Automaten. Sogenannte Chann
...
@@ -23,6 +23,7 @@ Ein System in Uppaal besteht aus einem oder mehreren Automaten. Sogenannte Chann
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.
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.
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.
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 werden zur Verifizierung beitragen.
\section{Testgenerierung mit TRON}
\section{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 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.
