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
|
| 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.
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.