« October 2017 »
October
MoTuWeThFrSaSu
1
2345678
9101112131415
16171819202122
23242526272829
3031
Uni-Logo
You are here: Home Teaching Winter Term 2017/18 Cyber-Physical Systems I - Discrete Models (Lecture)
Document Actions

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 

  • 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 at 12:00 noon 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)

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