Woche 10: Modellieren mit Alloy (I)
Übersicht
In dieser Woche werden wir uns mit dem Modellierungswerkzeug Alloy beschäftigen. Alloy ist eine formale Spezifikationssprache, mit der wir Designs analysieren und früh im Entwicklungsprozess Fehler finden können. Das Ziel dieser Einführung ist nicht, sie zu Expert:innen in der Formalen Modellierung zu machen, sondern Ihnen zu zeige, wie solche Werkzeuge aussehen und wie sie eingesetzt werden können.
Lernziele
Die Studierenden
- kennen die Grundidee von Alloy und können erklären, wie Alloy im Software Engineering eingesetzt werden kann.
- können einfache statische Modelle in Alloy erstellen und analysieren.
- kennen die Grundlegende Annahme die Alloy zugrunde liegt und wie sich der Ansatz von Alloy von der Überprüfung mittels Testen unterscheidet.
- kennen den Unterschied zwischen facts, predicates und assertion und wissen, wie sie diese in Alloy einsetzen können.
Vorlesungsslides
- Modellieren mit Alloy
- Slides (Auf Adam): pdf
Ressourcen
Ü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 wir mit Ihnen Ihren Testplan besprechen. Zudem sollten Sie Ihre Implementation fertigstellen und an der Präsentation arbeiten.