Seminar: Modellbasierte Software-Verifikation: Grundlagen und industrielle Praxis

Lehrstuhl Technische Informatik
Dozenten Prof. Dr. habil. Kropf
Dr. Ruf
Betreuer Dr. Ruf
Prof. Dr. habil. Kropf
Heckeler
Vorbesprechung         19.04.2012, 17:00 Uhr, A104
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 19.04.2012 in Raum A104 um 17:00 Uhr. Außerdem werden an diesem Tag auch die weiteren Termine fĂŒr das Block-Seminar bekanntgegeben.

Themen

  1. Boogie - A Modular Reusable Verifier for Object-Oriented Programs (Paper): Dieses Paper beschreibt die Architektur einer modernen Plattform zur Verifikation von objektorientierter Software, wie sie z.B. bei Spec# verwendet wird. Besonders deutlich wird das hier der Weg vom Quellcode ĂŒber Logik bis hin zum formalen Beweis erklĂ€rt.
  2. Why3 - Where Programs Meet Provers (Tutorial): Why3 ist eine Verifikationsplattform fĂŒr den formalen Beweis aussagenlogischer Formeln. In dem Tutorial geht es darum sich mit der Plattform vertraut zu machen und    EigenstĂ€ndig kleinere Formeln und Programme zu verifizieren.
  3. EMMA - a free Java code coverage tool (Tutorial): EMMA ist ein freies Werkzeug zur DurchfĂŒhrung unterschiedlicher Abdeckungsanalysen (Coverage). In diesem Tutorial geht es darum, erste Erfahrungen mit EMMA zu sammeln. Dies beinhaltet mehrere unterschiedliche Coverage-Techniken, unterschiedliche Ausgabeformate u.v.m. Es sollen eigenstĂ€ndig Coverage-Analysen mit kleinen Beispiel-Programmen durchgefĂŒhrt werden.
  4. Modeling and Analysis of Exception Handling by Using UML Statecharts (Paper): Dieses Paper beschreibt einen Framework zur Modellierung von Ausnahmebehandlungen. Dadurch können diese automatisch mit Hilfe von Model Checking geprĂŒft werden.
  5. Spezielle dynamische Testtechniken (Buchkapitel): Dieses Buchkapitel geht auf spezielle Testformen wie z.B. Mutationen-Tests, Regressionstests und Zufallstests ein.
  6. Modellbasiertes Testen (Buchkapitel): Modellbasiertes Testen ist ein vieldiskutiertes Thema. Das Kapitel beschriebt unterschiedliche Modellarten und deren Anwendung zu Testzwecken.
  7. Softwaremessung (Buchkapitel): Mit Messungen in der Softwaretechnik werden die gleichen Ziele verfolgt, die Messtechnik in anderen Bereichen auszeichnen. Mit Hilfe der Messungen und den zugehörigen Metriken soll vor allem TestqualitÀt bewertet werden.
  8. Bounded Model Checking of C and C++ Programs Using a Compiler IR (Tutorial): Dieses Paper beschreibt die Verwendung des neuen BMC Tools LLBMC. Mit diesem soll es nun auch möglich sein nicht-triviale C++ Programme zu verifizieren. Hier sollte der Workflow aufgebaut und die Möglichkeiten beleuchtet werden.
  9. PaMiraXT - Parallel SAT Solving with Threads and Message Passing (Paper): Das Paper stellt einen Algorithmus bereit mit dem es möglich ist ein SAT Problem auf mehrere Threads zu verteilen. Diese Methoden sollen analysiert und dargestellt werden.

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 (6-8 Seiten in PostScript- oder PDF-Format)
  • bei allen Seminarterminen anwesend sein

Die Seminarleistung wird nach folgenden Kriterien benotet:

  • 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)

 

Powerpoint-Vorlagen

PPT oder PPTX

Latex- und Word-Vorlage

Latex oder Word

Tips zur Gestalltung von Vortrag und Ausarbeitung

PDF-Anleitung