SS 2011: Modellierung nebenläufiger Systeme

Dozent:
Prof. Dr. Barbara König (E-Mail)

Nebenläufige Systeme - von denen verteilte Systeme ein Spezialfall sind - können von einem Benutzer oder Programmierer oft nur schwer überschaut werden. Bereits relativ kleine Systeme, die aus mehreren interagierenden Komponenten bestehen, können ein sehr komplexes Verhalten haben. Außerdem stößt man auf Phänomene und Probleme (Deadlocks, wechselseitiger Ausschluß), die bei sequentiellen Systemen in dieser Form nicht auftreten können. Daher werden in dieser Vorlesung entsprechende Modellierungstechniken und Analysemethoden vermittelt, die zum besseren Verständnis solcher Systeme führen. Es werden voraussichtlich folgende Themen behandelt:

• Transitionssysteme
• Verhaltensäquivalenzen (Trace-Äquivalenz, Bisimulation)
• Sicherheits- und Lebendigkeitseigenschaften
• Büchi-Automaten
• Temporale Logik, LTL-Model-Checking
• Prozesskalküle (CCS)
• Petri-Netze (Partialordnungstechniken)
• Graphtransformationssysteme

Im Wintersemester 2011/12 wird die Vorlesung mündlich geprüft. Prüfungstermin ist der 10.02.2012. Bitte vereinbaren Sie noch die genaue Uhrzeit.

Diese Vorlesung kann von Studierenden verschiedener Studiengänge gehört werden. Insbesondere handelt es sich dabei um:

• Studierende im Diplom-Studiengang "Angewandte Informatik" als Grundlagenfach Theoretische Informatik oder für den Bereich Informatik der Systeme
  
  
• Studierende im Duisburger Master-Studiengang "Angewandte Informatik (Ingenieur- und Medieninformatik)"
  
  
• Studierende im Master-Studiengang "International Studies in Engineering" (Computer Engineering)
  
  
• Studierende mit Nebenfach Informatik

• R. Milner: Communication and Concurrency. Prentice Hall, 1989.
• W.J. Fokkink: Introduction to Process Algebra. Springer, 2000.
• Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, Jiri Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
• Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model Checking. MIT Press, 2000.
• W. Reisig: Petrinetze. Springer, 1985. (Eine neuere Version ist hier verfügbar.)
• Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008.

Elektronisch verfügbare Literatur:

• Davide Sangiorgi: On the origins of Bisimulation, Coinduction, and Fixed Points. Technical Report 2007-24, Department of Computer Science, University of Bologna, 2007. http://www.cs.unibo.it/~sangio/DOC_public/history_bis_coind.pdf
• Madhavan Mukund: Finite-state Automate on Infinite Inputs. Tutorial talk, 1997.
  http://www.cmi.ac.in/~madhavan/papers/tcs-96-2.html
• Madhavan Mukund: Linear-Time Temporal Logic and Büchi Automata. Tutorial talk, 1997.
  http://www.cmi.ac.in/~madhavan/papers/isical97.html
• Tadao Murata: Petri Nets: Properties, Analysis and Applications. Proc. of the IEEE, 77(4), 1989.
  http://www.cs.unc.edu/~montek/teaching/spring-04/murata-petrinets.pdf

Folgende Werkzeuge werden in der Vorlesung eingesetzt:

• Model Checker SPIN
• The Edinburgh Concurrency Workbench

Vorlesung

• Mi, 8:30–10:00, LC 137
• Do, 8:30–10:00, LE 120

Übung

• Do, 14:15–15:45, LC 137

Im Wintersemester 2011/12 wird "Modellierung nebenläufiger Systeme" mündlich geprüft. Prüfungstermin ist der 10. Februar. Im Sekretariat (LF 227) liegen ab sofort Listen aus, in die Sie sich eintragen können, um einen Prüfungstermin zu erhalten.

In the winter semester 2011/12 there will be an oral exam for the course "Modellierung nebenläufiger Systeme", taking place on 10 February. You can obtain a slot by entering you name in the lists in the secretary's office (LF 227).

Die Ergebnisse der Klausur vom 21.7. hängen an dem Brett zwischen Raum LF 263 und LF 264 aus. Die Bonuspunkte sind bereits mit einberechnet. Die Klausureinsicht findet am Dienstag, den 16.8., um 14:00 Uhr im Raum LF 261 statt.

• Folien, Notizen und Übungsblätter

Die Folien werden ähnlich zu den Folien im Wintersemester 09/10 sein.

no news in this list.