Achtung:

Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right) Show image information

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right)

Vorlesung: Softwaremodellierung mit formalen Methoden

Veranstaltung: L.079.05603

Sommersemester 2020

Dozentin: Heike Wehrheim

Tutor: Cedric Richter

Die Veranstaltung wird über die PANDA Plattform organisiert. Die Anmeldung zur Veranstaltung findet über PAUL statt.

-- Diese Webseite kann sich ändern und wird kontinuierlich aktualisiert --

[letztes Update am 06. Mai 2020 um 12:30 Uhr]

Allgemeine Informationen

  • Hörerkreis: Studierende der Informatik im Bachelorstudiengang, 2. Studienabschnitt
  • Modul: Softwaremodellierung mit Formalen Methoden
  • ECTS-Punkte: 6

Inhalt

Formale Methoden sind Sprachen zur Modellierung/Spezifikation von Systemen. Ein Modell eines (Soft- oder Hardware) Systems beschreibt auf einer gewissen Abstraktionsebene die Funktionalität des Systems. Im Gegensatz zu (den meisten) Programmiersprachen besitzen formale Methoden eine genau festgelegte Semantik, d.h. eine mathematische Beschreibung der Bedeutung einer Spezifikation. Diese Festlegung der Semantik erlaubt es, das Systemmodell bereits vor der eigentlichen Implementierung formal zu analysieren und mögliche Fehler frühzeitig zu finden.

In der Vorlesung sollen verschiedene formale Methoden eingeführt werden, die für unterschiedliche Systemarten geeignet sind. Für jede dieser formalen Methoden werden Semantik und Analysetechniken vorgestellt und Modellierungsbeispiele zur Illustration des Einsatzbereiches besprochen.

Am Anfang der Vorlesung wird es vorrangig um die Modellierung von Parallelität und Kommunikation gehen. Hier werden Petrinetze und die Prozessalgebra CCS vorgestellt. Danach werden wir uns mit Sprachen zur Beschreibung von zeitlichen Aspekten (Timed Automata) und gegebenenfalls auch mit zustandsbasierten Formalismen zur Spezifikationen von Daten und Operationen (Z und Object-Z) beschäftigen.

Literatur

Einführung

  1. J. M. Wing, A Specifier's Introduction to Formal Methods. IEEE, Computer, 23(9):8-24, September 1990.
  2. E. Clarke and J. Wing, Formal Methods: State of the Art and Future Directions, CMU Computer Science Technical Report CMU-CS-96-178, August 1996, erschienen in: ACM Computing Surveys, 28(4):626-643, 1996.

Petrinetze:

  1. W. Reisig, Petrinetze - Eine Einführung. Springer Verlag, 1985.
  2. B. Baumgarten, Petri-Netze - Grundlagen und Anwendungen. BI Wissenschaftsverlag, 1990.
  3. Webseite Petri Nets World.

CCS:

  1. R. Milner, Communication and Concurrency, Prentice Hall, 1989.

Timed Automata:

  1. R. Alur, D. Dill: A Theory of Timed Automata. Theoretical Computer Science 126, p. 183 - 235, 1994.
  2. E.-R. Olderog, H. Dierks. Real-time Systems - Formal Specification and Automatic Verification. Cambridge University Press.

Z und Object-Z:

  1. J. M. Spivey, Z Reference Manual.
  2. J. Woodcock, J. Davies, Using Z - Specification, Refinement, and Proof. Prentice Hall, 1996.
  3. R. Duke, G. Rose. Formal Object-oriented Specification using Object-Z. MacMillan, 2000.
  4. G. Smith. The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, 2000.
  5. J. Derrick, E. Boiten. Refinement in Z and Object-Z. Foundations and Advanced Applications. Springer Verlag, 2001.
Wichtige Information

Auf Grund der aktuellen Lage kann sich die Organisation der Vorlesung ändern.

Informieren Sie sich bitte regelmäßig über den aktuellen Stand auf PANDA.

Contact

Prof. Dr. Heike Wehrheim

Specification and Modelling of Software Systems

Heike Wehrheim
Phone:
+49 5251 60-4331
Office:
O4.225
Web:

Cedric Richter

Specification and Modelling of Software Systems

Cedric Richter
Phone:
+49 5251 60-1762
Office:
O4.122
Web:

Office hours:

Monday - Friday

8am until ~4pm

The University for the Information Society