Home | deutsch  | Legals | Sitemap | KIT

Spezifikation und Verifikation von Software (WS 09/10)

Spezifikation und Verifikation von Software (WS 09/10)
Type: Vorlesung Links:
Place: SR 131
Time:

Mo, 15:45 - 17:15
Do, 15:45 - 17:15

Start: 19.10.2009
Lecturer:

Prof. P. H. Schmitt

SWS: 3
Exam:

Mündliche Vertiefungsfachprüfung

Diese Vorlesung wird im Wintersemester 2009/2010 zum ersten Mal in dieser Form gehalten.

Sie behandelt zwei verschiedene Spezifikationsmethoden:

  1. EventB
    Benutzt die Methode der sukzessiven Verfeinerung. Operiert auf der abstrakten Ebene rein mengentheoretischer Notation. Das zugehörige  Beweiswerkzeug heiß Rodin.
  2. Java Modeling Language JML
    Die Spezifikationen werden direkt als Annotationen in der Form spezieller Kommentare in den Java Code geschrieben. Syntax und Semantik von JML orientieren sich sehr stark an Java. Als Analysewerkzeuge werden benutzt: Ein runtime checker rac, ein Testgenerator JMLUnit, eine (unvollständige)  statische Analyse ESCJava2 und ein Theorembeweiser KeY.

Die Vorlesung ist in enger Anlehnung an des Praktikum Formale Entwicklung objektorientierter Software konzipiert. Zum einen werden die zur Durchführung der Praktikumsversuche erforderlichen einführenden Erklärungen bereitgestellt, zum anderen wird der theoretische Hintergund und verwandte Themen behandelt.