Formale Methoden im Software Engineering SS 2011

Downloads:

• Praktikum
• Vorlesung

Vorkenntnis für die Lehrveranstaltung:

Interesse an Logik und formalen Methoden, Vordiplomsveranstaltungen (insb. Logik für Informatiker)

Literatur zur Lehrveranstaltung:

Es besteht eigentlich keine Notwendigkeit, zusätzliche Literatur heranzuziehen. Wer sich dennoch etwas schlauer machen will, kann folgende Bücher lesen:

• V. Sperschneider and G. Antoniou, Logic: A Foundation for Computer Science, Addison Wesley, 1991
• J. Loeckx and H.D. Ehrich and M. Wolf, Specification of Abstract Data Types, Wiley-Teubner, 1996

Der Lehrstuhl Softwaretechnik und Programmiersprachen bietet im SS 2011 die Veranstaltung "Formale Methoden im Software Engineering" (integrierte V + Ü) an.

Die Verwendung formaler Methoden bei der Entwicklung korrekter Software steht an der Schwelle der kommerziellen Nutzung.
Das KIV-System ist ein Werkzeug, das die formale Spezifikation, Verifikation und Synthese von Programmen ermöglicht. Es wird seit mehreren Jahren entwickelt und inzwischen in industriellen Studien erprobt. Übergeordnetes Ziel ist die Produktion beweisbar korrekter Software.

Im Praktikum werden verschiedene klassische Methoden für das Programmieren im Kleinen behandelt. Darüber hinaus kommen innovative Techniken für das Programmieren im Großen zum Einsatz: Spezifikationstechniken und Methoden zum Nachweis der Korrektheit von großen, modular strukturierten Systemen. Das Praktikum vermittelt damit den ''state of the Art'' des Einsatzes formaler Methoden bei der Softwareentwicklung.

Die Rechner im Raum 3017N stehen auch ausserhalb der Praktikumszeiten zur Verfügung. Notfalls bei uns nach einem Schlüssel fragen, falls der Raum abgesperrt ist. Benutzen Sie dann aber bitte nicht die Rechnerzeile direkt am Eingang, da diese anderweitig benutzt wird.

Kurzfristige Änderung: Die letzte Vorlesung zu Temporallogik (TL) muss leider vom 8.7 um eine Woche auf den 15.7. verschoben werden. Da der Versuch zu TL bereits am 13.7 beginnt, wird am 6.7 sowohl vormittags als auch nachmittags eine kurze Einführung und Demo stattfinden. Die Folien zur Vorlesung sind schon online, und es wird empfohlen, sie bis zum 13.7 zur Vorbereitung zu überfliegen.

Das Praktikum am 6.7 findet wegen einer Veranstaltung nicht im Praktikumsraum sondern im Diplomanden-Raum 3007 statt.

Wichtig: Der/die letzte der abends geht, muss dafür sorgen, dass der Raum abgesperrt wird. Typischerweise dazu bei einem Mitarbeiter des Lehrstuhls vorbeigehen.

Subversion:

Ihre Aufgaben werden mit Hilfe eines Subversion Repositories verwaltet. Eine kurze Anleitung wie sie die einzelnen Aufgaben dort einchecken finden sie hier.

Mehr Infos zu Subversion gibt es unter den folgenden Links:

SVN Buch: http://svnbook.red-bean.com/

Starter Guide: http://www.cse.yorku.ca/~percept/svn_starters_guide.pdf

weitere Informationen zu der Lehrveranstaltung:

empfohlenes Studiensemester der Lehrveranstaltung:	Master
Fachrichtung Lehrveranstaltung:	Informatik (Dipl., Bachelor, Master)
Dauer der Lehrveranstaltung:	6 SWS
Typ der Lehrveranstaltung:	WV - Wahlvorlesung
Leistungspunkte:	8 LP für Vorlesung und Praktikum
Bereich:	(MA neue PO) Softwaretechnik; (alte POs) Softwaretechnik, Theoretische Informatik
Prüfung:	Sonstige
Lehrveranstaltungspflicht:	Wahlpflicht
Semester:	SS 2011