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-026 |
| Exercise | Group 1: Monday, 16:00 - 18:00, building 101 HS 00-026 Group 2: Monday, 16:00 - 18:00, building 101 SR 01-016 Group 3: Tuesday, 12:00 - 14:00, building 051, SR 00-031 |
| 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. 25: The exam review (Klausureinsicht) takes place on Wednesday, April 24, 13:00 - 15:00 in room 00-016 of building 052.
- Jan. 24: Sheet 12 will be published on Friday, January 25.
You can submit the solutions until Thursday, January 31, 15:59. - Jan. 22: Updated exercise 1 on sheet 11. You can submit the solutions until Thursday, January 24, 15:59.
- Jan. 17: Sheet 11 will be published on Friday, January 18.
- Dec. 17: There is no exercise sheet to work on until this Wednesday, December 19. Therefore, there will not be exercise sessions on January 7 and 8.
Instead, there will be a lecture on January 7, 16:00-18:00 h, in building 101, HS 00-026. - Dec. 17: You will have the opportunity to catch up on previous sheets during the Christmas break. This is an offer to get feedback for your own solutions if you submit them until Wednesday, January 9.
- Dec. 10: As sheet 8 was published late, the submission deadline is extended. Please hand in your solutions until Thursday, Dec 13, 15:59.
- Nov. 23: Updated sheet 6. Added one more exercise and the motivation.
- Nov. 20: Note that slides are available in our Ilias group.
- Oct. 25: Prof. Podelski will give a tutorial for those who are not familiar with proofs by induction.
Date and time: Wednesday, October 31st, 13:15 - 14:00 h.
Room: building 051, SR 00-034 (so this is not the room of the lecture!) - Oct 22: Submission time for the exercises updated.
- Oct. 22: Today, 16:00 - 18:00, there will be an introductory lecture in 101, HS 00-026.
There are no exercise classes this week. - Oct. 19: The time and place for the third exercise group is set.
- Oct. 19: We created an Ilias course. You can join here.
- Oct. 17: Due to illness, the lecture today is cancelled. However, the first exercise sheet, with tasks on mathematical foundations, will be published later today and is due next Wednesday, Oct. 24.
- Oct. 15: Due to illness, the (additional) lecture planned for today is cancelled.
There are no exercise groups in the first week, of course. - Oct. 8: We start with a lecture on Monday, Oct. 15, 16:00 - 18:00 in building 101 HS 00-026. Edit: This means that there will be two lectures in the first week.
- Oct. 8: Homepage online.
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.
Exercises
The lecture is accompanied by exercises. Each Wednesday we will publish an exercise sheet. Students will have time until the next Wednesday to prepare solutions for the problems stated on the exercise sheet. Solutions may be submitted alone or in groups of two. The solutions can be submitted by 15:59 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 or Tuesday.
The exercises are optional. However, we highly recommend to solve them and submit your solutions. This will train you to write down things in a formally correct way (being able to write down things in a formally correct way is an important goal of this lecture, and you need to train it). It will help you to self-evaluate your knowledge. Last but not least, it will help you to evaluate your capability to solve the exercises in the exam.
Exam
There will be a written exam at the end of the semester.
You may bring one DIN A4 sheet to the exam. 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 one DIN A4 sheet to the exam. 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 |
Appendix of "Principles of Model Checking" |
| Sheet 2 |
Appendix of "Principles of Model Checking" |
| Sheet 3 |
Section 2.1 |
| Sheet 4 |
Section 2.2 |
| Sheet 5 |
Section 2.2 |
| Sheet 6 |
Section 2.2 |
| Sheet 7 |
Section 3.2 |
| Sheet 8 |
Section 3.2 |
| Sheet 9 |
Section 3.3 |
| Sheet 10 |
Section 3.3 |
| Sheet 11 |
Section 3.4 |
| Sheet 12 |
Section 3.5 |
Old lectures
You can find information on previous courses on the following web pages.
- Winter Term 2017/18 (Here you can find last year's mock exam, for instance.)
- Winter Term 2016/17 (Here you can find old slides.)
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.