1.1 --- a/book/src/verification.tex	Thu Mar 24 01:11:45 2011 +0100
     1.2 +++ b/book/src/verification.tex	Thu Mar 24 13:42:41 2011 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  \section{Unit-Tests}
     1.5  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.
     1.6  
     1.7 -Zu den kritischen Modulen gehören u.a. \texttt{VirtualMachine}, \texttt{StackVector} und \texttt{TermFactory}.
     1.8 +Zu den kritischen Modulen gehören u.a. \texttt{VirtualMachine}, \texttt{StackVector} und \newline \texttt{TermFactory}.
     1.9  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.
    1.10  
    1.11  \section{Testspezifikation}
    1.12 @@ -96,7 +96,7 @@
    1.13  \caption[Histogramm von Separationszeiten]{Histogramm von den Separationszeiten an zwei verschiedenen Flow Points. Links: \emph{LALDO}, rechts: \emph{LABTAR}}%
    1.14  \label{fig:1figs}%
    1.15  \end{figure}\\
    1.16 -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.\\\\
    1.17 +Eine wichtige Anmerkung zu der folgenden Auswertung ist, dass die Separations\-beschrä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.\\\\
    1.18  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.
    1.19  
    1.20  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.