Seminar: Modellbasierte Software-Verifikation: Grundlagen und industrielle Praxis

Lehrstuhl Technische Informatik
Dozenten Prof. Dr. habil. Kropf
Dr. Ruf
Betreuer Dr. Ruf
Dr. Lämmermann
Prof. Dr. habil. Kropf
Heckeler
Vorbesprechung         22.04.2010, 17:00 Uhr, A302
Umfang 2 SWS / 4 LP
Prüfungsfach      Technische Informatik
Eintrag im LSF Modellbasierte Software-Verifikation: Grundlagen und industrielle Praxis

Beschreibung

Zuverlässigkeit, Sicherheit, Korrektheit und Robustheit von Software werden immer wichtiger. Immer wieder treten Fehler auf, darunter auch kritische, die auf gedanklich-logische Irrtümer in Spezifikation und Implementierung der Software zurückzuführen sind. Dabei spielen Compiler und Systemsoftware eine ebenso wichtige Rolle wie die verwendeten Softwaretechniken und Programmiersprachen. Zur Vermeidung von Fehlern werden die verwendeten Sprachen oft in den erlaubten Sprachkonstrukten eingeschränkt, um z.B. dynamische Fehlfunktionen (Speicherüberläufe, Speicherlecks u.ä.) zu verhindern, aber auch, um die Analyse und Verifikation zu vereinfachen.
Die Verifikations-Techniken reichen dabei von der statischen Analyse der Programme und deren  Spezifikation bis hin zu Kombinationen aus maschinellen Beweissystemen und Model-Checkern. Neben Fehlervermeidung ist auch Fehlertoleranz (z.B. durch Redundanz, Mehrfachauslegung) für Software ein interessanter Ansatz. Dazu werden Techniken, wie Laufzeitprüfung, Beobachterprozesse, Monitoring, Konsistenzprüfung eingesetzt.
Mehr und mehr stehen Qualitätsprüfung und die Garantie zur Einhaltung von Eigenschaften bei Software im Vordergrund. Ein Beispiel wäre z.B. die Zertifizierung sicherheitsrelevanter Systeme. In diesem Zusammenhang sind auch Bibliotheken, Werkzeuge, Compiler, Systemkomponenten und Fremdsoftware von Bedeutung, für die die Hersteller ebenfalls verantwortlich sind. Die Beherrschung dieser komplexen Zusammenhänge ist nicht nur für Systeme relevant, von denen Gefahr für Leib und Leben von Menschen ausgeht, sondern auch bei wirtschaftlichem Gefahrenpotential Software-basierter Systeme, z.B. im Bereich der Security.

Ziel dieses Seminars ist es einen Einblick in die Theorie der Software-Verifikation und die aktuellen, in der Forschung entwickelten, Tools zu geben, ohne den Fokus auf die heute eingesetzten industriellen Methoden zu verlieren.

Die Dozenten haben einschlägige Erfahrungen im Entwurf und der Verifikation von Systemen im industriellen Umfeld.

 

Themenvergabe:

Die Themenvergabe erfolgt am 22.04.2010. Außerdem werden an diesem Tag auch die weiteren Termine für das Block-Seminar bekanntgegeben.

Bemerkung

Randbedingungen fürs Seminar

Von den Teilnehmerinnen und Teilnehmnern wird eine weitgehend selbstständige Erarbeitung des jeweiligen Themengebiets incl. Literaturbeschaffung und -recherche erwartet. Literaturhinweise werden natürlich gegeben, eine bedarfsgesteuerte Betreuung ist sichergestellt.

Vortragsdauer und Themenaufbau

Der Vortrag soll einen Dauer von 25 Minuten haben und folgenden Aufbau besitzen:

  • Einleitung mit Motivation (ca. 5 Minuten im Vortrag)
  • Theorie zum jeweiligen Thema (ca. 10-15 Minuten im Vortrag)
  • Praktische Anwendung / Fallbeispiele (restliche Zeit, mind. 5. Minuten)
  • Zusammenfassung (2 Minuten im Vortrag)
Bedingungen für den Seminarschein / Benotung

Um den Schein zu erhalten muss

  • eine Vortragsgliederung 4 Wochen vor dem Vortragstermin mit dem Betreuer durchgesprochen sein
  • eine erste Vortragsversion 2 Wochen vor dem Vortragstermin mit dem Betreuer durchgesprochen sein (vorzugsweise PowerPoint oder PDF)
  • ein Vortrag (25 Minuten + Diskussion) gehalten werden
  • eine schriftliche Ausarbeitung abgegeben werden (5-10 Seiten in PostScript- oder PDF-Format)
  • bei allen Seminarterminen anwesend sein

Die Seminarleistung wird auf Wunsch benotet. Zur Bewertung werden folgende Kriterien herangezogen:

  • Einhaltung der Termine
  • Qualität der durchgeführten Literaturrecherche
  • Inhaltliche Qualität des Vortrags
  • Qualität der Präesntation incl. Zeiteinhaltung
  • Qualität der Ausarbeitung
  • Grad der Sebstständigkeit (davon unberührt sind natürlich Diskussionen mit dem Betreuer über Auswahl der zu präsentierenden Themen, Eignung zur Präsentation etc. - solche Diskussionen sind sogar explizit erwünscht)