Woche 11: Modellieren mit Alloy (II)

Übersicht

In dieser Woche werden wir das Modellierungswerkzeug Alloy vertiefen. Insbesondere werden wir sehen, wie wir dynamische Modelle in Alloy erstellen können. Zudem werden wir anhand von Anwendungsbeispielen sehen, wie wir Alloy für die Modellierung von Software Systemen einsetzen können.

Lernziele

Die Studierenden

• kennen die Zeitoperatoren von Alloy und können damit einfache temporale Eigenschaften modellieren.
• kennen die Grundlegende Strategie um dynamische Modelle in Alloy zu erstellen.
• können den Visualizer einsetzen um dynamische Aspekte von Modellen zu verstehen.
• können einfache dymamische Modelle in Alloy erstellen und analysieren.

Vorlesungsslides

• Modellieren mit Alloy
  • Slides (Auf Adam): pdf

Ressourcen

• Offizielle Seite für Alloy
• Alloy Dokumentation
• Formal software design with Alloy
• Alloy 6 - It’s all about time

Übungen

Versuchen Sie die Aufgaben im Alloy Übungsblatt zu lösen.

• Das Übungsblatt muss nicht abgegeben werden.
• Wir werden die Übungen in der letzten Übungsstunde am 17. Dezember besprechen.
• Das bearbeiten der Übungen ist freiwillig. Alloy wird aber ein Teil der Prüfung sein.

Übungsstunde:

Im Praktischen Teil der Vorlesung werden Sie weiter an Ihrem Projekt arbeiten und die Präsentation vorbereiten.