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)