1.1 --- a/book/src/verification.tex Sat Mar 26 01:46:39 2011 +0100
1.2 +++ b/book/src/verification.tex Mon Mar 28 19:25:26 2011 +0200
1.3 @@ -1,6 +1,6 @@
1.4 \chapter{Verifikation}
1.5 \section{Werkzeugeinsatz}
1.6 -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.\\
1.7 +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.\\
1.8 \begin{table}[h]
1.9 \begin{center}
1.10 \begin{tabular}{cll}
1.11 @@ -20,13 +20,13 @@
1.12 \end{center}
1.13 \end{table}\\
1.14 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.\\\\
1.15 -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.
1.16 +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 entwickelten Code, die generierten Objekte daraus werden auch zur Laufzeit aktiv.
1.17
1.18 \section{Unit-Tests}
1.19 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.20
1.21 Zu den kritischen Modulen gehören u.a. \texttt{VirtualMachine}, \texttt{StackVector} und \newline \texttt{TermFactory}.
1.22 -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.23 +Die \texttt{Virtual"-Machine} beherbergt die zeitbestimmenden 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.24
1.25 \section{Testspezifikation}
1.26 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.
1.27 @@ -58,7 +58,7 @@
1.28 \subsection{Analysewerkzeuge}
1.29 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.
1.30
1.31 -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:
1.32 +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:
1.33 \begin{itemize}
1.34 \item \texttt{dflowlog.py} ist das Basismodul zur Interaktion mit DFLOW-Logs
1.35 \item \texttt{filter.py} dient zum Entfernen nicht relevanter Datensätze
1.36 @@ -66,7 +66,7 @@
1.37 \item \texttt{pushback.py} versetzt Spalteneinträge nach hinten, erleichtert den Einsatz von cutbase.py
1.38 \item \texttt{cutbase.py} entfernt nicht relevante Spalten, als Vorbereitung zur Weiterverarbeitung mit \texttt{gnuplot}
1.39 \end{itemize}
1.40 -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:
1.41 +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, auf den aussagekräftigen Informationsteil reduzierten Form 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-Skripten realisiert:
1.42 \begin{itemize}
1.43 \item \texttt{dml.py} ist das Basismodul zur Interaktion mit DML-Dateien
1.44 \item \texttt{dml2db.py} dient zur Extraktion relevanter DML-Einträge und dem Laden der Daten in die Datenbank
1.45 @@ -85,7 +85,7 @@
1.46 \end{figure}\\
1.47 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.
1.48
1.49 -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.
1.50 +Interessant ist eine kleine Gruppe von abweichenden Zeiten im Bereich (26, -20). 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 an 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.
1.51 \begin{figure}[h]%
1.52 %\centering
1.53 \parbox{6.5cm}{\input{laldo_hist}}%