Seminar Modellbasierte Software-Verifikation: Grundlagen und industrielle Praxis

Arbeitsbereich Technische Informatik
Dozent Prof. Thomas Kropf mit Dr. J├╝rgen Ruf und Mitarbeitern
Umfang 2 SWS / 4 LP
Bereiche Diplom, Master und Bachelor (empfohlenes Semester: 6ff)
Pr├╝fungsf├Ącher Technische Informatik
Raum Seminarraum 2 F118
Vorbesprechung Donnerstag, 17 April 2008, 17:00 c.t., Sand 13 - A302
Termine Blockveranstaltung, Do. 17. Juli 2008, 17:00 c.t., Raum A104
Sprechstunde nach Vereinbarung
Kontakt/Anmeldung behrend(at)informatik.uni-tuebingen(dot)de
Eintrag im LSF Seminar

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.

Vortr├Ąge
Thema Vortragender Download Folien (PDF) Download Ausarbeitung (PDF)
Butterfield, Woodcock: Formalising Flash Memory: First Steps Harbarth, Daniel    
Leroy: "Formal Certification of a Compiler Back-end" Walch, Martin    
Weber: Towards Mechanized Program Verification with Separation Logic K├╝bler, Andreas    

Themen

Die Themen k├Ânnen hier eingesehen werden.

Randbedingungen

Randbedingungen f├╝r Ausarbeitung und Vorbereitung befinden sich hier (wichtig! Bitte Lesen!!).