Bild mit Unilogo
homeicon uni sucheicon suche siteicon sitemap kontakticon kontakt impressicon impressum
unilogo Universität Stuttgart 
Institut für Formale Methoden der Informatik

Abteilung Sichere und Zuverlässige Softwaresysteme

 

Vorlesung Model Checking (SS 2003)


Dozent: Prof. Dr. Javier Esparza

Vertiefungslinie: Theoretische Informatik

Zeit und Ort:
Mo 15:45-15:15 im Raum 0.108
Übung Do 15:45-17:15 (14-tägig) im Raum 0.363

Hörerkreis: Studierende im Hauptstudium

Empfehlenswert für:
Erweiterte Kenntnisse in den Gebieten Verifikation, Anwendungen der Automatentheorie, Logik

Inhalt:
Model-Checking ist eine Technik für die automatische Verifikation von Hardware- und
Softwaresystemen. Seit den ersten Arbeiten, die Mitte der 80er Jahren diese Technik
als eine theorestische Möglichkeit etablierten, ist der Fortschritt enorm gewesen,
insbesondere im Hardware-Bereich. Heuzutage haben alle wichtigsten Hardwarehersteller
Model-Checking Gruppen, die Software-Werkzeuge, sogenannte Model-Checker, entwickeln
und für die Verifikation von grossen Schaltkreisen anwenden.

In der Vorlesung werden die Grundlagen von Model-Checking behandelt. Zuerst wird
erklaert, wie Systeme modelliert werden. Anschliessend werden Temporale Logiken
eingeführt, die als Spezifikationssprachen dienen. Es werden dann die Algorithmen
beschrieben, die automatisch testen, ob das Modell die in Temporaler Logik
formulierten Eigenschaften besitzt. In der Vorlesung wird auch der am Bell-Labs
entwickelte und weit verbreitete SPIN Model-Checker behandelt.

Folien: (vom Stoff, dass bisher betrachtet wurde) (PDF)(gzipped PostScript)
Mit psnup -l -4 <infile> <outfile> bringt man vier Seiten PostScript-Datei auf einer Seite unter und kann so praktischer drucken.