Formale Spezifikation von Software (KITE und ST)
Vorlesung im Sommersemester 2004 (zwei SWS)
Jun.-Prof. Dr. Bernhard Beckert
Aktuelles
Lehrevaluation: Bitte füllen Sie diesen Fragebogen und geben Sie ihn in der letzten Vorlesung oder im Sekretariat bei Frau Riechert (Raum B226) ab. Ich möchte auch alle, die nur unregelmäßig an der Vorlesung teilgenommen haben, bitten, den Fragebogen auszufüllen. Die Befragung ist selbstverständlich anonym.
Frühere aktuelle Informationen
Allgemeine Informationen zur Vorlesung
Hörerkreis
Die Vorlesung richtet sich an Studenten der Informatik und der
Computervisualistik im Hauptstudium, die Interesse an formalen
Methoden der Softwareentwicklung haben.
Sie zählt zu den beiden Vertiefungsfächern KITE und ST.
Inhalt
Die Modellierung von Software in einer geeigneten Modellierungssprache
(z.B. UML) gehört schon seit langem zu einer grundlegenden Technik
des Software-Engineerings. Jedoch nimmt auch die praktische Bedeutung formaler
Methoden in der Softwareentwicklung ständig zu, da mehr und mehr sicherheitskritische
Anwendungen entstehen und die Qualitätsansprüche an Software
wachsen.
In der Vorlesungen werden zunächst Techniken der formalen Beschreibung
(Spezifikation) von Software vorgestellt (wobei die Spezifikation objektorientierter
Software den Schwerpunkt bildet). Themen in diesem Bereich sind:
-
Mathematische Grundlagen (insbes. Mengentheorie, Logik)
-
Formale Semantik von UML-Klassendiagrammen
-
Object Constraint Language (OCL)
-
Abstract State Machines (ASMs)
-
State Charts
-
Die Spezifikationssprache Z
-
Abstrakte Datentypen
Zeit und Ort
Dienstags, 12:00 Uhr s.t., Raum B016
Die Vorlesung findet wöchentlich statt, erstmals am 27.04. und
letzmals am 27.07; am 07.06. fällt sie aus (13 Doppelstunden).
Materialien zur Vorlesung
Folien
-
01Intro.pdf
- Introduction and Motivation (Vorlesung am 27.04.04)
-
02SetTheory.pdf
- Set Theory (als bekannt vorausgesetzt)
-
03PredicateLogic.pdf
- Propositional and Predicate Logic (Vorlesung am 27.04.04 bis Folie 10, Vorlesung am 04.05.04 ab Folie 11)
-
04ModalLogic.pdf
- Modal Logic (Vorlesung am 04.05.04 bis Folie 5, Vorlesung am 11.05.04 ab Folie 6)
-
05UMLOverview.pdf
- UML: Overview (Vorlesung am 11.05.04)
-
06UMLClassDiagramsByExample.pdf
- UML Class Diagrams by Example (Vorlesung am 11.05.04 bis Folie 6, Vorlesung am 18.05.04 ab Folie 7)
-
07UMLObjectDiagrams.pdf
- UML Object Diagrams (Vorlesung am 18.05.04)
-
08OCLByExample.pdf
- OCL by Example (Vorlesung am 18.05.04 bsi Folie 16, Vorlesung am 25.05.04 ab Folie 17)
-
09OCLExampleRBAC.pdf
- OCL Example: Role-based Access Control (Vorlesung am 25.05.04 bis Folie 17, Vorlesung am 15.06.04 ab Folie 18)
-
10StateCharts.pdf
- UML State Charts (Vorlesung am 22.06.04)
-
11Z.pdf
- The Z Specification Language (Vorlesung am 29.06.04 bis Folie 32, Vorlesung am 06.07.04 ab Folie 33)
-
12SteamBoilerZ.pdf
- An Example for Specification in Z: Steam Boiler Control (Vorlesung am 06.07.04)
-
13ASM.pdf
- Abstract State Machines (Vorlesung am 13.07.04)
-
14SteamBoilerASM.pdf
- An Example for Specification in ASM: Steam Boiler Control (Vorlesung am 20.07.04)
-
15CASL.pdf
- Algebraic Specification (Vorlesung am 20.07.04)
Weitere Materialien
Bernhard Beckert