You are here: Home Teaching Winter Term 2016/17 Cyber-Physical Systems I - …

Cyber-Physical Systems I - Discrete Models

In this course we demonstrate how cyber-physical systems, in the wide range of their heterogeneous aspects (large-scale systems, system of systems, embedded systems, concurrent systems, hardware systems, software systems) can be modeled using the basic notion of transition systems. We consider relevant formalisms for modeling correctness properties of cyber-physical systems, and show how the models can be analyzed using algorithmic methods in order to prove correctness or find errors.
Course type Lecture
Instructors Prof. Dr. Andreas Podelski, Dr. Matthias Heizmann, Christian Schilling
Lecture Monday, 16:00 - 18:00, building 101 HS 00-026
Wednesday, 16:00 - 17:00, building 101 SR 00-010/014
Exercise Wednesday, 17:00 - 18:00
  • Group 1 (English, held by Arber Zela) building 051 SR 00-031
  • Group 2 (English, held by Dominik Winterer) building 106 SR 00-007
  • Group 3 (German, held by Betim Musa) building 101 SR 00-010/014
Language of instruction English
Credits 6
Exams Written exam, on 13th March at 14:00 (s.t.) in rooms 026, 036, and 010/14 in building 101

Summer term: on 12th September at 9:00 (s.t.) in room 01-009/013 in building 101
Course catalog Cyber-Physical Systems – Discrete Models - Lecture
Cyber-Physical Systems – Discrete Models - Exercise

Description

The course provides an introduction to discrete models of cyber-physical systems, their analysis and verification:
  • The students learn how to model cyber-physical systems as transition systems. Here, the main focus lies on software and hardware aspects of cyber-physical systems and on methods for modeling parallelism and communication.
  • Moreover, the students learn how to express properties about such systems. The course covers different mechanisms to specify temporal properties including linear time properties and branching time properties such as LTL, CTL, and CTL* properties.
  • Finally, the course demonstrates how to develop algorithms for checking whether these properties hold. After presenting algorithms for explicit state systems we introduce symbolic BDD-based algorithms which are able to tackle the well-known "state explosion problem". In addition, the course covers basic "Bounded Model Checking" (BMC) techniques which restrict the analysis to computation paths up to a certain length and reduce the verification problem to a Boolean satisfiability problem.
  • All necessary foundations for these algorithms such as fixed point theory, data structures like binary decision diagrams (BDDs), and satisfiability (SAT) solvers are introduced in the course as well.

News 

  • Sep. 14: The exam review (Klausureinsicht) for the summer term takes place on Monday, September 25, at 2 pm in room 00-016 of building 052.
  • Aug 17: The exam in the summer term (2017) will be a written exam. We have the same rules as in the winter term (see Exam Section below).
  • Mar. 27: The exam review (Klausureinsicht) takes place on Wednesday, April 19, from 2 pm to 3 pm in room 00-016 of building 052.
  • Mar. 13: Most likely you will be able to see the exam results in the Campus Management system starting from some day between 22nd and 24th March. (However, there is some risk that we need more time for providing the results.)
  • Feb. 08: Added information about the duration of the exam (90min)
  • Feb. 06: Added information about material that you may bring to the exam (A4 sheet).
  • Jan. 23: Exercise 2d on sheet 12 became a bonus exercise because the property which was given in natural language was not very precise.
  • Dec. 04: New "WhithoutOverlay" version of slides available. This version is a compromise between the slides (which contain many overlay frames) and the handout (which is sometimes unreadable). Many thanks to Claus Schätzle for sharing his perl scripts that transform the slides.
  • Nov. 30: There was a typo in Exercise 1 on sheet 7.
  • Nov. 24: There was a mistake in sheet 6 (that was corrected yesterday evening): Instead of "bad prefix of minimal total length" we accidentally wrote "minimal bad prefix".
  • Nov. 2: Exercise 2 on sheet 2 became a bonus exercise.
  • Oct 27: The room for the group 2 tutorial was changed (see above).
  • Oct, 21: Solutions for exercises have to be submitted via the post boxes that are located in the ground floor of building 051.
  • Oct, 20: From now on Monday's lecture will be in room HS 00-026 in building 101.
  • Oct, 19: You may submit your solutions of exercise sheets alone or in a group of two.
  • Oct. 19: Until this evening the exercise groups on this website were accidentally listed in the wrong order. Please re-check the room number before you visit your exercise group.
  • Oct. 18:

    • The application limit in the course management system (HisInOne) was raised from 80 to 100.
    • The groups have been assigned. To make the group size equal, we had to move some students from group 1 to group 2. If you want to change the group, please write a mail to Christian, ideally with a suitable candidate for swapping.

Exercises

The lecture is accompanied by exercises. At the beginning of each week we will publish an exercise sheet at this website. Students will have time until the next Monday to prepare solutions for the problems stated on the exercise sheet. The solutions have to be submitted before the start of the lecture via the post boxes that are located in the ground floor of building 051. The solutions will be corrected by the tutors and discussed in the exercise groups on Wednesday.

Exam

There will be a written exam at the end of the semester. Prerequisite for admission to the final exam is an active participation in the exercises. A sufficient criterion for an active participation is that you received 50% of the exercise points and presented at least one exercise in the discussions at the exercise group.
You may bring to the exam one DIN A4 sheet. Both sides of this sheet may be filled with any notes (e.g., definitions, theorems, examples) but the notes have to be handwritten. You may not use any other material in the exam (except for writing utensils).
The duration of the exam will be 90 minutes.

Resources

Slides

date slides
handout topics
Mon, October 17
Introduction



Wed, October 19
lec02-slides.pdf

lec02-handout.pdf
Formal verification, Transition systems, Transition systems for sequential circuits
Mon, October 24
lec03-slides.pdf
lec03-WithoutOverlays.pdf lec03-handout.pdf
Program graphs, Transition systems for program graphs, Guarded Command Language
Wed, October 26
lec04-slides.pdf lec04-WithoutOverlays.pdf lec04-handout.pdf Guarded Command Language, Spin
Mon, October 31
lec05-slides.pdf lec05-WithoutOverlays.pdf lec05-handout.pdf Parallel systems, Interleaving operator
Wed, November 2
lec06-slides.pdf lec06-WithoutOverlays.pdf lec06-handout.pdf Parallel systems, Synchronization operator, Nondeterminism
Mon, November 7
lec07-slides.pdf lec07-WithoutOverlays.pdf lec07-handout.pdf Parallel systems, Mutual exclusion, State-based view on transition systems
Wed,
November 9
lec08-slides.pdf lec08-WithoutOverlays.pdf lec08-handout.pdf State-based view on transition systems, Paths, Traces
Mon,
November 14
lec09-slides.pdf lec09-WithoutOverlays.pdf lec09-handout.pdf Traces, Regular expressions, Omega-regular expressions
Wed,
November 16
lec10-slides.pdf lec10-WithoutOverlays.pdf lec10-handout.pdf LT properties, Trace inclusion, Trace equivalence
Mon,
November 21
lec11-slides.pdf lec11-WithoutOverlays.pdf lec11-handout.pdf Propositional logic, Invariants, Safety properties
Wed,
November 23
lec12-slides.pdf lec12-WithoutOverlays.pdf lec12-handout.pdf Safety properties, Prefix closure
Mon,
November 28
lec13-slides.pdf lec13-WithoutOverlays.pdf lec13-handout.pdf Prefix closure, Finite traces and trace inclusion, Liveness properties
Wed,
November 30
lec14-slides.pdf lec14-WithoutOverlays.pdf lec14-handout.pdf Fairness
Mon,
December 5
lec15-slides.pdf lec15-WithoutOverlays.pdf
lec15-handout.pdf Fairness, Finite automata (NFA), Regular safety properties
Wed, December 7
lec16-slides.pdf lec16-WithoutOverlays.pdf lec16-handout.pdf Regular safety properties, Ultimate automata library
Mon,
December 12
lec17-slides.pdf lec17-WithoutOverlays.pdf lec17-handout.pdf Checking regular safety properties
Wed, December 14
lec18-slides.pdf lec18-WithoutOverlays.pdf lec18-handout.pdf ω-regular properties, Büchi automata (NBA)
Mon, December 19
lec19-slides.pdf lec19-WithoutOverlays.pdf lec19-handout.pdf Equivalence of Büchi automata and ω-regular expressions.
Wed, December 21
lec20-slides.pdf lec20-WithoutOverlays.pdf lec20-handout.pdf Nonemptiness for NBA, Generalized Büchi Automata (GNBA)
Mon, January 9
lec21-slides.pdf lec21-WithoutOverlays.pdf lec21-handout.pdf Checking ω-regular properties
Wed, January 11
lec22-slides.pdf lec22-WithoutOverlays.pdf lec22-handout.pdf Intersection for GNBA, Syntax of LTL
Mon, January 16
lec23-slides.pdf lec23-WithoutOverlays.pdf lec23-handout.pdf Semantics of LTL
Wed, January 18
lec24-slides.pdf lec24-WithoutOverlays.pdf lec24-handout.pdf Weak Until, LTL-PNF
Mon, January 23
lec25-slides.pdf lec25-WithoutOverlays.pdf lec25-handout.pdf Automata-based LTL model checking

Wed, January 25 lec26-slides.pdf lec26-WithoutOverlays.pdf lec26-handout.pdf
Mon, January 30
lec27-slides.pdf lec27-WithoutOverlays.pdf lec27-handout.pdf Computation tree logic
Wed, February 1
lec28-slides.pdf lec28-WithoutOverlays.pdf lec28-handout.pdf CTL model checking
Mon, February 6
          -
lec29-WithoutOverlays.pdf
           -
Brief summary of course content up to Lecture 17
Wed, February 8
          -
lec30-WithoutOverlays.pdf            -
Brief summary of course content starting with Lecture 18. Ultimate LTL Automizer

Examples

Lecture 21: Automata Script file for trafficlight example

Lecture 22: Automata Script file for messages example

Exercise sheets

sheet submission
sheet 1 Mon, October 24
sheet 2
Mon, October 31
sheet 3
Mon, November 7
sheet 4
Mon, November 14
sheet 5
Mon, November 21
sheet 6
Mon, November 28
sheet 7
Mon, December 5
sheet 8
Mon, December 12
sheet 9
Mon, December 19
sheet 10 Mon, January 9
sheet 11 Mon, January 16
sheet 12 Mon, January 23
sheet 13
Mon, January 30
sheet 14 Mon, February 6

Literature

The lecture will follow very closely the famous textbook "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen (MIT Press).  A copy is available in the library.