Die Vorlesung beschäftigt sich zunächst mit der Analyse von UML-Diagrammen. Es werden Class, State, Activity und Sequence Diagrams betrachtet.
Zuerst werden Class Diagrams mit Alloy, einer Sprache für die Spezifikation von objekt-orientierten Software-Systemen, modelliert und analysiert. Die Beziehung von Alloy zu OCL (Object Constraint Language) wird skizziert.
Anschließend werden State Diagrams (Statecharts) eingeführt, wobei das Problem, Statecharts eine formale Semantik zu geben, diskutiert wird. Die zwei populärsten Semantiken werden vorgestellt und miteinander verglichen.
Der nächste Teil der Vorlesung beschäftigt sich mit Activity Diagrams. Dabei wird ihre Beziehung zu Petrinetzen erläutert und es werden Analysetechniken für Petrinetze (Erreichbarkeitsgraph, Überdeckungsgraph, Invarianten) präsentiert.
Im weiteren Verlauf der Vorlesung werden dann Sequence Diagrams (message sequence charts) eingeführt. Ihre Semantik wird formalisiert und das Problem, Race Conditions zu identifizieren, wird vorgestellt und gelöst.
Wenn die Zeit dann noch ausreicht, wird sich die Vorlesung auch mit der Analyse von Java-Programmen beschäftigen.
esp