Dissertation "Programmanalysen zur Verbesserung der Softwaremodellprüfung".

Abstract: Die Softwarequalität kann mittels Modellprüfung gesteigert werden, indem formale Eigenschaften von Software bzw. davon abgeleitete Modelle verifiziert werden. Die derzeit verfügbaren Modellprüfer sind nicht in der Lage, Quelltexte komplexer Softwareprojekte selbständig, automatisiert und ohne Fehlalarme zu überprüfen. Um Fehlalarme zu reduzieren, wurden präzise Modelle in Form von symbolischen Kellersystemen (SPDS) betrachtet und Verfahren entwickelt, welche die Softwaremodellprüfung verbessern. Da Modellprüfer sehr sensitiv auf die Größe des betrachteten Zustandsraumes reagieren, wurden vorrangig Techniken zu seiner Verkleinerung entworfen, ohne den Wahrheitsgehalt der zu prüfenden Eigenschaften zu verändern. Neben neuen theoretischen Erkenntnissen wurde experimentell gezeigt, dass so in einigen Fällen die Modellprüfung erst ermöglicht wird und in anderen Fällen sich die Modellprüfung sogar ganz erübrigt.

Download: diss.pdf

Anlagen: diss.zip

Mein Buch "Toleranzen in Helsgauns Lin-Kernighan-Heuristik für das TSP" ist nun beim VDM Verlag Dr. Müller erschienen. Es handelt sich um einen Nachdruck meiner Diplomarbeit in einer überarbeiteten und korrigierten Fassung (ISBN 3836494744).

Link bei Amazon: hier.

Inhaltsverzeichnis

• Einführende Erläuterungen
  • Motivation und Vorbemerkungen
  • Das Problem des Handelsreisenden und Varianten
  • Probleminstanzen und Bezugsquellen
  • Transformation von Problemen
• TSP-Heuristiken
  • Klassen von Algorithmen
  • Lokale Suche
    • Swaps bzw. Opts
    • Einfache lokale Suche
    • Wiederholte lokale Suche und Mehrfachstart
    • Komplexität lokaler Suche
  • Klassisches Verfahren von Lin und Kerninghan
    • Kriterien bei der Suche nach k-Swaps
    • Weitere Verbesserungen
  • Modifikationen von Keld Helsgaun
    • Untere Schranke für STSP nach Held und Karp
    • Bestimmung der 1-Baum Toleranz
    • Weitere Modifikationen
    • Anfangstouren
• Toleranzen und Variationen
  • Toleranz bezüglich optimaler Touren
  • Klassifizierung von Toleranzen
  • Verwendete Ressourcen
  • Untersuchte Toleranzen und Variationen
    • Experimentiergrundlage und Einfluss der 1-Baum-Toleranz (SNN vs SLKH)
    • SRX
    • SMTE
    • SMTESOX
    • SSP3AX
    • SSP*AX
    • D2OPT
    • SLAP
    • SLKHDBLBXK(ADJ)(B)
    • SBBXPLKHYT
    • SBBTXPLKHYT
  • Vorhersagequalität statischer Toleranzen
  • Tourqualität und Laufzeit bester Versionen
  • Analysen für VLSI-Beispiele
• Weitere Untersuchungen und Modifikationen
  • MaxMatrixDimension
  • Profiler-Analyse
  • Anfangstouren -- SMTEXPI
• Abschlussbemerkungen
  • Zusammenfassung
  • Ausblick
• Anhang: Tools zur Automatisierung
  • 2collections2excel
  • Best2tex
  • Clear_collection
  • Collcetion2tex
  • ExtractResults4Vgl + GenerateVgl
  • Get_tour_length
  • Import_log2collection
  • Trials2excel + GenerateCharts
• Anhang: Spezifikation des Dateiformats Kollektion
• Literatur
• Abbildungsverzeichnis
• Listings

Im Rahmen meiner Tätigkeit als wissenschaftliche Hilfskraft habe ich zum TSP-Applet von Prof. Sibeyn eine Dokumentation erstellt.

Download: AppletTSP_Doku.pdf

Zu dieser Dokumentation ist eine Übersetzung in Englisch verfügbar (vielen Dank an Sylvia Bongard).

Download: AppletTSP_Doku_eng.pdf

Die aktuelle Version des Applets ist zu finden auf der TSP-Projektseite:
http://www.informatik.uni-halle.de/ti/forschung/toleranzen!

Inhaltsverzeichnis

• Einführung
  • Überblick
    • Problem des Handlungsreisenden
  • Bedienung
• Funktionsweise
• Direkte Tests
  • Einfache Tests
    • Knotenzahltest
    • Kantenzahltest
    • Grad--0--Test
    • Grad--1--Test
    • Zusammenhangstest
    • Brückentest
    • Artikulationspunkttest
  • Tupel--Tests
    • Funktionsweise
    • Durchführung
    • Einzeltest
    • Paartest
    • Tripeltest
    • Quadrupeltest und Pentupeltest
• Graph--Reduktionsstrategien und weitere Tests
  • Knotengrad basierte Reduktion
  • Reduktion nach kleinen Kreisen
  • Eulertest
  • Eulerreduktion
  • Indirekte Kanten--Reduktion
  • Kombinieren von Strategien -- Fixpunktberechnung
• Branch&Bound
  • Branch&Bound für TSP
  • Berechnung einer oberen Schranke
    • Verfahren von Kruskal für minimalen Spannbaum
    • Berechnung einer Greedytour
    • Tourverbessernde Heuristiken und Local-Search
    • Swaps
  • Berechnung einer unteren Schranke
    • Toleranzen
    • MTE-Toleranzen
    • untere Schranke durch MTE-Toleranzen
    • Untere Schranke mit minimalem Spannbaum
    • Iterative Verbesserungen der Schranken
  • Kandidatenwahl -- Branching
    • Branching auf Kanten
    • Branching auf Graphen
• Anhang: Tiefen- und Breitensuche
• Literatur
• Abbildungsverzeichnis