1.1 --- a/book/src/verification.tex Tue Mar 29 13:29:50 2011 +0200
1.2 +++ b/book/src/verification.tex Tue Mar 29 13:44:35 2011 +0200
1.3 @@ -23,26 +23,23 @@
1.4 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.5
1.6 \section{Unit-Tests}
1.7 -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.8 -
1.9 +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.10 Zu den kritischen Modulen gehören u.a. \texttt{VirtualMachine}, \texttt{StackVector} und \newline \texttt{TermFactory}.
1.11 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.12
1.13 \section{Testspezifikation}
1.14 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.15
1.16 -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.
1.17 +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.\\\\
1.18 +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.\\\\
1.19 +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.
1.20
1.21 -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.
1.22 -
1.23 -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.\\\\
1.24 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.
1.25
1.26 \section{Testdurchführung}
1.27 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.
1.28
1.29 -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}.
1.30 -
1.31 +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}.\\\\
1.32 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.
1.33
1.34 \section{Effizienz}
1.35 @@ -83,8 +80,7 @@
1.36 \label{fig:atot_etot_atd}
1.37 \end{center}
1.38 \end{figure}\\
1.39 -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.40 -
1.41 +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.42 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.43 \begin{figure}[h]%
1.44 %\centering