Softwaretechnik 2, WiSe 11
Softwaretechnik II gibt eine Einführung in die Entwicklung von Softwaresystemen mit Hilfe von formalen Methoden am konkreten Beispiel der B-Methode.
Die Vorlesung fand als Blockkurs in der Woche vom 26. bis 30. September 2011, um 8:30 - 18:00 Uhr statt, also noch vor der eigentlichen Vorlesungszeit.
Nächstes Treffen: Mittwoch, 9. November um 14:30 Uhr im Seminarraum.
Für das Semester wird es dann eine Projektarbeit geben, die bis zum Ende des Semesters läuft. Innerhalb des Semesters wird es dann ein paar Treffen geben, bei dem offene Fragen geklärt werden können.
Link zur Veranstaltung im letzten Jahr: Softwaretechnik 2, Winter 2010
Projekte
Es gibt zwei Projekte, die über das Semester bearbeitet werden.
Für das Event-B-Projekt muss bis zum 30. November 2011 ein Prototyp abgegeben werden, der einige Refinementebenen enthält, die bereits mehrere Funktionalitäten modellieren. Arbeiten Sie vorab bitte das Tutorial im Event-B Handbuch durch.
Beide Projekte müssen im Januar 2012 fertig gestellt werden (auch hier wird noch das genaue Datum bekannt gegeben). Sie stellen die Prüfungsvoraussetzung dar.
Für beide Projektebeschreibungen folgen hier voraussichtlich Ende Oktober aktualisierte Fassungen.
Ich habe eine Seite Projektkommentare eingerichtet, um Kommentare zu Designentscheidungen zu sammeln.
Auktionssystem
Als Beispiel wie ein System spezifiziert, verfeinert und dann nach Java übertragen werden kann, wird ein Banksystem vorgestellt. Es können Benutzer angelegt werden, Geld abgehoben oder eingezahlt werden, Transaktionen vorgenommen werden und der Kontostand abgefragt werden.
Hier schonmal der Java-Teil: File:2011 WS ST2Projekt.zip
Hier ist das B Projekt: File:2011 WS ST2tarProjekt.arc.gz Es kann entpackt werden, wenn man in Click'n Prove auf [rr] (unten in der Mitte auf der Startseite) klickt.
Das in B als korrekt bewiesene System hat übrigens einen Fehler! Ich überlege mir gerade noch einen Finderlohn...
Entsprechende Erklärungen kommen bald!
Buch
Dieses Modul basiert auf dem Buch "The B-Method: An Introduction" von Steve Schneider.
Das Buch ist unter der Signatur datg111 mehrfach in der Lehrbuchsammlung der Bibliothek vorhanden.
Für den Event-B-Teil des Projektes benutzen Sie bitte das Event-B Handbuch, das nur online verfügbar ist. Da wir das Handbuch zur Zeit am Lehrstuhl überarbeiten, nutzen Sie bitte das Feedback-Formular im Handbuch, um Verbesserungsvorschläge und Fehler zu melden.
Material
- Die modifizierten Folien zum Buch
- Übungsblatt aus dem letzten Jahr zum Thema Mengen/Relationen in Click'n Prove.
- Aus einer vorherigen Vorlesung gibt es noch Übungsblätter:
Maschinen aus der Vorlesung
Die Maschinen wurden alle wegen des Uploads auf die Webseiten umbenannt. Sie funktionieren erst, wenn sie lokal korrekt benannt sind.
- Die abstrakte Bibliotheksmaschine.
- Eine weitere Version der Bibliotheksmaschine, die statt eines eigenen Datentyps Copy Zahlen verwendet. Das Refinement dazu implementiert einen Counter, der sicher stellt, dass jede Zahl nur einmal vergeben wird.