You are here: Home Teaching Winter Term 2017/18 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, Tanja Schindler
Lecture Wednesday, 16:00 - 18:00, building 101 HS 00-036
Exercise Monday, 12:00 - 14:00
  • Group 1 (English) building 051, room 00-034 (Konstantina)
Monday, 16:00 - 18:00
  • Group 2 (English) building 051, room 00-031 (Elisabeth)
  • Group 3 (German) building 101, room 00-026 (Jens)
Language of instruction English
Credits 6
Exams Written exam
Course catalog Cyber-Physical Systems – Discrete Models - Lecture
Cyber-Physical Systems – Discrete Models - Exercises

News 

  • Mar. 23: The grades for the exam are published. You will have the opportunity to review your exam on April 9, 14:00 - 16:00 in our meeting room 052-00-016.
  • Mar. 6: Corrected a typo in the mock exam: in exercise 7, the state on the right is called s_3.
  • Feb. 21: Uploaded a mock exam (at the bottom of this page).
  • Feb. 1: Corrected sheet number of Sheet 13.
  • Jan. 31: Added motivation to Sheet 13.
  • Nov. 29: Sheet 6 was updated, there was a mistake in Ex.1 (g) (wrong alphabet).
  • Nov. 18: Small change in Sheet 5: Exercise 2 (c) has been replaced by a slightly different task.
  • Oct. 27: Sheet 3 is online. You will have time until Nov. 10 as there will be no CPS I sessions (lecture and exercises) next week. However, we recommend to start working on the material and the exercises early as it takes a lot of time.
  • Oct. 27: The new sheet will be published by 7 pm today.
  • Oct. 26: There will not be exercise groups on Monday, Oct. 30. You still have to submit your solutions to sheet 2 until Friday, Oct. 27, and will get a new sheet then.
  • Oct. 24: Updated sheet 2. The tasks remain the same, but it should be clearer now what we expect in Ex. 2.
  • Oct. 17: You can join the Ilias course via this link.
  • Oct. 12: We start with a lecture on Monday, Oct. 16, 16:00 - 18:00, in building 101, room 00-026. There are no tutorials in the first week.
    From the second week on, the lecture will take place on Wednesday and the tutorials on Monday, as stated above.

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.

Course

We follow the concept of a "flipped classroom" where the student reads the relevant part of the course material before it is discussed in class. The exercises should give an orientiation on what to focus while working through the material. Each student will prepare a set of questions for each upcoming class.

Exercises

The lecture is accompanied by exercises. Each Friday we will publish an exercise sheet. Students will have time until the next Friday to prepare solutions for the problems stated on the exercise sheet. Submissions in groups of two are strongly encouraged. The solutions have to be submitted by 11:59 am 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 Monday.

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. You have to submit solutions to every exercise sheet and present 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 must not use any other material in the exam (except for writing utensils).
The duration of the exam will be 90 minutes.

Resources 

Exercise sheets

Here you find the list of exercise sheets.

Exercise sheet
 Literature
Sheet 1
pp. 19 - 29
Sheet 2 pp. 29 - 35
pp. 915 - 920 (A.3)
Sheet 3 Sects. 2.2.1 and 2.2.2
A.1 and A.2
Sheet 4
Sect. 2.2.3 and A.2
Sheet 5
Sect. 2.2.4
Sheet 6 Sect. 3.2 to (incl.) 3.2.3
Sheet 7 Sects. 3.3.1 and 3.3.2
Sheet 8 Sect. 3.4
Sects. 3.2.4 and 3.3.3
Sheet 9 Sect. 3.5
Sheet 10 Sects. 4.1 and 4.2
Sheet 11
Sects. 4.3.1 and 4.3.2
Sheet 12
Sects. 4.3.3 and 4.3.4
Sheet 13 Sect. 4.4

 

Mock exam

To prepare for the exam, you can work on this mock exam.

Old slides

You can find slides from last year's lecture on the corresponding webpage. (You need a login.)

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.