
sawine@1: \chapter{Verifikation}
sawine@1: \section{Werkzeugeinsatz}
sawine@1: Nach Beendigung der Entwicklungsphase, war man in der Lage ein Fazit über die Qualität der eingesetzten Werkzeuge zu stellen. Deren Einsatz wurde hinsichtlich der Effektivitätssteigerung bewertet. Tabelle \ref{auto_gen_loc} bietet eine quantitative Übersicht über die Komplexität der entwickelten Komponenten.\\
sawine@1: \begin{table}[h]
sawine@1: \begin{center}
sawine@1: \begin{tabular}{cll}
sawine@1: \toprule
sawine@1: \textbf{Komponente}				& \textbf{Lines of Code}	& \textbf{autogenerierter Anteil}\\
sawine@1: \midrule
sawine@1: \texttt{flex}-Konfiguration		& 84						& -\\
sawine@1: \texttt{bison}-Konfiguration	& 348						& -\\
sawine@1: {autogeneriert}					& 4188 						& -\\
sawine@1: {ATCCL}							& 13741 					& 30\%\\
sawine@1: {DFLOW}							& 5796						& 0\%\\
sawine@1: Gesamt							& 19537						& 21\%\\
sawine@1: \bottomrule
sawine@1: \end{tabular}
sawine@1: \caption{Anteil an automatisch generiertem Code}
sawine@1: \label{auto_gen_loc}
sawine@1: \end{center}
sawine@1: \end{table}\\
sawine@1: Das ATCCL-Framework ist in Codezeilen bemessen der Schwerpunkt der Entwicklung gewesen. Mit einem Konfigurationsaufwand von 432 Zeilen Code, wurde mit Hilfe von \texttt{flex} und \texttt{bison} rund 30\% des ATCCL-Frameworks generiert. Die quantitative Auswertung beinhaltet nicht die hohe Komplexität einer Parsergenerierung und der notwendigen Testprozeduren, um die Fehlerfreiheit des Parsers zu gewährleisten. Zusammenfassend kann man behaupten, mit dem Einsatz der Parsergeneratoren eine enorme Steigerung der Produktivität erzielt zu haben.\\\\
sawine@1: Nach \cite{code_gen} bietet der Einsatz von Codegeneratoren auch beim Zertifizierungsprozess einen Vorteil gegenüber manuell entwickeltem Code. Bei dem ATCCL-Framework wird die Zertifizierung der Parsergeneratoren nicht notwendig sein, da der automatisch generierter Code ausschließlich im Compiler-Front-End zum Einsatz kommt. Das Front-End ist für die Syntax- und Semantikanalyse zuständig, welche nur bei der Initialisierung durchgeführt werden. Fehlverhalten in der Initialisierungsphase bedeutet keine Gefährdung der Sicherheit, solange diese erfolgreich erkannt werden und somit die operative Phase verhindert wird. Die Synthese erfolgt durch manuell entwickeltem Code, die generierten Objekte daraus werden auch zur Laufzeit aktiv.
sawine@1: 
sawine@1: \section{Unit-Tests}
sawine@1: Während der Implementierungsphase wurden für die C++-Klassen Unit-Tests erstellt, die das Verhalten der Einheiten gegen die Anforderungen prüfen. Mit Hilfe von Über"-deckungs"-diagnosen werden nicht ausreichend getestete Module lokalisiert und die ungeprüften Bereiche mit weiteren Tests belegt.
sawine@1: 
sawine@1: Zu den kritischen Modulen gehören u.a. \texttt{VirtualMachine}, \texttt{StackVector} und \texttt{TermFactory}.
sawine@1: Die \texttt{Virtual"-Machine} beherbergt die zeit-bestimmenden Algorithmen und muss deshalb besonders intensiv getestet werden. Hier ist nicht nur die Korrektheit der Ergebnisse relevant, sondern auch die Laufzeiten der Berechnungen, mehr dazu in Abschnitt \ref{verification:efficiency}. Die StackVector-Klasse dient als Standardklasse für eine Reihe von Situationen, Fehler in dieser Klasse würden Konsequenzen für eine Reihe von Modulen haben. Die TermFactory ist als objekterzeugende Einheit wegen der dynamischen Speicherallokierung kritisch. Gleichzeitig bieten die Tests dieser Klasse eine unmittelbare Prüfung für neu integrierte Property-Klassen.
sawine@1: 
sawine@1: \section{Testspezifikation}
sawine@1: Die Testspezifikation -- auch System Test Description -- wird analog zu dem SRS\footnote{System Requirements Specification -- Dokument zur Spezifikation der Systemanforderungen} entwickelt. Jeder Test hat mindestens eine Anforderung abzudecken, alle Anforderungen müssen mindestens in einem Test verifiziert werden.
sawine@1: 
sawine@1: Die Testspezifikation beschreibt unabhängige Tests. Ein Test besteht aus einer Vorbereitungssequenz und den Testschritten. Jeder Test muss die getesteten Anforderungen und die zu testende Version der Software referenzieren.
sawine@1: 
sawine@1: Ein Testschritt beschreibt eine Aktion und den erwarteten Effekt. Tritt dieser Effekt nicht auf, oder ist die Durchführung der Aktion nicht möglich, gilt der Testschritt als fehlgeschlagen. Bei Fehlschlag findet eine Gewichtung des Fehlers statt, die in Abhängigkeit von der Priorität der getesteten Anforderung und der Art des Fehlereffekts ermittelt wird.
sawine@1: 
sawine@1: Am Ende des Tests wird ermittelt ob der Durchlauf erfolgreich war. Sind während des Durchlaufs Fehler aufgetreten, hängt die Gesamtbewertung von der Gewichtung und Anzahl der Fehler ab.\\\\
sawine@1: Die Granularität der Testabdeckung spielt eine entscheidende Rolle bei der Effektivität der Testläufe. Ist diese zu hoch, entstehen möglicherweise viele redundante Testschritte, die einen Testdurchlauf unnötigerweise verlangsamen. Deckt man hingegen zu viele Anforderungen mit einem Test ab, so erschwert es die Lokalisierung des Fehlverhaltens.
sawine@1: 
sawine@1: \section{Testdurchführung}
sawine@1: Die Tests werden entsprechend der STD\footnote{System Test Description -- Dokumentation der Systemtestprozeduren} durchgeführt. Für die Durchführung der Tests sind die Testingenieure des Testteams verantwortlich.
sawine@1: 
sawine@1: Die Verifizierungstests werden bei jeder neuen Softwareversion durchgeführt. Bei verteilten Systemen kann eine Komponente Einfluss auf andere Komponenten haben, in diesem Fall müssen alle in Verbindung stehenden Komponenten auch getestet werden, dies sind die sog. \emph{Regression Tests}\footnote{Testprozeduren, die mit jeder neuen Version wiederholt durchgeführt werden, um alle in Abhängigkeit stehenden Komponenten auf ihre Korrektheit zu überprüfen}.
sawine@1: 
sawine@1: Da das ATCCL-Framework eine eigenständige Library ist, ist diese größtenteils unabhängig von anderen Modulen und muss nur bei neuen Versionen getestet werden. Die DFLOW-Kom"-ponente hingegen ist in das FDPS integriert. Bei jeder Aktualisierung des FDPS oder einer Komponente, die in Verbindung mit dem FDPS steht, muss auch DFLOW neu verifiziert werden.
sawine@1: 
sawine@1: \section{Effizienz}
sawine@1: \label{verification:efficiency}
sawine@1: Beansprucht das DFLOW zu viel Bearbeitungszeit für eine Anfrage, so kann es den Betrieb eines Planers stören. Eine höhere Belastung als bei der manuellen Eingabe ist die automatische Übernahme von Überflügen in das DFLOW-System. Da die Komplexität der Bearbeitung in der virtuellen Maschine des ATCCL-Frameworks liegt, muss diese auf ihre Leistungsfähigkeit geprüft werden.
sawine@1: 
sawine@1: Zum Testen der Performance der virtuellen Maschine wurde eine Reihe von Worst-Case-Szenarien mit Hilfe von Unit-Tests entwickelt und diese auf einer GCC-optimierten Version ausgeführt. Dafür wurden Flugplanmuster mit unwahrscheinlichen und sehr vielen Kombinationen gewählt. Die Testdurchläufe wurden auf Systemen durchgeführt, die auch beim Kunden in Einsatz kommen.\\\\
sawine@1: Die Evaluation ergab einen Mittelwert von 11 µs pro Auswertung eines Flugplanmusters, was bei der Evaluation von 3000 Flugplänen eine Gesamtzeit von 33 ms ergibt. Im Realbetrieb werden sich maximal 1000 bis 1500 Flugpläne zum gleichen Zeitpunkt im System befinden, bei einem Umsatz von ca. 150 pro Stunde.
sawine@1: 
sawine@1: \section{Leistungsanalyse}
sawine@1: Das Ziel der DFLOW-Komponente bestand in der Optimierung der Abflugplanung unter Berücksichtigung der Luftraumbeschränkungen. Nach der erfolgreichen Realisierung aller Anforderungen, galt es die Leistung der Komponente im operativen Betrieb zu bewerten.
sawine@1: 
sawine@1: \subsection{Analysewerkzeuge}
sawine@1: Die Bewertung basiert auf den von DFLOW erstellten Logdaten und den DMAP-Transaktions"-protokollen. Die DFLOW-Logs enthalten einen Eintrag für jeden erfassten Starter, während die \emph{Daily Movement Logs} -- kurz DML -- alle Flüge innerhalb des kontrollierten Gebiets protokollieren.
sawine@1: 
sawine@1: Durch die detaillierte Protokollführung, entstehen große Datenmengen. Die tägliche Datenmenge misst im Durchschnitt ca. 350 kB für die DFLOW-Logs, 6 MB für die DMLs und 60 MB für die DMAP-Transaktionen. Um eine Analyse dieser Daten zu ermöglichen, wurden \emph{Python}\footnote{Eine dynamische, höhere Programmiersprache, der gute Lesbarkeit attestiert wird -- wird durch die hohe Abstraktion und weite Verbreitung oft als Skriptsprache eingesetzt}-Skripte entwickelt. Die Skripte dienen der Vorverarbeitung der Datensätze, im Detail:
sawine@1: \begin{itemize}
sawine@1: \item \texttt{dflowlog.py} ist das Basismodul zur Interaktion mit DFLOW-Logs
sawine@1: \item \texttt{filter.py} dient zum Entfernen nicht relevanter Datensätze
sawine@1: \item \texttt{analyse.py} bietet mehrere Auswertemöglichkeit, u.a. Differenzenbildung von Zeiten und Ermittlung der zeitlichen Separation der individuellen Flüge
sawine@1: \item \texttt{pushback.py} versetzt Spalteneinträge nach hinten, erleichtert den Einsatz von cutbase.py
sawine@1: \item \texttt{cutbase.py} entfernt nicht relevante Spalten, als Vorbereitung zur Weiterverarbeitung mit \texttt{gnuplot}
sawine@1: \end{itemize}
sawine@1: Zusätzlich wurde nach dem Prinzip des \emph{Data-Warehouse} eine \emph{MySQL}\footnote{Ein Open-Source-Datenbankmanagementsystem}-Datenbank angelegt. In die Datenbank wurden Daten, in aufbereiteter und auf den aussagekräftigen Informationsteil reduziert, aus den verschiedenen Protokollquellen importiert. Die Datenbank bietet eine Möglichkeit mit SQL-Abfragen dynamische Auswertungen und Zusammenhänge zwischen verschiedenen Datensätzen zu bilden. Die Extraktion, Transformation und das Laden in die Datenbank wurde mit einem weiteren Python-Skript realisiert:
sawine@1: \begin{itemize}
sawine@1: \item \texttt{dml.py} ist das Basismodul zur Interaktion mit DML-Dateien
sawine@1: \item \texttt{dml2db.py} dient zur Extraktion relevanter DML-Einträge und dem Laden der Daten in die Datenbank
sawine@1: \end{itemize}
sawine@1: \subsection{Datensatz}
sawine@1: Die Analysen basieren auf den Aufzeichnungen von 1. Januar bis zum 8. April 2010. Der Datensatz basiert auf den Logdaten eines von mehreren FDPS-Servern. Da die Server in einem redundanten System agieren und die aktuellen Daten zum Zeitpunkt der Analyse noch nicht zusammengeführt waren, waren keine absoluten Bewertungen der Daten möglich, wie z.B. hinsichtlich der Verkehrsflussdichten. 
sawine@1:  
sawine@1: \subsection{Auswertung}
sawine@1: Abbildung \ref{fig:atot_etot_atd} zeigt die Verteilung der Differenz zwischen der frühesten Abflugzeit \emph{ETOT} und der von DFLOW vergebenen Abflugzeit \emph{ATOT}. Die Gegenüberstellung mit der Differenz der vergebenen Abflugzeit und der tatsächlichen Abflugzeit soll die Konformität der Abflugplanung mit der DFLOW-Vergabe visualisieren.\\
sawine@1: \begin{figure}[h]
sawine@1: \begin{center}
sawine@1: \input{atot_etot_atd}
sawine@1: \caption{Abflugzeitkonformität}
sawine@1: \label{fig:atot_etot_atd}
sawine@1: \end{center}
sawine@1: \end{figure}\\
sawine@1: Die Analyse der rund 1800 Flüge ergab, dass die vergebenen Zeiten zum größten Teil sehr strikt eingehalten werden. Man sieht eine starke Konzentration um den Nullpunkt auf der X-Achse. Die Streuung beschränkt sich, bis auf wenige Ausnahmen, auf eine Abweichung von $\pm$3 Minuten. 
sawine@1: 
sawine@1: Interessant ist eine kleine Gruppe von abweichenden Zeiten im Bereich (-20, 25). Die Flüge in diesem Bereich wurden zur Einhaltung der Separationsregeln um rund 25 Minuten zeitlich versetzt. Die tatsächliche Abflugzeit liegt jedoch 20 Minuten vor der vergebenen Zeit, also unmittelbar nach der frühesten Abflugzeit. Die Entscheidung der Planer die vergebene Zeit nicht zu übersteuern und trotzdem den frühzeitigen Abflug zu gestatten, mag in der Funktion von DFLOW liegen, solche Verletzungen der Abflugslots visuell zu signalisieren. Sowohl der Planer an der AWP als auch der Fluglotse an der CWP werden durch eine definierte Zeichenkette über die Abweichung informiert und diesen Flügen besondere Aufmerksamkeit bei der Eingliederung in den Luftverkehr widmen.
sawine@1: \begin{figure}[h]%
sawine@1: %\centering
sawine@1: \parbox{6.5cm}{\input{laldo_hist}}%
sawine@1: \qquad
sawine@1: \begin{minipage}{1.2in}%
sawine@1: \input{labtar_hist}
sawine@1: \end{minipage}%
sawine@1: \caption[Histogramm von Separationszeiten]{Histogramm von den Separationszeiten an zwei verschiedenen Flow Points. Links: \emph{LALDO}, rechts: \emph{LABTAR}}%
sawine@1: \label{fig:1figs}%
sawine@1: \end{figure}\\
sawine@1: Eine wichtige Anmerkung zur folgenden Auswertung ist, dass die Separationsbeschränkungen auf Zeiträume mit hohem Verkehrsaufkommen gelegt werden. Da in diesen Zeiträumen der Großteil des täglichen Flugverkehrs abgehandelt wird, hat dies Auswirkung auf die Statistik.\\\\
sawine@1: Flow Point \emph{LALDO} umfasst zwei Wegpunkte und definiert in der Summe ca. 6 Stunden am Tag eine zeitliche Separation von 3 Minuten. Die Statistik belegt diesen Zustand und die erfolgreiche Funktion des DFLOW: für über 54\% der erfassten Flüge wurde von DFLOW eine Separation von 3 Minuten geplant. Die größeren Separationen zwischen 3 und 10 Minuten sind ein Zeichen dafür, dass der Flow Point noch freie Kapazitäten besitzt. Zum Vergleich weist \emph{LABTAR} im Durchschnitt eine höhere Verkehrsflussdichte von 29\% auf.
sawine@1: 
sawine@1: Auch für den Flow Point \emph{LABTAR} sind zwei Wegpunkte für die Separation definiert. Die Separationskonfiguration für diesen Flow Point ist differenzierter und umfasst mehrere Zeiträume mit unterschiedlichen Zeiten. Rund 7,5 Stunden pro Tag gilt eine Separation von 5 Minuten, während ca. 1,5 Stunden eine zeitliche Separation von 3 Minuten gewährleistet werden soll. Das Histogramm zeigt dieses Verhalten mit den beiden größten Ausschlägen, 70\% der Separationszeiten liegen bei 5 Minuten und 10\% bei 3 Minuten.
sawine@1: 
sawine@1: 
sawine@1: 




