[03-BB-700.21] Formale Modellierungen

Christoph Lüth
Till Mossakowski

Aktuelles

Die Termine am 21.06. und am 25.06. müssen aus Krankheitsgründen leider entfallen. Der reguläre Betrieb wird am 28.06. wieder aufgenommen.

Termine

K 4 SWS
Mo 14:00 - 16:00 MZH 1460
Do 16:00 - 18:00 Cartesium 2.43
Beginn: 16.04.2012

Inhalt

Formale Modellierungen ermöglichen eine problem-orientierte Sicht auf Software. Sie stellen gleichzeitig ein Kriterium für die Korrektheit von Software dar, und machen so Test und Verifikation erst möglich. Dies ist besonders in sicherheitskritischen Bereichen wichtig.

In dieser Vorlesung werden drei Modellierungs-Methoden vorgestellt:

1. Die Java Modeling Language (JML) stellt einen Hoare-Kalkül für objekt-orientierte Programme in Java bereit. Methoden können mit Vor- und Nachbedingungen, Klassen mit Invarianten annotiert werden. Es gibt eine Reihe von Werkzeugen für JML. Wir werden hauptsächlich ESC/Java2 verwenden.
2. Die Unified Modeling Language ist unabhängig von einer bestimmten Programmiersprache und erlaubt deshalb eine problemnähere grafische Modellierung von Software, die zunächst stärker von der Struktur des Codes abstrahieren kann. UML besteht aus einer Vielzahl von Diagrammen. In dieser Vorlesung werden wir uns auf Klassendiagramme, State machines und OCL konzentrieren. Als Werkzeuge verwenden wir ArgoUML und Hugo/RT.
3. Temporallogik erlaubt die Spezifikation nebenläufiger Programme, z.B. von gegenseitigem Ausschluss kritischer Bereiche. Als Werkzeug verwenden wir den nuSMV Model-Checker.

Installation der Software

Vorlesungsfolien und Übungsblätter

Hier sind die Vorlesungsfolien, entweder als interaktive Folien, oder als Handouts zum Ausdrucken:

• Vorlesung vom 16.04.2012: [Folien] [Handouts]
• Vorlesung vom 19 und 23.04.2012 BoundedStack.java
• Vorlesung vom 26.04.2012
• Vorlesung vom 03.05.2012
• Vorlesung vom 07.05.2012: [Folien] [Handouts]
• Vorlesung vom 14.05.2012: [Folien] [Handouts]
• Vorlesung vom 31.05.2012: [Folien] [Handouts]
• Vorlesung vom 04.06.2012: [Folien] [Handouts]
  Dazu die Beispiele: example-fbs.zargo, example-fbs.use.
• Vorlesung vom 28.06.2012: [Folien]
  
• Vorlesung vom 02.07.2012: [Folien]
  Dazu die Beispiele: short.smv, counter.smv, mutex-simplie.smv, mutex.smv.
• Vorlesung vom 05.07.2012, Beispiele: ferry.smv, alternating-bit-protocol.smv.
• Vorlesung vom 09.07.2012: [Folien]
• Vorlesung vom 19.07.2012: [Folien]
• Einige Vorlesungen in einem Dokument: [Folien] [Handouts].

• 1. Übungsblatt (Abgabe: 10.5.) gemeinsam in der Veranstaltung erarbeitete Modellierungsschritte: Bank.java
• 2. Übungsblatt (Abgabe: 07.06.)
• 3. Übungsblatt (Abgabe: 19.07.)

Literatur und Links

• Gary T. Leavens, Yoonsik Cheon. Design by Contract with JML. Draft tutorial.
• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, chapter 12, pages 175-188. Kluwer, 1999.
• Mehr zu Z: Homepage der Community Z Tools, ein LaTeX style file, und und eine Kurzanleitung dazu.
• OCL: Der Sprachstandard
• Jos Warmer, Anneke Kleppe: The Object Constraint Language. Precise Modeling with UML. Addison-Weslay, 1999. ISBN 0-201-37940-6
• Verschiedene OCL-Werkzeuge (mehr siehe im OCL Portal):
  • USE (Uni Bremen), ArgoUML (Open Source), HOL-OCL (ETH Zürich)
• Michael Huth, Mark Ryan: Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004. ISBN 0 521 54310X