Spezifikationstechnik

Organisatorisches

Lernziele & erworbene Kompetenzen:

• Vertrautheit mit Methoden der formalen Spezifikation
  
• Befähigung zur Einschätzung, für welche Software-Artefakte der Einsatz formaler Spezifikation sinnvoll ist.
  
• Kenntnisse über Potentiale und Grenzen formaler Methoden

Vorlesungsinhalte

• Formale versus informale Spezifikation
• Spezifikation, Validierung, Verifikation, Generierung
• Spezifikation abstrakter Datentypen
• Spezifikation von zeitlichen Abläufen und Prozessen, Anwendungsbeispiel: Protokollspezifikation
• Konkrete Spezifikationssprachen und Werkzeuge

• Motivation und Grundbegriffe
• Spezifikation abstrakter Datentypen
• Dynamische und temporale Logik
• Spezifikation von Prozessen
• Spezifikation verteilter Systeme
• Objektspezifkation
• Weitere Spezifikationsansätze

Vorlesungsfolien

1. Organisatorisches und Einfuehrung
2. Logikgrundlagen
3. Begriffe
4. Spezifikation abstrakter Datentypen
5. Automaten zur Ablaufbeschreibung
6. Temporale Logiken
7. Automaten und temporale Logik
8. Model Checking
9. Gastvorlesung: Don't Claim Its Safe
10. Spezifikation von Prozessen: Petri-Netze
11. Spezifikation von Prozessen: Prozesskalkuele

Uebung

1. Uebung 1 (08.04.2009)
2. Uebung 2 (15.04.2009)
3. Uebung am 22.04.2009 entfaellt
4. Uebung 3 (29.04.2009)
5. Uebung 4 (06.05.2009)
6. Uebung 5 (13.05.2009)
7. Uebung am 20.05.2009 entfaellt
8. Uebung 6 (03.06.2009)
9. Uebung 7 (10.06.2009)
10. Praktische Uebung 8 (17.06.2009; G29-336)
11. Praktische Uebung (Fortsetzung) (24.06.2009; G29-336)
12. Praktische Uebung 9 (06. und 08.07.2009; G29-336)