MAIS

Formale Spezifikation und Analyse (Seminar für Bachelorstudenten)

Form: Seminar für Bachelorstudenten, 24.-26.6., Ort wird noch bekannt gegeben

Anmeldung: Anmeldungen nimmt Elisabeth Kraft entgegen. Falls Sie sie nicht antreffen sollten, wenden Sie sich bitte an Alexander Lux im Büro nebenan (S2-02-E317).

Vorwissen: Kanonik-Vorlesung "Foundations of Computing" aus dem Wintersemester 2007/2008

Literatur: Wird in der Vorbesprechung bekanntgegeben

Vorbesprechung: Donnerstag, 3. April 2008, 13:00 Uhr in S202/E202.

Kontakt: Bei Fragen bitte an Alexander Lux wenden.

Thema:

Durch eine Spezifikation kann beschrieben werden, welche Eigenschaften ein System hat oder haben sollte. Gegenüber spezifizierten Eigenschaften kann ein System analysiert werden. Von Interesse sind hierbei vor allem funktionale Eigenschafte wie das Ein-/Ausgabeverhalten, das zeitliche Verhalten, die Toleranz gegenüber Störungen und Aspekte der IT Sicherheit. Verwendet man formale Sprachen zur Spezifikation anstatt natürlicher Sprachen, so wird es möglich Spezifikationen mit rigorosen, mathematischen Methoden zu analysieren, also formal zu analysieren. So kann z.B. nachgewiesen werden, dass eine Implementierung bezüglich der gegebenen Spezifikation korrekt ist oder dass die Spezifikation gewisse Metaeigenschaften erfüllt. Wünschenswerte Metaeigenschaften von Spezifikationen sind z.B. Widerspruchsfreiheit, Eindeutigkeit und Adäquatheit, wobei sich letztere nur informell nachweisen lässt.

Basis der formalen Spezifikation und Analyse sind formale Modelle der zu spezifizierenden und analysierenden Systeme. Viele System verhalten sich probabilistisch, weil ihr Verhalten zum Beispiel von zufälligen Umgebungseinflüssen abhängt. Daher liegt ein Schwerpunkt des Seminars auf der Verwendung probabilistischer Modelle. In der Informatik interessieren uns häufig die Eigenschaften von Programmen, z.B. ob sie zuverlässig funktionieren oder sicher sind. Daher ist ein weiterer Schwerpunkt die Behandlung formaler Analysemethoden für Programme.

Im Seminar werden Ansätze, Techniken und Werkzeuge für formale Spezifikationen und Analyse anhand von aktuellen Forschungsartikeln behandelt.