Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
Institute of Formal Methods in Computer Science

Software Reliability and Security Group


Networks and Processes (SS 2011)

Lecturer: Dirk Nowotka

Tutor: Nikola Milosavljevic

Note, that the course starts on May 5 (not on April 28)!
The Exam results are out and can be found on the door of room 1.108. The corrections can be inspected in room 1.108 on August 16 at 2pm.

Thu 14:00-15:30 in Room 0.363 (CS building); first lecture on May 5
Thu 15:45-17:15 (every other week) in Room 0.363 (CS building)

Thu 15:45-17:15 (every other week) in Room 0.363 (CS building); first exercise session on May 12

It takes place on thursday July 28, 2011, and starts at 2pm in Room 0.363
(two hand-written sheets of A4 paper with personal notes are allowed material).
Old exam sheets together with example solutions can be found on the websites of Networks and Processes of the previous years.
Go to and follow the links to previous winter terms. There you find the respective NP sites with previous exams published.

Intended Audience:
Students of the Master of Science program Information Technology (INFOTECH),
students of the "Diplom-Studiengang Elektrotechnik und Informationstechnik"
(under the German title "Netze und Prozesse", the lectures are identical),
students of Informatik or Softwaretechnik (Vertiefungslinie Sichere und Zuverlässige Softwaresysteme)

Contents (short version):
Modeling and analysis of parallel and distributed systems. Specifying system properties with temporal logics and using model checking to verify them. Basics of computer aided verification algorithms. Petri nets as system description formalisms.

Slides: PDF file

Exercise Sheets:
Demo Exercise -- Sample solutions
Exercise Sheet 1
Exercise Sheet 2
Exercise Sheet 3
Exercise Sheet 4

The PEP tool (University of Oldenburg)
Spin (Bell Labs) -- short introduction to Promela (PDF) and models used in the lecture (ZIP)
DDcal (University of Colorado) -- a BDD "calculator"
SMV (CMU) -- some tool demonstration slides (PDF) and a couple of examples (tar.gz)