Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Formale Entwicklung objektorientierter Software (WS 2012/13)

Formale Entwicklung objektorientierter Software
Typ: Praktikum
Ort: Bei Vorlesungsterminen Raum 301; Bei Meetings und Präsentationen der Studierenden Raum 211
Zeit (regulär): Mi, 17.30 - 19.00;
Bei Präsentationen der Studierenden:
  • Gruppe 1: 17:30-18:00,
  • Gruppe 2: 18:00-18:30,
  • Gruppe 3: 18:30-19:00
(Die Gruppen können die Reihenfolge untereinander ausmachen)
Beginn: 24.10.2012
Dozierende: Prof. P. H. Schmitt
Prof. B. Beckert
Daniel Bruns
David Faragó
Christoph Gladisch (Leitung)
Christoph Scheben
Mattias Ulbrich
LVNr.: 24308

Beschreibung

Ist fehlerfreie Software möglich?

Wenn Sie die Antwort auf diese Frage interessiert und Sie schon immer einmal Software in einer Gruppe entwickeln wollten, dann ist dieses Praktikum genau das, wonach Sie suchen.

Anhand eines selbst realisierten Software-Projektes lernen Sie in einer Gruppe Aspekte der formalen Softwareentwicklung kennen und anzuwenden, d.h. Analyse, Modellierung, Spezifikation, Implementierung und Verifikation (aber z. B. auch Dokumentation). Für die Implementierung verwenden wir Java, zum Spezifizieren die Java Modeling Language (JML). Als Verifikationswerkzeuge werden z. B. ESC/Java2, JMLUnit, der JML Runtime Assertion Checker (RAC) und KeY eingesetzt.

Der in der Vorlesung "Formale Systeme" behandelte Stoff sowie Programmierkenntnisse werden vorausgesetzt. Kenntnisse aus der Vorlesung "Softwaretechnik" sind von Vorteil. In der parallel laufenden Vorlesung "Spezifikation und Verifikation von Software" werden die notwendigen theoretischen Grundlagen zum Praktikum vermittelt. Zu den einzelnen Praktikumseinheiten gibt es Übungsaufgaben.

Vorbesprechung am Mittwoch, dem 17. Oktober 2012, um 17:30 im Raum 301 (Geb. 50.34)

Ablauf des Praktikums

  • Im Abstand von etwa ein bis zwei Wochen werden von den Teilnehmern Lösungen zu Übungsblättern präsentiert (siehe unten). Die Teilnehmer sind in Gruppen aufgeteilt. Die Präsentationen der Gruppen an einem Termin finden zeitlich getrennt statt (im Abstand von 30min, siehe oben), sodass eine präsentierende Gruppe die jeweilige Präsentationen der vorhergehenden Gruppen nicht hört. Das Format der Präsentationen ist frei wählbar.
  • Die Teilnehmer wechseln sich mit den Präsentationen innerhalb einer Gruppe ab, aber alle Teilnehmer müssen Fragen während der Präsentation beantworten können.
  • Die schriftliche Abgabe zu einem Übungsblatt findet ein oder wenige Tage vorher statt und wird auf dem Blatt bekannt gegeben.
  • Abwechselnd zu den Präsentationen der Teilnehmer finden Treffen zum gemeinsamen Arbeiten und für zwei Vorlesungstermine statt.
  • Anwesenheit an allen Terminen ist erforderlich. Ausnahmen müssen nachweisbar begründet sein.

Terminplan

Achtung: Änderungen des Plans sind vorbehalten

Übungsblätter

Weitere Informationen und relevante Dokumente

Anmerkung: Bei den Tools handelt es sich meistens um Prototypen.

JML

ESC/Java2

KeY