Lecturer: Dirk Nowotka

Lectures:
Thu 14:00-15:30 in Room V47.05
Thu 15:45-17:15 (every other week) in Room V47.05

Exercises:
Thu 15:45-17:15 (every other week) in Room V47.05

Evaluation:
Go to fachschaft.informatik.uni-stuttgart.de/VU/Frageboegen/e1.html (in German) to give feedback.

The results of the exam are out!
You can get your mark from a list posted at the door of my office (1.156). If you'd like to inspect your corrected answer sheet pop in or make an appointment by email.

Exam: (Note the change of the exam date!)
Thursday in the last but one week of the lecture period, that is Feb 5, 2009, starting at 2pm in Room V47.05
(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 www.informatik.uni-stuttgart.de/fmi/szs/teaching/ 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, LaTeX sources

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

Tools:
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) from last year and a couple of examples (tar.gz)

Exam:
The problems (of the written exam on 5.2.2009)
Sample solutions