# 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, Dominik Klumpp |

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: Monday, 16:00 - 18:00, building 051 SR 01-018 |

Language of instruction | English |

Credits | 6 |

Exams | Written exam |

Course catalog | Cyber-Physical Systems -- Discrete Models - Lecture Cyber-Physical Systems -- Discrete Models - Exercises |

## News

- Oct 18: On
**Monday, Oct 21**, there will be a lecture instead of the exercise sessions. The lecture will take place in room HS 00-026 in building 101. - Oct 18: An Ilias course has been created for the lecture. The lecture slides will be uploaded there, and there exists a discussion forum for your questions. If you are registered for the lecture in HisInOne, you will receive a link allowing you to join.
- Oct 14: Exercise Sheet 01 uploaded. This is a short exercise sheet which has to be submitted by Wednesday in the first week of lectures (Oct 23).
- Sep 27: 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 must be submitted by 15:59 on Wednesday via the post boxes that are located in the ground floor of building 051. The tutors will correct the solutions in the four following days (Thu - Sun) and discuss them in the exercise groups on Monday.

The exercises are not optional. You must obtain at least 50% of the exercise points. The goal is to 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). Correcting the exercises will help us to evaluate your knowledge and to evaluate your capability to solve the exercises in the exam.

The students present their solutions in the exercise group. This is done on a voluntary basis (you can choose which exercises you want to present), but every student must present his/her solution to an exercise in an exercise group at least once in the semester.

## Exam

There will be a written exam at the end of the semester.

You may bring

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

### Slides

The lecture slides are uploaded to the lecture's Ilias course.

### Exercise sheets

Exercise Sheet |
Submission By |
---|---|

Sheet 01 |
Oct 23, 16:00 |

### Old lectures

You can find information on previous courses on the following web pages.

- Winter Term 2018/19 (Here you can find old exercise sheets.)
- Winter Term 2017/18 (Here you can find an old 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.